X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_tactics%2FnTactics.mli;h=a4b2bde6879231b7f8ad716d1f115144f43392b0;hb=95adf6dc8e29a71adc34e71eafe3f427990126e0;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..a4b2bde68 100644
--- a/helm/software/components/ng_tactics/nTactics.mli
+++ b/helm/software/components/ng_tactics/nTactics.mli
@@ -28,10 +28,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