X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_unification%2FcicUnification.ml;h=fb1ca113f23e7f3b40035b8c68f47cd74bf9048d;hb=c9995e146dc70bed25b9fe2913f3d5d31a4f9086;hp=bf035d74af217985f3a32f70126eed6afa133c4f;hpb=bf60fc57745fba8a2a22215ed1286eceae0f7700;p=helm.git

diff --git a/helm/ocaml/cic_unification/cicUnification.ml b/helm/ocaml/cic_unification/cicUnification.ml
index bf035d74a..fb1ca113f 100644
--- a/helm/ocaml/cic_unification/cicUnification.ml
+++ b/helm/ocaml/cic_unification/cicUnification.ml
@@ -38,9 +38,10 @@ let type_of_aux' metasenv subst context term =
   | CicMetaSubst.MetaSubstFailure msg ->
     raise (AssertFailure
       ((sprintf
-        "Type checking error: %s in context\n%s.\nException: %s.\nBroken invariant: unification must be invoked only on well typed terms"
+        "Type checking error: %s in context\n%s\nand metasenv\n%s.\nException: %s.\nBroken invariant: unification must be invoked only on well typed terms"
         (CicMetaSubst.ppterm subst term)
-        (CicMetaSubst.ppcontext subst context) msg)))
+        (CicMetaSubst.ppcontext subst context)
+        (CicMetaSubst.ppmetasenv metasenv subst) msg)))
 
 (* NUOVA UNIFICAZIONE *)
 (* A substitution is a (int * Cic.term) list that associates a
@@ -131,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