X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_tactics%2FnTactics.mli;h=822421a24eebe3716663c45d765712aaccaa2a07;hb=f57cdba1f7cad1891a2fcc38432f73a584d47e48;hp=74bbcbcb4214a3565506a04d1dc81695bf746970;hpb=12f96bd48b460d06f9858a334ee7c52d6831712f;p=helm.git

diff --git a/helm/software/components/ng_tactics/nTactics.mli b/helm/software/components/ng_tactics/nTactics.mli
index 74bbcbcb4..822421a24 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
@@ -44,6 +43,8 @@ val elim_tac:
    what:NTacStatus.tactic_term -> where:NTacStatus.tactic_pattern -> 
      's NTacStatus.tactic
 val intro_tac: string -> 's NTacStatus.tactic
+val intros_tac: 
+     ?names_ref:string list ref -> string list -> 's NTacStatus.tactic
 val cases_tac: 
    what:NTacStatus.tactic_term -> where:NTacStatus.tactic_pattern -> 
      's NTacStatus.tactic
@@ -95,3 +96,7 @@ val analyze_indty_tac :
 
 
 val find_in_context : 'a -> ('a * 'b) list -> int
+
+val inversion_tac: 
+   what:NTacStatus.tactic_term -> where:NTacStatus.tactic_pattern -> 
+     's NTacStatus.tactic