(** Les types de notre langage *) type term_type = | Int | Bool | Arrow of term_type * term_type | Var of int (** Une substitution associe à toute variable de type [Var index] un type *) type substitution (** L'image de [Var index] par [empty_substitution] est [Var index]. *) val empty_substitution : substitution (** [image subst index] est l'image de [Var index] par [subst] *) val image : substitution -> int -> term_type (** Le type du résultat d'une unification *) type unification = | Success of substitution | Failure of substitution * term_type * term_type (** [unification constraints] calcule une substitution à appliquer * à chaque paire de termes de la liste [constraints] de contraintes, * de sorte que les images des deux membres d'une paire soient identiques. *) val unification : (term_type * term_type) list -> unification