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 8cb794ff6e17e918eefd4f0696276a41fc806822..1d7c2f69cf5f1f70b08508362e200f6c92fdb75d 100644 (file)
--- 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)) ;