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

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 =

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

diff --git a/helm/gTopLevel/proofEngine.mli b/helm/gTopLevel/proofEngine.mli
index 59ed974cada6328782f22d9f2b55183548fb47b1..29a6f2d7945b26ba449225858c0f18178a621f73 100644 (file)
--- a/helm/gTopLevel/proofEngine.mli
+++ b/helm/gTopLevel/proofEngine.mli
@@ -79,7 +79,9 @@ val right : unit -> unit
 
 val assumption : unit -> unit
 
-val generalize : Cic.term list -> unit
+val generalize :
+ ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
+  Cic.term list -> unit
 
 val absurd : Cic.term -> unit
 val contradiction : unit -> unit