+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 distribute_tac: NTacStatus.lowtactic -> NTacStatus.tactic
+val block_tac: NTacStatus.tactic list -> NTacStatus.tactic
+
+val apply_tac: NTacStatus.tactic_term -> NTacStatus.tactic
+val change_tac:
+ where:NTacStatus.tactic_pattern -> with_what:NTacStatus.tactic_term ->
+ NTacStatus.tactic
+val elim_tac:
+ what:NTacStatus.tactic_term -> where:NTacStatus.tactic_pattern ->
+ NTacStatus.tactic
+val intro_tac: string -> NTacStatus.tactic
+val case1_tac: string -> NTacStatus.tactic