aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/output/Tactics.v
blob: a7c497cfaf62bdb9bd7a6b846bf6b1e26ca0a0e5 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
(* Test printing of Tactic Notation *)

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

Ltac f H := split; [a H|e H].
Print Ltac f.

(* Test printing of match context *)
(* Used to fail after translator removal (see bug #1070) *)

Ltac g := match goal with |- context [if ?X then _ else _ ] => case X end.
Print Ltac g.