1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
|
From Ltac2 Require Import Ltac2 Constr.
Import Constr.Unsafe.
Goal True.
let t := open_constr:(_ :> False) in
match kind t with
| Evar e _ => Control.new_goal e > [refine 'I|]
| _ => Control.throw Not_found
end.
Show Existentials. (* Existential 1 = ?Goal : [ |- False] (shelved) *)
Abort.
Goal True.
let t := unshelve open_constr:(_ :> False) in
Control.extend [Control.shelve] (fun () => ()) [];
match kind t with
| Evar e _ => Control.new_goal e > [refine 'I|]
| _ => Control.throw Not_found
end.
Show Existentials.
Abort.
|
