...

diff --git a/helm/ocaml/cic_unification/cicUnification.ml b/helm/ocaml/cic_unification/cicUnification.ml
index 37f8621c8980d5fa50d2d8dd90114db33130c747..9c2dde84b45dd1aef507d2a6a00d3c8dcfb8e818 100644 (file)
--- 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)