X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FequalityTactics.ml;h=1d7c2f69cf5f1f70b08508362e200f6c92fdb75d;hb=40a7d275adaa09bfcc8642e383bd3e4a23c71506;hp=8cb794ff6e17e918eefd4f0696276a41fc806822;hpb=4a5311d795b19019a675f60c33710301873f646c;p=helm.git

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