From 26ba7a9eb493528432f73b990eb7e9c17f16e1b8 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 29 Jan 2003 17:02:40 +0000 Subject: [PATCH] Added a callback to the generalize tactic to generate a fresh name. --- helm/gTopLevel/gTopLevel.ml | 3 ++- helm/gTopLevel/proofEngine.ml | 3 ++- helm/gTopLevel/proofEngine.mli | 4 +++- 3 files changed, 7 insertions(+), 3 deletions(-) diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml index 27c6ca17b..3c57c96cb 100644 --- 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 313790a7f..577bdd705 100644 --- 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 59ed974ca..29a6f2d79 100644 --- 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 -- 2.39.2