The fresh_name generator has been moved to ProofEngineHelpers.

[helm.git] / helm / gTopLevel / variousTactics.ml

diff --git a/helm/gTopLevel/variousTactics.ml b/helm/gTopLevel/variousTactics.ml
index 95b74ab99c7dde663a5a437cf5ce9da4f5fc1d5c..fc6897bafc9d8afa548a4bd5722705da0c6c0f0e 100644 (file)
--- a/helm/gTopLevel/variousTactics.ml
+++ b/helm/gTopLevel/variousTactics.ml
@@ -189,7 +189,7 @@ let contradiction_tac ~status =
   let module P = PrimitiveTactics in
   let module T = Tacticals in
    T.then_ 
-      ~start: (P.intros_tac ~mknames:(function () -> "FOO")) 
+      ~start:P.intros_tac
       ~continuation:(
         T.then_ 
            ~start: (elim_type_tac ~term:(C.MutInd (U.uri_of_string "cic:/Coq/Init/Logic/False.ind") 0 [] )) 
@@ -495,8 +495,7 @@ let replace_tac ~what ~with_what ~status:((proof, goal) as status) =
                                                        (* quale uguaglianza usare, eq o eqT ? *)
               ~continuations:[
                 T.then_ 
-                   ~start:
-                     (P.intros_tac ~mknames:(function () ->"dummy_for_replace"))
+                   ~start:P.intros_tac
                    ~continuation:(T.then_ 
                                      ~start:(rewrite_back_tac ~term:(C.Rel 1)) (* C.Name "dummy_for_replace" *)
                                      ~continuation:(ProofEngineStructuralRules.clear