Optional callbacks have been added to tactics that need to introduce

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

diff --git a/helm/gTopLevel/proofEngine.ml b/helm/gTopLevel/proofEngine.ml
index e333ec3b8ec9e5d741a2c856164ddfbbe0c32f66..99e6a081cdeaccb8940fe687eb30ae6bb380ea35 100644 (file)
--- a/helm/gTopLevel/proofEngine.ml
+++ b/helm/gTopLevel/proofEngine.ml
@@ -165,9 +165,12 @@ let simpl_in_scratch  = reduction_tactic_in_scratch ProofEngineReduction.simpl
 
 let can_apply term = can_apply_tactic (PrimitiveTactics.apply_tac ~term)
 let apply term = apply_tactic (PrimitiveTactics.apply_tac ~term)
-let intros () = apply_tactic PrimitiveTactics.intros_tac
-let cut term = apply_tactic (PrimitiveTactics.cut_tac ~term)
-let letin term = apply_tactic (PrimitiveTactics.letin_tac ~term)
+let intros ?mk_fresh_name_callback () =
+ apply_tactic (PrimitiveTactics.intros_tac ?mk_fresh_name_callback ())
+let cut ?mk_fresh_name_callback term =
+ apply_tactic (PrimitiveTactics.cut_tac ?mk_fresh_name_callback term)
+let letin ?mk_fresh_name_callback term =
+ apply_tactic (PrimitiveTactics.letin_tac ?mk_fresh_name_callback term)
 let exact term = apply_tactic (PrimitiveTactics.exact_tac ~term)
 let elim_intros_simpl term =
   apply_tactic (PrimitiveTactics.elim_intros_simpl_tac ~term)
@@ -232,7 +235,7 @@ let absurd term = apply_tactic (NegationTactics.absurd_tac ~term)
 let contradiction () = apply_tactic NegationTactics.contradiction_tac
 
 let decompose ~uris_choice_callback term =
- apply_tactic (EliminationTactics.decompose_tac ~term ~uris_choice_callback)
+ apply_tactic (EliminationTactics.decompose_tac ~uris_choice_callback term)
 
 (*
 let decide_equality () = apply_tactic VariousTactics.decide_equality_tac