blob: 96b6d652c9b516d4d463b4ff8c36c93db6b90127 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
|
(* 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 BZ#1070) *)
Ltac g := match goal with |- context [if ?X then _ else _ ] => case X end.
Print Ltac g.
(* Test an error message (BZ#5390) *)
Lemma myid (P : Prop) : P <-> P.
Proof. split; auto. Qed.
Goal True -> (True /\ True) -> True.
Proof.
intros H.
Fail intros [H%myid ?].
Fail destruct 1 as [H%myid ?].
Abort.
(* Test that assert_succeeds only runs a tactic once *)
Ltac should_not_loop := idtac + should_not_loop.
Goal True.
assert_succeeds should_not_loop.
assert_succeeds (idtac "a" + idtac "b"). (* should only output "a" *)
Abort.
|
