The fresh_name generator has been moved to ProofEngineHelpers.

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

diff --git a/helm/gTopLevel/fourierR.ml b/helm/gTopLevel/fourierR.ml
index 9076ae70fffce795573bb6733e8140a60e73da04..bb1c2febf583893ed8c81fe387908782c39b0d3f 100644 (file)
--- a/helm/gTopLevel/fourierR.ml
+++ b/helm/gTopLevel/fourierR.ml
@@ -1004,8 +1004,7 @@ let assumption_tac ~status:(proof,goal)=
 let contradiction_tac ~status:(proof,goal)=
        Tacticals.then_ 
                 (*inutile sia questo che quello prima  della chiamata*)
-               ~start:
-                  (PrimitiveTactics.intros_tac ~mknames:(function () -> "boh"))
+               ~start:PrimitiveTactics.intros_tac
                ~continuation:(Tacticals.then_ 
                        ~start:(VariousTactics.elim_type_tac ~term:_False) 
                        ~continuation:(assumption_tac))
@@ -1045,11 +1044,11 @@ theoreme,so let's parse our thesis *)
 
    (* now let's change our thesis applying the th and put it with hp *) 
 
-   let proof,gl = Tacticals.then_ 
-       ~start:(PrimitiveTactics.apply_tac ~term:!th_to_appl)
-       ~continuation:
-          (PrimitiveTactics.intros_tac ~mknames:(function () -> fhyp))
-               ~status:(s_proof,s_goal) in
+   let proof,gl =
+    Tacticals.then_ 
+     ~start:(PrimitiveTactics.apply_tac ~term:!th_to_appl)
+     ~continuation:PrimitiveTactics.intros_tac
+     ~status:(s_proof,s_goal) in
    let goal = if List.length gl = 1 then List.hd gl 
                                     else failwith "a new goal" in