added patch to not unify any term containing the in_scope tag with

an entry in the local context

diff --git a/helm/software/components/ng_refiner/nCicMetaSubst.ml b/helm/software/components/ng_refiner/nCicMetaSubst.ml
index 94cfe669036143734c56d3c4e5d5992fe0977256..432f3e4bf064786df54d371ddaefdf140f73dac5 100644 (file)
--- a/helm/software/components/ng_refiner/nCicMetaSubst.ml
+++ b/helm/software/components/ng_refiner/nCicMetaSubst.ml
@@ -220,6 +220,8 @@ let int_of_out_scope_tag tag =
 ;;
 
 
+exception Found;;
+
 (* INVARIANT: we suppose that t is not another occurrence of Meta(n,_), 
    otherwise the occur check does not make sense in case of unification
    of ?n with ?n *)
@@ -232,11 +234,22 @@ let delift ~unify metasenv subst context n l t =
         with NCicUtils.Subst_not_found _ -> false)
     | _ -> false
   in
+  let contains_in_scope subst t = 
+    let rec aux _ () = function
+      | NCic.Meta _ as t ->
+          if is_in_scope_meta subst t then raise Found
+          else ()
+      | t -> 
+          if is_in_scope_meta subst t then raise Found
+          else NCicUtils.fold (fun _ () -> ()) () aux () t
+    in
+    try aux () () t; false with Found -> true
+  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 || is_in_scope_meta subst t then None else
+       if flexible_arg subst t || contains_in_scope 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 ->