X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_tactics%2FnTactics.mli;h=a4c48e68681b7171985bb30a812f2548b51a1199;hb=668fb315dc8502dc1b4d336eba19ab9436bf5b7a;hp=e1a5de8957735d52ea20863a38c8e54ee080e40f;hpb=d272210a331d720b08d50b845fa21fa7ec0d4252;p=helm.git

diff --git a/helm/software/components/ng_tactics/nTactics.mli b/helm/software/components/ng_tactics/nTactics.mli
index e1a5de895..a4c48e686 100644
--- a/helm/software/components/ng_tactics/nTactics.mli
+++ b/helm/software/components/ng_tactics/nTactics.mli
@@ -11,6 +11,8 @@
 
 (* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *)
 
+val print_tac: bool -> string -> 's NTacStatus.tactic
+
 val dot_tac: 's NTacStatus.tactic
 val branch_tac: ?force:bool -> 's NTacStatus.tactic
 val shift_tac: 's NTacStatus.tactic
@@ -28,10 +30,7 @@ val compare_statuses : past:#NTacStatus.lowtac_status -> present:#NTacStatus.low
 
 val distribute_tac:
  NTacStatus.lowtac_status NTacStatus.lowtactic -> 's NTacStatus.tactic
-val exec : ((int * Continuationals.Stack.switch) list * 'a list * 'b list *
-      [> `NoTag ])
-     list NTacStatus.status NTacStatus.tactic -> 
-  (#NTacStatus.lowtac_status as 's) -> Continuationals.goal -> 's
+val exec : NTacStatus.tac_status NTacStatus.tactic -> 's NTacStatus.lowtactic
 val block_tac: 's NTacStatus.tactic list -> 's NTacStatus.tactic
 
 val apply_tac: NTacStatus.tactic_term -> 's NTacStatus.tactic