1. Added a callback to the generalize tactic to generate a fresh name.

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

diff --git a/helm/ocaml/tactics/equalityTactics.ml b/helm/ocaml/tactics/equalityTactics.ml
index c1212360c96d0c1702b0055ff6a51417dd691dc3..4ff71c792a2af0f030b43102724c0f6d3d896d85 100644 (file)
--- a/helm/ocaml/tactics/equalityTactics.ml
+++ b/helm/ocaml/tactics/equalityTactics.ml
@@ -169,11 +169,10 @@ let replace_tac ~what ~with_what ~status:((proof, goal) as status) =
                      with_what]))
               ~continuations:[
                 T.then_
-                   ~start:(rewrite_back_tac ~term:(C.Rel 1)) (* C.Name "dummy_for_replace" *)
+                   ~start:(rewrite_back_tac ~term:(C.Rel 1))
                    ~continuation:(
                      ProofEngineStructuralRules.clear
                       ~hyp:(List.hd context)) ;
-(*                                                     (Some(C.Name "dummy_for_replace" , C.Def (CicTypeChecker.type_of_aux' metasenv context (C.Rel 1)) (* NOOOO!!!!! tipo di dummy *) )))) ; *)
                 T.id_tac]
               ~status
        else raise (ProofEngineTypes.Fail "Replace: terms not replaceable")