Added a callback to the generalize tactic to generate a fresh name.

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

diff --git a/helm/gTopLevel/proofEngine.ml b/helm/gTopLevel/proofEngine.ml
index 313790a7fd362c369326175c8182a2dec3be1f88..577bdd7053828ecf39adb8249bcff80e99da78f8 100644 (file)
--- a/helm/gTopLevel/proofEngine.ml
+++ b/helm/gTopLevel/proofEngine.ml
@@ -229,7 +229,8 @@ let right () = apply_tactic IntroductionTactics.right_tac
 
 let assumption () = apply_tactic VariousTactics.assumption_tac
 
-let generalize terms = apply_tactic (VariousTactics.generalize_tac ~terms)
+let generalize ?mk_fresh_name_callback terms =
+ apply_tactic (VariousTactics.generalize_tac ?mk_fresh_name_callback terms)
 
 let absurd term = apply_tactic (NegationTactics.absurd_tac ~term)
 let contradiction () = apply_tactic NegationTactics.contradiction_tac