parameter sintax added to axiom statement

[helm.git] / helm / software / components / tactics / compose.mli

diff --git a/helm/software/components/tactics/compose.mli b/helm/software/components/tactics/compose.mli
index 37e69d42f3f37dfd9c78fd7d5b318b42f1fa9bb7..44db74b76aa2fe3ecb134d1be46e6d9311f57fb2 100644 (file)
--- a/helm/software/components/tactics/compose.mli
+++ b/helm/software/components/tactics/compose.mli
@@ -26,4 +26,5 @@
 val compose_tac: 
   ?howmany:int -> 
   ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
-  Cic.term -> Cic.term -> ProofEngineTypes.tactic
+  int (* times *) ->
+  Cic.term -> Cic.term option -> ProofEngineTypes.tactic