test-suite/output/Tactics.v


1
2
3
4
5
6
7
8
9

(* Test printing of Tactic Notation *)

Tactic Notation "a" constr(x) := apply x.
Tactic Notation "e" constr(x) := exact x.

Lemma test : True -> True /\ True.
intro H; split; [a H|e H].
Show Script.
Qed.