From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 2 Mar 2004 17:39:57 +0000 (+0000)
Subject: ...
X-Git-Tag: v0_0_4~52
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=59dbe769533f32fb0fde68c516c7a5348c56cfe6;p=helm.git

...
---

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)