From 59dbe769533f32fb0fde68c516c7a5348c56cfe6 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 2 Mar 2004 17:39:57 +0000 Subject: [PATCH 1/1] ... --- helm/ocaml/cic_unification/cicUnification.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/helm/ocaml/cic_unification/cicUnification.ml b/helm/ocaml/cic_unification/cicUnification.ml index 37f8621c8..9c2dde84b 100644 --- a/helm/ocaml/cic_unification/cicUnification.ml +++ b/helm/ocaml/cic_unification/cicUnification.ml @@ -91,7 +91,7 @@ let rec fo_unif_subst subst context metasenv t1 t2 = else raise (UnificationFailure (sprintf "Error trying to unify %s with %s: the algorithm tried to check whether the two substitutions are convertible; if they are not, it tried to unify the two substitutions. No restriction was attempted." - (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm substt2))) + (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2))) | (C.Meta (n,l), C.Meta (m,_)) when n>m -> fo_unif_subst subst context metasenv t2 t1 | (C.Meta (n,l), t) -- 2.39.2