Tactic generalize ported to patterns and activated in matita.

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

diff --git a/helm/ocaml/tactics/tactics.mli b/helm/ocaml/tactics/tactics.mli
index 5eb66704f7fe61f2d76cc379709ef49c7e1ecc19..b656fe58cc6af392219b12843d3f42c4cd6d6670 100644 (file)
--- a/helm/ocaml/tactics/tactics.mli
+++ b/helm/ocaml/tactics/tactics.mli
@@ -34,7 +34,7 @@ val fold :
 val fourier : ProofEngineTypes.tactic
 val generalize :
   ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
-  Cic.term list -> ProofEngineTypes.tactic
+  term:Cic.term -> ProofEngineTypes.pattern -> ProofEngineTypes.tactic
 val set_goal : int -> ProofEngineTypes.tactic
 val injection : term:Cic.term -> ProofEngineTypes.tactic
 val intros :