From e9e3089b886e88a07267743cae79d6a9cabdd3c3 Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Tue, 5 Jul 2005 10:14:07 +0000
Subject: [PATCH] id ;-) and lapply patched

---
 helm/ocaml/tactics/fwdSimplTactic.ml | 27 +++++++++++++++++++--------
 helm/ocaml/tactics/tacticals.ml      |  7 +++++--
 2 files changed, 24 insertions(+), 10 deletions(-)

diff --git a/helm/ocaml/tactics/fwdSimplTactic.ml b/helm/ocaml/tactics/fwdSimplTactic.ml
index 6f64855d1..57c980513 100644
--- a/helm/ocaml/tactics/fwdSimplTactic.ml
+++ b/helm/ocaml/tactics/fwdSimplTactic.ml
@@ -44,6 +44,16 @@ let error msg = raise (PET.Fail msg)
 
 (* unexported tactics *******************************************************)
 
+let id_tac = 
+   let id_tac (proof,goal) = 
+      try
+         let _, metasenv, _, _ = proof in
+         let _, _, _ = CicUtil.lookup_meta goal metasenv in
+         (proof,[goal])
+      with CicUtil.Meta_not_found _ -> (proof, [])
+   in 
+   PET.mk_tactic id_tac
+
 let clearbody ~index =
    let rec find_name index = function
       | Some (Cic.Name name, _) :: _ when index = 1 -> name
@@ -68,20 +78,21 @@ let strip_prods metasenv context ?how_many to_what term =
       metasenv, Cic.Meta (index, irl), index
    in
    let update_counters = function
-      | None, []                 -> None, T.id_tac, []
-      | None, to_what :: tail    -> None, PT.apply_tac ~term:to_what, tail
-      | Some hm, []              -> Some (pred hm), T.id_tac, []
-      | Some hm, to_what :: tail -> Some (pred hm), PT.apply_tac ~term:to_what, tail
+      | None, []                 -> None, false, id_tac, []
+      | None, to_what :: tail    -> None, true, PT.apply_tac ~term:to_what, tail
+      | Some hm, []              -> Some (pred hm), false, id_tac, []
+      | Some hm, to_what :: tail -> Some (pred hm), true, PT.apply_tac ~term:to_what, tail
    in 
    let rec aux metasenv metas conts tw = function
       | Some hm, _ when hm <= 0               -> metasenv, metas, conts 
       | xhm, Cic.Prod (Cic.Name _, t1, t2)    ->
          let metasenv, meta, index = mk_meta metasenv t1 in    
-	 aux metasenv (meta :: metas) ((T.id_tac, index) :: conts) tw (xhm, (S.subst meta t2))      
+	 aux metasenv (meta :: metas) (conts @ [id_tac, index]) tw (xhm, (S.subst meta t2))      
       | xhm, Cic.Prod (Cic.Anonymous, t1, t2) ->
-         let xhm, tac, tw = update_counters (xhm, tw) in 
+         let xhm, pos, tac, tw = update_counters (xhm, tw) in 
          let metasenv, meta, index = mk_meta metasenv t1 in    
-	 aux metasenv (meta :: metas) ((tac, index) :: conts) tw (xhm, (S.subst meta t2))
+	 let conts = if pos then (tac, index) :: conts else conts @ [tac, index] in 
+	 aux metasenv (meta :: metas) conts tw (xhm, (S.subst meta t2))
       | _, t                                  -> metasenv, metas, conts 
    in
    aux metasenv [] [] to_what (how_many, term)
@@ -138,7 +149,7 @@ let fwd_simpl_tac
          | uri :: _ -> 
 	    Printf.eprintf "fwd: %s\n" (UriManager.string_of_uri uri); flush stderr;
 	    let start = lapply_tac (Cic.Rel index) (Cic.Const (uri, [])) in  
-            let tac = T.thens ~start ~continuations:[PESR.clearbody hyp] in
+            let tac = T.thens ~start ~continuations:[PESR.clear hyp] in
             PET.apply_tactic tac status
    in
    PET.mk_tactic fwd_simpl_tac
diff --git a/helm/ocaml/tactics/tacticals.ml b/helm/ocaml/tactics/tacticals.ml
index 3c89150ad..b72e6e24f 100644
--- a/helm/ocaml/tactics/tacticals.ml
+++ b/helm/ocaml/tactics/tacticals.ml
@@ -44,9 +44,12 @@ let warn s =
   (* not a tactical, but it's used only here (?) *)
 
 let id_tac = 
- let tac (proof,goal) = (proof,[goal])
+ let id_tac (proof,goal) = 
+  let _, metasenv, _, _ = proof in
+  let _, _, _ = CicUtil.lookup_meta goal metasenv in
+  (proof,[goal])
  in 
-  mk_tactic tac
+  mk_tactic id_tac
 
   (**
     naive implementation of ORELSE tactical, try a sequence of tactics in turn:
-- 
2.39.2