X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_tactics%2FnTactics.mli;h=d9964ddcebbbd94f5b08b224f7792e36d294d4a0;hb=23fa9e70972efb0a805a4fecf6c91103f42408f2;hp=ab049f1c34fdc3495536a45c97f0273580c84e2b;hpb=e603c19e82c160362587cb0bc578287c87122b90;p=helm.git

diff --git a/helm/software/components/ng_tactics/nTactics.mli b/helm/software/components/ng_tactics/nTactics.mli
index ab049f1c3..d9964ddce 100644
--- a/helm/software/components/ng_tactics/nTactics.mli
+++ b/helm/software/components/ng_tactics/nTactics.mli
@@ -11,19 +11,26 @@
 
 (* $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: 's NTacStatus.tactic
+val branch_tac: ?force:bool -> 's NTacStatus.tactic
 val shift_tac: 's NTacStatus.tactic
 val pos_tac: int list -> 's NTacStatus.tactic
+val case_tac: string -> 's NTacStatus.tactic
 val wildcard_tac: 's NTacStatus.tactic
 val merge_tac: 's NTacStatus.tactic
 val focus_tac: int list -> 's NTacStatus.tactic
 val unfocus_tac: 's NTacStatus.tactic
 val skip_tac: 's NTacStatus.tactic
-val try_tac: 's NTacStatus.tactic -> 's NTacStatus.tactic
+val try_tac: NTacStatus.tac_status NTacStatus.tactic -> 's NTacStatus.tactic
+val repeat_tac: NTacStatus.tac_status NTacStatus.tactic -> 's NTacStatus.tactic
+
+val compare_statuses : past:#NTacStatus.lowtac_status -> present:#NTacStatus.lowtac_status -> int list * int list
 
 val distribute_tac:
  NTacStatus.lowtac_status NTacStatus.lowtactic -> 's NTacStatus.tactic
+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
@@ -31,19 +38,24 @@ val assumption_tac: 's NTacStatus.tactic
 val change_tac: 
    where:NTacStatus.tactic_pattern -> with_what:NTacStatus.tactic_term -> 
      's NTacStatus.tactic
+val cut_tac: NTacStatus.tactic_term -> 's NTacStatus.tactic
 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
 val case1_tac: string -> 's NTacStatus.tactic
+val lapply_tac: NTacStatus.tactic_term -> 's NTacStatus.tactic
 val rewrite_tac:
   dir:[ `LeftToRight | `RightToLeft ] ->
    what:NTacStatus.tactic_term -> where:NTacStatus.tactic_pattern -> 
     's NTacStatus.tactic
 val generalize_tac : where:NTacStatus.tactic_pattern -> 's NTacStatus.tactic
+val clear_tac : string list -> 's NTacStatus.tactic
 val reduce_tac: 
       reduction:[ `Normalize of bool | `Whd of bool ] ->
       where:NTacStatus.tactic_pattern -> 's NTacStatus.tactic
@@ -55,6 +67,24 @@ val assert_tac:
  ((string * [`Decl of NTacStatus.tactic_term | `Def of NTacStatus.tactic_term * NTacStatus.tactic_term]) list * NTacStatus.tactic_term) list ->
   's NTacStatus.tactic
 
-val auto_tac:
-  params:(NTacStatus.tactic_term list * (string * string) list) -> 
-   's NTacStatus.tactic
+val constructor_tac : 
+        ?num:int -> args:NTacStatus.tactic_term list -> 's NTacStatus.tactic
+
+val atomic_tac :
+ (NTacStatus.tac_status -> 'c #NTacStatus.status) ->
+   (#NTacStatus.tac_status as 'f) -> 'f
+
+type indtyinfo 
+
+val ref_of_indtyinfo : indtyinfo -> NReference.reference
+
+val analyze_indty_tac :
+    what:NTacStatus.tactic_term ->
+    indtyinfo option ref -> (#NTacStatus.tac_status as 'a) -> 'a
+
+
+val find_in_context : 'a -> ('a * 'b) list -> int
+
+val inversion_tac: 
+   what:NTacStatus.tactic_term -> where:NTacStatus.tactic_pattern -> 
+     's NTacStatus.tactic