unification:

[helm.git] / helm / software / components / ng_tactics / nTactics.ml

diff --git a/helm/software/components/ng_tactics/nTactics.ml b/helm/software/components/ng_tactics/nTactics.ml
index 7fa2b48d8bc081f1a6fb3a5566253cd9bc89d7c7..f45aa656b5136ce182460ca856526390668129c3 100644 (file)
--- a/helm/software/components/ng_tactics/nTactics.ml
+++ b/helm/software/components/ng_tactics/nTactics.ml
@@ -240,13 +240,15 @@ let reopen status =
  let subst, newm = 
    List.partition 
     (function (_,(Some tag,_,_,_)) -> 
-            tag <> in_scope_tag && tag <> out_scope_tag
+            tag <> NCicMetaSubst.in_scope_tag && 
+            not (NCicMetaSubst.is_out_scope_tag tag)
     | _ -> true)
     subst 
  in
  let in_m, out_m = 
    List.partition
-     (function (_,(Some tag,_,_,_)) -> tag = in_scope_tag | _ -> assert false)
+     (function (_,(Some tag,_,_,_)) -> 
+         tag = NCicMetaSubst.in_scope_tag | _ -> assert false)
      newm
  in
  let metasenv = List.map (fun (i,(_,c,_,t)) -> i,(None,c,t)) in_m @ metasenv in
@@ -288,11 +290,11 @@ let elim_tac ~what ~where status =
    [ select_tac ~where;
      distribute_tac (fun status goal ->
        let goalty = get_goalty status goal in
+       let _,_,w = what in
        let status, what = 
          disambiguate status what None (ctx_of goalty) in
        let _ty_what = typeof status (ctx_of what) what in 
        (* check inductive... find eliminator *)
-       let w = (*astify what *) CicNotationPt.Ident ("m",None) in
        let holes = [ 
          CicNotationPt.Implicit;CicNotationPt.Implicit;CicNotationPt.Implicit]
        in