From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Wed, 11 Feb 2004 12:09:30 +0000 (+0000)
Subject: fixed typo
X-Git-Tag: V_0_3_0~15
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=22d6cd4a655dcb53de42877ea3faf5432e201111;p=helm.git

fixed typo
---

diff --git a/helm/ocaml/cic_unification/cicUnification.ml b/helm/ocaml/cic_unification/cicUnification.ml
index 90eacc568..fb1ca113f 100644
--- a/helm/ocaml/cic_unification/cicUnification.ml
+++ b/helm/ocaml/cic_unification/cicUnification.ml
@@ -132,7 +132,7 @@ prerr_endline "********* PROCEED AT YOUR OWN RISK. AND GOOD LUCK." ;
       else
        raise (UnificationFailure (sprintf
         "Can't unify %s with %s due to different constants"
-        (CicPp.ppterm t1) (CicPp.ppterm t1)))
+        (CicPp.ppterm t1) (CicPp.ppterm t2)))
    | C.MutInd (uri1,i1,exp_named_subst1),C.MutInd (uri2,i2,exp_named_subst2) ->
       if UriManager.eq uri1 uri2 && i1 = i2 then
        fo_unif_subst_exp_named_subst subst context metasenv