fixed typo

diff --git a/helm/ocaml/cic_unification/cicUnification.ml b/helm/ocaml/cic_unification/cicUnification.ml
index 90eacc56850f44102ab629a0d840be56c63d6253..fb1ca113f23e7f3b40035b8c68f47cd74bf9048d 100644 (file)
--- 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