X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_refiner%2FnCicMetaSubst.ml;h=beeeeeb6b288a6c22cc0d8bfe28efd67c31066ef;hb=3df31c02806eca83c63c14e6a89844f764c3e2cb;hp=0207c9231e058b15d5ab820d21b0bf1719ca2cca;hpb=e2718488c73b2cdf20b26af46e80a11b91fac220;p=helm.git

diff --git a/matita/components/ng_refiner/nCicMetaSubst.ml b/matita/components/ng_refiner/nCicMetaSubst.ml
index 0207c9231..beeeeeb6b 100644
--- a/matita/components/ng_refiner/nCicMetaSubst.ml
+++ b/matita/components/ng_refiner/nCicMetaSubst.ml
@@ -53,7 +53,7 @@ let newmeta,maxmeta,pushmaxmeta,popmaxmeta =
   (fun () -> incr maxmeta; !maxmeta),
   (fun () -> !maxmeta),
   (fun () -> pushedmetas := !maxmeta::!pushedmetas; maxmeta := 0),
-  (fun () -> match !pushedmetas with [] -> assert false | hd::tl -> pushedmetas := tl)
+  (fun () -> match !pushedmetas with [] -> assert false | _hd::tl -> pushedmetas := tl)
 ;;
 
 exception NotFound of [`NotInTheList | `NotWellTyped];;
@@ -525,8 +525,7 @@ let delift status ~unify metasenv subst context n l t =
          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. *)