assert false could happen

[helm.git] / helm / software / components / ng_tactics / nTactics.mli

diff --git a/helm/software/components/ng_tactics/nTactics.mli b/helm/software/components/ng_tactics/nTactics.mli
index e1a5de8957735d52ea20863a38c8e54ee080e40f..a4c48e68681b7171985bb30a812f2548b51a1199 100644 (file)
--- 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