(* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *)
+exception Error of string lazy_t
type lowtac_status = {
pstatus : NCic.obj;
lstatus : LexiconEngine.status
}
-type lowtactic = lowtac_status * int -> lowtac_status * int list * int list
+type lowtactic = lowtac_status -> int -> lowtac_status
type tac_status = {
gstatus : Continuationals.Stack.t;
type tactic = tac_status -> tac_status
type tactic_term = CicNotationPt.term Disambiguate.disambiguator_input
+type tactic_pattern = GrafiteAst.npattern Disambiguate.disambiguator_input
val dot_tac: tactic
val branch_tac: tactic
val block_tac: tactic list -> tactic
val apply_tac: tactic_term -> tactic
+val change_tac: where:tactic_pattern -> with_what:tactic_term -> tactic
+val elim_tac: what:tactic_term -> where:tactic_pattern -> tactic
val pp_tac_status: tac_status -> unit