X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_refiner%2FnCicMetaSubst.ml;h=94cfe669036143734c56d3c4e5d5992fe0977256;hb=7233348f05485c2ee317df9c3407cf1ce7e56927;hp=1a2b5471b0cf76910eb0666c1cba0fb96a59b7bb;hpb=d174e54c365ab9df38367de9336c213a03be3c27;p=helm.git

diff --git a/helm/software/components/ng_refiner/nCicMetaSubst.ml b/helm/software/components/ng_refiner/nCicMetaSubst.ml
index 1a2b5471b..94cfe6690 100644
--- a/helm/software/components/ng_refiner/nCicMetaSubst.ml
+++ b/helm/software/components/ng_refiner/nCicMetaSubst.ml
@@ -224,11 +224,19 @@ let int_of_out_scope_tag tag =
    otherwise the occur check does not make sense in case of unification
    of ?n with ?n *)
 let delift ~unify metasenv subst context n l t =
+  let is_in_scope_meta subst = function
+    | NCic.Meta (i,_) ->
+        (try 
+           let tag, _, _, _ = NCicUtils.lookup_subst i subst in 
+           tag = Some in_scope_tag 
+        with NCicUtils.Subst_not_found _ -> false)
+    | _ -> false
+  in
   let unify_list in_scope = 
     match l with
     | _, NCic.Irl _ -> fun _ _ _ _ _ -> None
     | shift, NCic.Ctx l -> fun metasenv subst context k t ->
-       if flexible_arg subst t then None else
+       if flexible_arg subst t || is_in_scope_meta subst t then None else
          let lb = List.map (fun t -> t, flexible_arg subst t) l in
          HExtlib.list_findopt
           (fun (li,flexible) i ->
@@ -266,12 +274,18 @@ let delift ~unify metasenv subst context n l t =
             (NCicPp.ppterm ~context ~metasenv ~subst t))))
     | NCic.Meta (i,l1) as orig ->
         (try
-           let tag,_,t,_ = NCicUtils.lookup_subst i subst in
-           let in_scope = 
+           let tag,c,t,ty = NCicUtils.lookup_subst i subst in
+           let in_scope, clear = 
              match tag with 
-             | Some tag when tag = in_scope_tag -> 0
-             | Some tag when is_out_scope_tag tag -> int_of_out_scope_tag tag
-             | _ -> in_scope
+             | Some tag when tag = in_scope_tag -> 0, true
+             | Some tag when is_out_scope_tag tag->int_of_out_scope_tag tag,true
+             | _ -> in_scope, false
+           in
+           let ms = 
+             if not clear then ms
+             else 
+               metasenv, 
+               (i,(None,c,t,ty)) :: List.filter (fun j,_ -> i <> j) subst
            in
            aux (context,k,in_scope) ms (NCicSubstitution.subst_meta l1 t)
          with NCicUtils.Subst_not_found _ ->