From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 17 Nov 2005 18:19:39 +0000 (+0000)
Subject: Major code semplification and improvement:
X-Git-Tag: V_0_7_2_3~47
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=da3c6e228c3c7ec75c8fd80e8fd7846327eb1b39

Major code semplification and improvement:
 1. the proof term generated used to have a (Hletin) ...
    Now it has a (H) ...
 2. the code has been greatly simplified by renaming the old variable
    first and doing a letin later; I used to do the letin first and
    rename the new variable at the end
---

diff --git a/helm/ocaml/tactics/equalityTactics.ml b/helm/ocaml/tactics/equalityTactics.ml
index 2b2afae67..20dede31e 100644
--- a/helm/ocaml/tactics/equalityTactics.ml
+++ b/helm/ocaml/tactics/equalityTactics.ml
@@ -58,27 +58,19 @@ let rewrite_tac ~direction ~pattern equality =
             (Some (Cic.Name s,_))::_ -> s
           | _ -> assert false
        in
+        let dummy = "dummy" in
         Some arg,false,
          (fun ~term ->
            Tacticals.seq
             ~tactics:
-              [PT.letin_tac term;
-               PET.mk_tactic (fun status ->
-                PET.apply_tactic
-                 (ProofEngineStructuralRules.clearbody
-                   (last_hyp_name_of_status status)) status);
-               PET.mk_tactic (fun status ->
-                let hyp = last_hyp_name_of_status status in
-                 PET.apply_tactic
-                  (ReductionTactics.simpl_tac
-                    ~pattern:
-                      (None,[hyp,Cic.Implicit (Some `Hole)],Cic.Implicit None))
-                  status);
-               ProofEngineStructuralRules.clear name;
-               PET.mk_tactic (fun status ->
-                let hyp = last_hyp_name_of_status status in
-                 PET.apply_tactic
-                  (ProofEngineStructuralRules.rename hyp name) status)
+              [ProofEngineStructuralRules.rename name dummy;
+               PT.letin_tac
+                ~mk_fresh_name_callback:(fun _ _ _ ~typ -> Cic.Name name) term;
+               ProofEngineStructuralRules.clearbody name;
+               ReductionTactics.simpl_tac
+                ~pattern:
+                  (None,[name,Cic.Implicit (Some `Hole)],Cic.Implicit None);
+               ProofEngineStructuralRules.clear dummy
               ]),
          pat,gty
     | _ -> assert false (*CSC: not implemented yet!*)