1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
|
Require Import Ltac2.Ltac2.
(* exact0 at the time of the bug, with eexact part removed for simplicity *)
Ltac2 exact0 c :=
Control.enter (fun _ =>
Control.with_holes c (fun c => Control.refine (fun _ => c))).
Ltac2 Eval
let x := constr:(0) in
Constr.pretype preterm:($x).
(* (* uncaught Not_found *) *)
Ltac2 Eval
let x := constr:(0) in
Constr.pretype preterm:(ltac2:(let y () := x in exact0 y)).
(* (* anomaly unbound variable x *) *)
Notation "[ x ]" := ltac2:(exact0 (fun () => Constr.pretype x)).
Check ltac2:(let y := constr:(0) in exact0 (fun () => open_constr:([ $y ]))).
|
