X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_refiner%2FnCicMetaSubst.ml;h=e3ee8d60e0bdb48025c46a84da36e107d7f8e42f;hb=446bec03de2d1e48ee612cd8020777aeeb7fbf06;hp=73cc91892788b5b2c033f6fc39b17562f0530bbe;hpb=7aeec317f639936095e10f88cc0b2710262082d0;p=helm.git

diff --git a/matita/components/ng_refiner/nCicMetaSubst.ml b/matita/components/ng_refiner/nCicMetaSubst.ml
index 73cc91892..e3ee8d60e 100644
--- a/matita/components/ng_refiner/nCicMetaSubst.ml
+++ b/matita/components/ng_refiner/nCicMetaSubst.ml
@@ -57,8 +57,7 @@ exception NotFound of [`NotInTheList | `NotWellTyped];;
 
 let position to_skip n (shift, lc) =
   match lc with
-  | NCic.Irl _ when to_skip > 0 -> assert false  (* unclear to me *)
-  | NCic.Irl len when n <= shift || n > shift + len ->
+  | NCic.Irl len when n <= shift + to_skip || n > shift + len ->
      raise (NotFound `NotInTheList)
   | NCic.Irl _ -> n - shift
   | NCic.Ctx tl ->
@@ -261,18 +260,20 @@ and restrict status metasenv subst i (restrictions as orig) =
 ;;
 
 let rec is_flexible status context ~subst = function 
-  | NCic.Meta (i,_) ->
+  | NCic.Meta (i,lc) ->
+       (try 
+          let _,_,t,_ = NCicUtils.lookup_subst i subst in
+          let t = NCicSubstitution.subst_meta status lc t in
+          is_flexible status context ~subst t
+        with NCicUtils.Subst_not_found _ -> true)
+  | NCic.Appl (NCic.Meta (i,lc) :: args)-> 
       (try 
-        let _,_,t,_ = List.assoc i subst in
-        is_flexible status context ~subst t
-      with Not_found -> true)
-  | NCic.Appl (NCic.Meta (i,_) :: args)-> 
-      (try 
-        let _,_,t,_ = List.assoc i subst in
+        let _,_,t,_ = NCicUtils.lookup_subst i subst in
+        let t = NCicSubstitution.subst_meta status lc t in
         is_flexible status context ~subst 
           (NCicReduction.head_beta_reduce status ~delta:max_int 
             (NCic.Appl (t :: args)))
-      with Not_found -> true)
+      with NCicUtils.Subst_not_found _ -> true)
    (* this is a cheap whd, it only performs zeta-reduction.
     * 
     * it works when the **omissis** disambiguation algorithm
@@ -514,6 +515,11 @@ 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 _