From 04ade947888ac1115dfe104714bed61c32e1c9c3 Mon Sep 17 00:00:00 2001
From: Alberto Griggio <griggio@fbk.eu>
Date: Mon, 26 Sep 2005 14:55:28 +0000
Subject: [PATCH] added apply_tac_verbose_with_subst, returning a
 Cic.substitution instead of a substitution function, needed by the new
 paramodulation

---
 helm/ocaml/tactics/primitiveTactics.ml  | 22 +++++++++++++++-------
 helm/ocaml/tactics/primitiveTactics.mli |  5 +++++
 2 files changed, 20 insertions(+), 7 deletions(-)

diff --git a/helm/ocaml/tactics/primitiveTactics.ml b/helm/ocaml/tactics/primitiveTactics.ml
index 62f4eb1f3..f38dd10b3 100644
--- 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 5f608beb9..01d200eb7 100644
--- 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 ->
-- 
2.39.2