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

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

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