From: Wilmer Ricciotti <ricciott@cs.unibo.it>
Date: Fri, 27 Jan 2012 14:31:20 +0000 (+0000)
Subject: Fixes a bug in is_flexible (when checking a meta in subst, we did a recursive
X-Git-Tag: make_still_working~1966
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=e305a62a7cb0a49fea3d241474e4c5bcd40e7272;p=helm.git

Fixes a bug in is_flexible (when checking a meta in subst, we did a recursive
call on its body without applying the local context, resulting in various
assertion failures).
---

diff --git a/matita/components/ng_refiner/nCicMetaSubst.ml b/matita/components/ng_refiner/nCicMetaSubst.ml
index f1fa293b3..57f12a458 100644
--- a/matita/components/ng_refiner/nCicMetaSubst.ml
+++ b/matita/components/ng_refiner/nCicMetaSubst.ml
@@ -260,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