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

diff --git a/helm/ocaml/cic_unification/cicUnification.ml b/helm/ocaml/cic_unification/cicUnification.ml
index 3c8b07729..fb1ca113f 100644
--- a/helm/ocaml/cic_unification/cicUnification.ml
+++ b/helm/ocaml/cic_unification/cicUnification.ml
@@ -25,8 +25,9 @@
 
 open Printf
 
-exception AssertFailure of string;;
 exception UnificationFailure of string;;
+exception Uncertain of string;;
+exception AssertFailure of string;;
 
 let debug_print = prerr_endline
 
@@ -37,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
@@ -96,7 +98,11 @@ let rec fo_unif_subst subst context metasenv t1 t2 =
           fo_unif_subst subst context metasenv lifted_oldt t
         with Not_found ->
          let t',metasenv',subst' =
+          try
            CicMetaSubst.delift n subst context metasenv l t
+          with
+             (CicMetaSubst.MetaSubstFailure msg)-> raise(UnificationFailure msg)
+           | (CicMetaSubst.Uncertain msg) -> raise (Uncertain msg)
          in
           (n, t')::subst', metasenv'
        in
@@ -126,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