blob: 8fa9199408c873ff715e3fc4cea3210a08c1d926 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
|
(* 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.
(* Test printing of match context *)
(* Used to fail after translator removal (see bug #1070) *)
Lemma test2 : forall n:nat, forall f: nat -> bool, O = if (f n) then O else O.
Proof.
intros;match goal with |- context [if ?X then _ else _ ] => case X end;trivial.
Show Script.
Qed.
|
