X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2Ftactics.mli;h=b69e43e88328ebcec45200a7303ecc0686e7d742;hb=f541206af7fccf9de78b31d8f2aaf5f786f63d1f;hp=6bf03b6750ffe94aa2846685dda753af19048eff;hpb=e5efa2e0b70723b431cdc4cffe10b41167145ca4;p=helm.git

diff --git a/helm/ocaml/tactics/tactics.mli b/helm/ocaml/tactics/tactics.mli
index 6bf03b675..b69e43e88 100644
--- a/helm/ocaml/tactics/tactics.mli
+++ b/helm/ocaml/tactics/tactics.mli
@@ -36,6 +36,7 @@ val generalize :
 val set_goal : int -> ProofEngineTypes.tactic
 val injection : term:Cic.term -> ProofEngineTypes.tactic
 val intros :
+  ?howmany:int ->
   ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
   unit -> ProofEngineTypes.tactic
 val left : ProofEngineTypes.tactic