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

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

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index 27c6ca17b8ec1915f410256dea436d50c662ddd7..3c57c96cb96214a2232c99caafaa2f304d8a3db8 100644 (file)
--- a/helm/gTopLevel/gTopLevel.ml
+++ b/helm/gTopLevel/gTopLevel.ml
@@ -2292,7 +2292,8 @@ let split = call_tactic ProofEngine.split;;
 let left = call_tactic ProofEngine.left;;
 let right = call_tactic ProofEngine.right;;
 let assumption = call_tactic ProofEngine.assumption;;
-let generalize = call_tactic_with_goal_inputs ProofEngine.generalize;;
+let generalize =
+ call_tactic_with_goal_inputs (ProofEngine.generalize ~mk_fresh_name_callback);;
 let absurd = call_tactic_with_input ProofEngine.absurd;;
 let contradiction = call_tactic ProofEngine.contradiction;;
 let decompose =