Janno (Apr 27 2023 at 09:29): Janno (Apr 27 2023 at 09:29):Why is the one remaining and focused goal in the example below also still on the shelf after Control.new_goal?
From Ltac2 Require Import Ltac2 Constr.
Import Constr.Unsafe.
Goal True.
let t := open_constr:(_ : False) in
match kind t with
| Cast t _ _ =>
match kind t with
| Evar e _ => Control.new_goal e > [refine 'I|]
| _ => ()
end
| _ => ()
end.
Show Existentials. (* Existential 1 = ?Goal : [ |- False] (shelved) *)
Having discussed this with Janno last week, it seems to us that this is an Ltac2 bug. Can anyone confirm?
Gaëtan Gilbert (May 02 2023 at 21:55):(deleted)
Last updated: Nov 29 2023 at 22:01 UTC