From 40a7d275adaa09bfcc8642e383bd3e4a23c71506 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 5 Sep 2003 13:00:27 +0000
Subject: [PATCH] Replace tactic fixed. It was not working any longer. (It
 produced a dummy eta-expansion).

---
 helm/ocaml/tactics/equalityTactics.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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)) ;
-- 
2.39.2