From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 5 Sep 2003 13:00:27 +0000 (+0000)
Subject: Replace tactic fixed. It was not working any longer. (It produced a dummy
X-Git-Tag: v0_0_1~34
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=40a7d275adaa09bfcc8642e383bd3e4a23c71506

Replace tactic fixed. It was not working any longer. (It produced a dummy
eta-expansion).
---

diff --git a/helm/ocaml/tactics/equalityTactics.ml b/helm/ocaml/tactics/equalityTactics.ml
index 8cb794ff6..1d7c2f69c 100644
--- a/helm/ocaml/tactics/equalityTactics.ml
+++ b/helm/ocaml/tactics/equalityTactics.ml
@@ -169,7 +169,7 @@ let replace_tac ~what ~with_what ~status:((proof, goal) as status) =
                      with_what]))
               ~continuations:[
                 T.then_
-                   ~start:(rewrite_back_tac ~term:(C.Rel 1))
+                   ~start:(rewrite_simpl_tac ~term:(C.Rel 1))
                    ~continuation:(
                      ProofEngineStructuralRules.clear
                       ~hyp:(List.hd context)) ;