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
|
Require Import Ltac2.Ltac2.
(* Preterms are not terms *)
Fail Notation "[ x ]" := $x.
Section Foo.
Notation "[ x ]" := ltac2:(Control.refine (fun _ => Constr.pretype x)).
Goal [ True ].
Proof.
constructor.
Qed.
End Foo.
Section Bar.
(* Have fun with context capture *)
Notation "[ x ]" := ltac2:(
let c () := Constr.pretype x in
refine constr:(forall n : nat, n = ltac2:(Notations.exact0 true c))
).
Goal forall n : nat, [ n ].
Proof.
reflexivity.
Qed.
(* This fails currently, which is arguably a bug *)
Fail Goal [ n ].
End Bar.
|
