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

[helm.git] / helm / ocaml / tactics / proofEngineReduction.mli

diff --git a/helm/ocaml/tactics/proofEngineReduction.mli b/helm/ocaml/tactics/proofEngineReduction.mli
index 2c210b677c3e02c8861a43ca058018cf81d5e426..e3bdfd49ee39606d85f955831bd107662465580b 100644 (file)
--- a/helm/ocaml/tactics/proofEngineReduction.mli
+++ b/helm/ocaml/tactics/proofEngineReduction.mli
@@ -43,6 +43,6 @@ val replace_lifting :
   what:Cic.term -> with_what:Cic.term -> where:Cic.term -> Cic.term
 val replace_lifting_csc :
   int -> equality:(Cic.term -> Cic.term -> bool) ->
-  what:Cic.term -> with_what:Cic.term -> where:Cic.term -> Cic.term
+  what:Cic.term list -> with_what:Cic.term list -> where:Cic.term -> Cic.term
 val reduce : Cic.context -> Cic.term -> Cic.term
 val simpl : Cic.context -> Cic.term -> Cic.term