From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Thu, 9 Apr 2009 13:09:16 +0000 (+0000)
Subject: ?_OS1 := C[ ?_IN ]
X-Git-Tag: make_still_working~4098
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=f094694e53cfeea2c33e8c2aa2abac6dd7e44138;p=helm.git

?_OS1 := C[ ?_IN ]
?_IN := m
=======================
?[m;m]  =?=  ?_OS1

used to yield ? := Rel 2 instead of Rel 1, since the first m
was still out of scope when recursion reaches ?_IN
---

diff --git a/helm/software/components/ng_refiner/nCicMetaSubst.ml b/helm/software/components/ng_refiner/nCicMetaSubst.ml
index adc1ac620..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 ->