added apply_tac_verbose_with_subst, returning a Cic.substitution instead of a

substitution function, needed by the new paramodulation

diff --git a/helm/ocaml/tactics/primitiveTactics.ml b/helm/ocaml/tactics/primitiveTactics.ml
index 62f4eb1f30e947e1fb510fb253dfb7af1c6aeb4c..f38dd10b3108c13a991d6ad00b73b0868bbb0ca3 100644 (file)
--- a/helm/ocaml/tactics/primitiveTactics.ml
+++ b/helm/ocaml/tactics/primitiveTactics.ml
@@ -239,7 +239,7 @@ 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 ~term (proof, goal) =
+let apply_tac_verbose_with_subst ~term (proof, goal) =
   (* Assumption: The term "term" must be closed in the current context *)
  let module T = CicTypeChecker in
  let module R = CicReduction in
@@ -313,15 +313,16 @@ let apply_tac_verbose ~term (proof, goal) =
    let (newproof, newmetasenv''') = 
      subst_meta_and_metasenv_in_proof proof metano subst_in newmetasenv''
    in
-     (subst_in,
-       (newproof, 
-          List.map (function (i,_,_) -> i) new_uninstantiatedmetas))
+   (((metano,(context,bo',Cic.Implicit None))::subst)(* subst_in *), (* ALB *)
+    (newproof, 
+     List.map (function (i,_,_) -> i) new_uninstantiatedmetas))
 
-let apply_tac ~term status = snd (apply_tac_verbose ~term status)
 
-let apply_tac_verbose ~term status =
+(* ALB *)
+let apply_tac_verbose_with_subst ~term status =
   try
-    apply_tac_verbose ~term status
+(*     apply_tac_verbose ~term status *)
+    apply_tac_verbose_with_subst ~term status
       (* TODO cacciare anche altre eccezioni? *)
   with 
   | CicUnification.UnificationFailure _ as e -> 
@@ -329,6 +330,13 @@ let apply_tac_verbose ~term status =
   | CicTypeChecker.TypeCheckerFailure _ as e ->
       raise (Fail (Printexc.to_string e))
 
+(* ALB *)
+let apply_tac_verbose ~term status =
+  let subst, status = apply_tac_verbose_with_subst ~term status in
+  (CicMetaSubst.apply_subst subst), status
+
+let apply_tac ~term status = snd (apply_tac_verbose ~term status)
+
   (* TODO per implementare i tatticali e' necessario che tutte le tattiche
   sollevino _solamente_ Fail *)
 let apply_tac ~term =

diff --git a/helm/ocaml/tactics/primitiveTactics.mli b/helm/ocaml/tactics/primitiveTactics.mli
index 5f608beb9143982e3359fd52e33ca1c8769c199d..01d200eb76ece2859d1e460e7f6447bfda339729 100644 (file)
--- a/helm/ocaml/tactics/primitiveTactics.mli
+++ b/helm/ocaml/tactics/primitiveTactics.mli
@@ -23,6 +23,11 @@
  * http://cs.unibo.it/helm/.
  *)
 
+(* ALB, needed by the new paramodulation... *)
+val apply_tac_verbose_with_subst:
+  term:Cic.term -> ProofEngineTypes.proof * int ->
+  Cic.substitution * (ProofEngineTypes.proof * int list)
+
 (* not a real tactic *)
 val apply_tac_verbose :
   term:Cic.term ->