Big changes:

[helm.git] / helm / ocaml / cic_unification / cicUnification.ml

diff --git a/helm/ocaml/cic_unification/cicUnification.ml b/helm/ocaml/cic_unification/cicUnification.ml
index 3c8b077297fd5ad8da82700f4dd081fade124c19..bf035d74af217985f3a32f70126eed6afa133c4f 100644 (file)
--- 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
 
@@ -96,7 +97,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