Typing of intros_tac improved. It now has a parameter that is a fresh-names

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

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