apply now uses both menv and subst to decide the fresh meta number

diff --git a/helm/software/components/tactics/primitiveTactics.ml b/helm/software/components/tactics/primitiveTactics.ml
index 192460633d7577ff26a18e40d2d8ac4e8f699651..e09f0a1f7dc890ecbee234b53042677fea3aab91 100644 (file)
--- a/helm/software/components/tactics/primitiveTactics.ml
+++ b/helm/software/components/tactics/primitiveTactics.ml
@@ -246,14 +246,14 @@ let rec count_prods context ty =
     Cic.Prod (n,s,t) -> 1 + count_prods (Some (n,Cic.Decl s)::context) t
   | _ -> 0
 
-let apply_tac_verbose_with_subst ~term (proof, goal) =
+let apply_with_subst ~term ~subst (proof, goal) =
   (* Assumption: The term "term" must be closed in the current context *)
  let module T = CicTypeChecker in
  let module R = CicReduction in
  let module C = Cic in
   let (_,metasenv,_,_) = proof in
   let metano,context,ty = CicUtil.lookup_meta goal metasenv in
-  let newmeta = new_meta_of_proof ~proof in
+  let newmeta = CicMkImplicit.new_meta metasenv subst in
    let exp_named_subst_diff,newmeta',newmetasenvfragment,term' =
     match term with
        C.Var (uri,exp_named_subst) ->
@@ -326,10 +326,10 @@ let apply_tac_verbose_with_subst ~term (proof, goal) =
 
 
 (* ALB *)
-let apply_tac_verbose_with_subst ~term status =
+let apply_with_subst ~term ?(subst=[]) status =
   try
 (*     apply_tac_verbose ~term status *)
-    apply_tac_verbose_with_subst ~term status
+    apply_with_subst ~term ~subst status
       (* TODO cacciare anche altre eccezioni? *)
   with 
   | CicUnification.UnificationFailure msg
@@ -338,7 +338,7 @@ let apply_tac_verbose_with_subst ~term status =
 
 (* ALB *)
 let apply_tac_verbose ~term status =
-  let subst, status = apply_tac_verbose_with_subst ~term status in
+  let subst, status = apply_with_subst ~term status in
   (CicMetaSubst.apply_subst subst), status
 
 let apply_tac ~term status = snd (apply_tac_verbose ~term status)

diff --git a/helm/software/components/tactics/primitiveTactics.mli b/helm/software/components/tactics/primitiveTactics.mli
index ce5194ad133e4c1435ed6932189c86628f60916d..c30952cae8b4ba6dc99aeca7549aa0ed98ad840a 100644 (file)
--- a/helm/software/components/tactics/primitiveTactics.mli
+++ b/helm/software/components/tactics/primitiveTactics.mli
@@ -43,8 +43,8 @@ val classify_metas :
   (Cic.term * Cic.context * Cic.term) list
 
 (* ALB, needed by the new paramodulation... *)
-val apply_tac_verbose_with_subst:
-  term:Cic.term -> ProofEngineTypes.proof * int ->
+val apply_with_subst:
+  term:Cic.term -> ?subst:Cic.substitution -> ProofEngineTypes.proof * int ->
   Cic.substitution * (ProofEngineTypes.proof * int list)
 
 (* not a real tactic *)