blob: 899260f59a25ffa7ab54f65781d3b72166281d69 (
plain)
1
2
3
4
5
6
7
8
9
10
11
|
(* This was fixed at some time, suspectingly in PR #6328 *)
Inductive foo := F (a : forall var : Type -> Type, unit -> var unit) (_ : a = a).
Goal foo.
eexists (fun var => fun u : unit => ltac:(clear u)).
shelve.
Unshelve.
all:[ > | ].
shelve.
Fail Grab Existential Variables.
Abort.
|
