Generalize now works on a list of convertible terms, generalizing all of

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

diff --git a/helm/gTopLevel/proofEngine.mli b/helm/gTopLevel/proofEngine.mli
index 8f8b1261d4e6bfb66bf1a2133860719d90ab1587..59ed974cada6328782f22d9f2b55183548fb47b1 100644 (file)
--- a/helm/gTopLevel/proofEngine.mli
+++ b/helm/gTopLevel/proofEngine.mli
@@ -79,7 +79,7 @@ val right : unit -> unit
 
 val assumption : unit -> unit
 
-val generalize : Cic.term -> unit
+val generalize : Cic.term list -> unit
 
 val absurd : Cic.term -> unit
 val contradiction : unit -> unit