fix

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

diff --git a/helm/ocaml/tactics/tactics.mli b/helm/ocaml/tactics/tactics.mli
index 6bf03b6750ffe94aa2846685dda753af19048eff..b69e43e88328ebcec45200a7303ecc0686e7d742 100644 (file)
--- 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