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

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

diff --git a/helm/gTopLevel/fourierR.ml b/helm/gTopLevel/fourierR.ml
index 07a94a9b1252108ffed55b294fef0447eab75d3d..c08183bebf889300aa8c56893930d4a842e3deaf 100644 (file)
--- a/helm/gTopLevel/fourierR.ml
+++ b/helm/gTopLevel/fourierR.ml
@@ -1002,7 +1002,9 @@ let assumption_tac ~status:(proof,goal)=
 (* !!!!! fix !!!!!!!!!! *)
 let contradiction_tac ~status:(proof,goal)=
        Tacticals.then_ 
-               ~start:(PrimitiveTactics.intros_tac ~name:"bo?" ) (*inutile sia questo che quello prima  della chiamata*)
+                (*inutile sia questo che quello prima  della chiamata*)
+               ~start:
+                  (PrimitiveTactics.intros_tac ~mknames:(function () -> "boh"))
                ~continuation:(Tacticals.then_ 
                        ~start:(VariousTactics.elim_type_tac ~term:_False) 
                        ~continuation:(assumption_tac))
@@ -1044,7 +1046,8 @@ theoreme,so let's parse our thesis *)
 
    let proof,gl = Tacticals.then_ 
        ~start:(PrimitiveTactics.apply_tac ~term:!th_to_appl)
-       ~continuation:(PrimitiveTactics.intros_tac ~name:fhyp)
+       ~continuation:
+          (PrimitiveTactics.intros_tac ~mknames:(function () -> fhyp))
                ~status:(s_proof,s_goal) in
    let goal = if List.length gl = 1 then List.hd gl 
                                     else failwith "a new goal" in