blob: 489fa638e455a53df9d0913b8fb4b46f9ed04a30 (
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
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
|
Require Import Ltac2.Ltac2.
Import Ltac2.Notations.
(** Test calls to Ltac1 from Ltac2 *)
Ltac2 foo () := ltac1:(discriminate).
Goal true = false -> False.
Proof.
foo ().
Qed.
Goal true = false -> false = true.
Proof.
intros H; ltac1:(match goal with [ H : ?P |- _ ] => rewrite H end); reflexivity.
Qed.
Goal true = false -> false = true.
Proof.
intros H; ltac1:(rewrite H); reflexivity.
Abort.
(** Variables do not cross the compatibility layer boundary. *)
Fail Ltac2 bar nay := ltac1:(discriminate nay).
Fail Ltac2 pose1 (v : constr) :=
ltac1:(pose $v).
(** Test calls to Ltac2 from Ltac1 *)
Set Default Proof Mode "Classic".
Ltac foo := ltac2:(foo ()).
Goal true = false -> False.
Proof.
ltac2:(foo ()).
Qed.
Goal true = false -> False.
Proof.
foo.
Qed.
(** Variables do not cross the compatibility layer boundary. *)
Fail Ltac bar x := ltac2:(foo x).
Ltac mytac tac := idtac "wow".
Goal True.
Proof.
(** Fails because quotation is evaluated eagerly *)
Fail mytac ltac2:(fail).
(** One has to thunk thanks to the idtac trick *)
let t := idtac; ltac2:(fail) in mytac t.
constructor.
Qed.
|
