(* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *)
-val dot_tac: NTacStatus.tactic
-val branch_tac: NTacStatus.tactic
-val shift_tac: NTacStatus.tactic
-val pos_tac: int list -> NTacStatus.tactic
-val wildcard_tac: NTacStatus.tactic
-val merge_tac: NTacStatus.tactic
-val focus_tac: int list -> NTacStatus.tactic
-val unfocus_tac: NTacStatus.tactic
-val skip_tac: NTacStatus.tactic
+val dot_tac: 's NTacStatus.tactic
+val branch_tac: '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 repeat_tac: NTacStatus.tac_status NTacStatus.tactic -> 's NTacStatus.tactic
-val distribute_tac: NTacStatus.lowtactic -> NTacStatus.tactic
-val block_tac: NTacStatus.tactic list -> NTacStatus.tactic
+val distribute_tac:
+ NTacStatus.lowtac_status NTacStatus.lowtactic -> 's NTacStatus.tactic
+val block_tac: 's NTacStatus.tactic list -> 's NTacStatus.tactic
-val apply_tac: NTacStatus.tactic_term -> NTacStatus.tactic
+val apply_tac: NTacStatus.tactic_term -> 's NTacStatus.tactic
+val assumption_tac: 's NTacStatus.tactic
val change_tac:
where:NTacStatus.tactic_pattern -> with_what:NTacStatus.tactic_term ->
- NTacStatus.tactic
+ 's NTacStatus.tactic
+val cut_tac: NTacStatus.tactic_term -> 's NTacStatus.tactic
val elim_tac:
what:NTacStatus.tactic_term -> where:NTacStatus.tactic_pattern ->
- NTacStatus.tactic
-val intro_tac: string -> NTacStatus.tactic
+ 's NTacStatus.tactic
+val intro_tac: string -> 's NTacStatus.tactic
val cases_tac:
what:NTacStatus.tactic_term -> where:NTacStatus.tactic_pattern ->
- NTacStatus.tactic
-val case1_tac: string -> NTacStatus.tactic
+ '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 ->
- NTacStatus.tactic
-val generalize_tac : where:NTacStatus.tactic_pattern -> NTacStatus.tactic
-val eval_tac:
- reduction:[ `Whd of bool ] ->
- where:NTacStatus.tactic_pattern -> NTacStatus.tactic
+ 's NTacStatus.tactic
+val generalize_tac : where:NTacStatus.tactic_pattern -> 's NTacStatus.tactic
+val reduce_tac:
+ reduction:[ `Normalize of bool | `Whd of bool ] ->
+ where:NTacStatus.tactic_pattern -> 's NTacStatus.tactic
val letin_tac:
where:NTacStatus.tactic_pattern ->
what: NTacStatus.tactic_term ->
- string -> NTacStatus.tactic
+ string -> 's NTacStatus.tactic
val assert_tac:
- (string * [`Decl of NTacStatus.tactic_term | `Def of NTacStatus.tactic_term * NTacStatus.tactic_term]) list * NTacStatus.tactic_term ->
- NTacStatus.tactic
+ ((string * [`Decl of NTacStatus.tactic_term | `Def of NTacStatus.tactic_term * NTacStatus.tactic_term]) list * NTacStatus.tactic_term) list ->
+ 's NTacStatus.tactic
+
+val constructor_tac :
+ ?num:int -> args:NTacStatus.tactic_term list -> 's NTacStatus.tactic