new more flexible compose, see matita/tests/compose.ma for a sample

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

diff --git a/components/tactics/tactics.mli b/components/tactics/tactics.mli
index d63e8805cf6d846e92b63d16e4c74cd236c9a9ce..16c668266987e31378f64737531ba32c16ba2017 100644 (file)
--- a/components/tactics/tactics.mli
+++ b/components/tactics/tactics.mli
@@ -1,4 +1,4 @@
-(* GENERATED FILE, DO NOT EDIT. STAMP:Fri Jun  1 17:03:59 CEST 2007 *)
+(* GENERATED FILE, DO NOT EDIT. STAMP:Mon Jun  4 13:44:18 CEST 2007 *)
 val absurd : term:Cic.term -> ProofEngineTypes.tactic
 val apply : term:Cic.term -> ProofEngineTypes.tactic
 val applyS :
@@ -105,4 +105,4 @@ val whd : pattern:ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic
 val compose :
   ?howmany:int ->
   ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
-  Cic.term -> Cic.term -> ProofEngineTypes.tactic
+  int -> Cic.term -> Cic.term option -> ProofEngineTypes.tactic