X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fcompose.mli;h=44db74b76aa2fe3ecb134d1be46e6d9311f57fb2;hb=9e7df95a820cb91d075f1a20d703175da874596c;hp=37e69d42f3f37dfd9c78fd7d5b318b42f1fa9bb7;hpb=3990759a81db3ce45bf4ec56e1985e532151f6e0;p=helm.git

diff --git a/helm/software/components/tactics/compose.mli b/helm/software/components/tactics/compose.mli
index 37e69d42f..44db74b76 100644
--- 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