Why is the one remaining and focused goal in the example below also still on the shelf after
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?
Last updated: Nov 29 2023 at 22:01 UTC