val print_tac: bool -> string -> 's NTacStatus.tactic
+val id_tac: 's NTacStatus.tactic
val dot_tac: 's NTacStatus.tactic
val branch_tac: ?force:bool -> 's NTacStatus.tactic
val shift_tac: 's NTacStatus.tactic
dir:[ `LeftToRight | `RightToLeft ] ->
what:NTacStatus.tactic_term -> where:NTacStatus.tactic_pattern ->
's NTacStatus.tactic
+val generalize0_tac : NotationPt.term list -> 's NTacStatus.tactic
val generalize_tac : where:NTacStatus.tactic_pattern -> 's NTacStatus.tactic
val clear_tac : string list -> 's NTacStatus.tactic
val reduce_tac:
val inversion_tac:
what:NTacStatus.tactic_term -> where:NTacStatus.tactic_pattern ->
's NTacStatus.tactic
+
+val exact_tac: NTacStatus.tactic_term -> 's NTacStatus.tactic