Most warnings turned into errors and avoided

[helm.git] / matita / components / ng_refiner / nCicMetaSubst.ml

diff --git a/matita/components/ng_refiner/nCicMetaSubst.ml b/matita/components/ng_refiner/nCicMetaSubst.ml
index 57f12a458fd160bb3a1917bbad2079101aad7e00..beeeeeb6b288a6c22cc0d8bfe28efd67c31066ef 100644 (file)
--- a/matita/components/ng_refiner/nCicMetaSubst.ml
+++ b/matita/components/ng_refiner/nCicMetaSubst.ml
@@ -47,10 +47,13 @@ let outside exc_opt =
 exception MetaSubstFailure of string Lazy.t
 exception Uncertain of string Lazy.t
 
-let newmeta,maxmeta = 
+let newmeta,maxmeta,pushmaxmeta,popmaxmeta = 
   let maxmeta = ref 0 in
+  let pushedmetas = ref [] in
   (fun () -> incr maxmeta; !maxmeta),
-  (fun () -> !maxmeta)
+  (fun () -> !maxmeta),
+  (fun () -> pushedmetas := !maxmeta::!pushedmetas; maxmeta := 0),
+  (fun () -> match !pushedmetas with [] -> assert false | _hd::tl -> pushedmetas := tl)
 ;;
 
 exception NotFound of [`NotInTheList | `NotWellTyped];;
@@ -515,10 +518,14 @@ let delift status ~unify metasenv subst context n l t =
         NCicUtils.Meta_not_found _ ->
          (* Fake metavariable used in NTacStatus and NCicRefiner :-( *)
          assert (n = -1); res
+      | NCicTypeChecker.TypeCheckerFailure msg ->
+         HLog.error "----------- Problem with Dependent Types ----------";
+         HLog.error (Lazy.force msg) ;
+         HLog.error "---------------------------------------------------";
+         raise (NotFound `NotWellTyped)
       | TypeNotGood
       | NCicTypeChecker.AssertFailure _
-      | NCicReduction.AssertFailure _
-      | NCicTypeChecker.TypeCheckerFailure _ ->
+      | NCicReduction.AssertFailure _ ->
          raise (NotFound `NotWellTyped))
    with NotFound reason ->
       (* This is the case where we fail even first order unification. *)