Optional callbacks have been added to tactics that need to introduce

[helm.git] / helm / ocaml / tactics / equalityTactics.ml

diff --git a/helm/ocaml/tactics/equalityTactics.ml b/helm/ocaml/tactics/equalityTactics.ml
index 79b5b1dbe499e50a6b2d26788a023bcf30081554..29df82c08ab5f21f121a688231ecf98d46058836 100644 (file)
--- a/helm/ocaml/tactics/equalityTactics.ml
+++ b/helm/ocaml/tactics/equalityTactics.ml
@@ -162,12 +162,11 @@ let replace_tac ~what ~with_what ~status:((proof, goal) as status) =
        then T.thens
               ~start:(
                 P.cut_tac 
-                   ~term:(
-                     C.Appl [
-                      (C.MutInd ((U.uri_of_string "cic:/Coq/Init/Logic/eq.ind"), 0, [])) ; (* quale uguaglianza usare, eq o eqT ? *)
-                      wty ; 
-                      what ; 
-                      with_what]))
+                 (C.Appl [
+                   (C.MutInd ((U.uri_of_string "cic:/Coq/Init/Logic/eq.ind"), 0, [])) ; (* quale uguaglianza usare, eq o eqT ? *)
+                     wty ; 
+                     what ; 
+                     with_what]))
               ~continuations:[
                 T.then_
                    ~start:(rewrite_back_tac ~term:(C.Rel 1)) (* C.Name "dummy_for_replace" *)