Hugo Herbelin (Jan 08 2023 at 08:01): Hugo Herbelin (Jan 08 2023 at 08:01):I realize the following (maybe) counter-intuitive behavior:
Goal 0 = 1.
let x := open_constr:(eq_sym _) in
refine x.
(* Goal 1 = 0 is on the shelf *)
Undo.
refine (eq_sym _).
(* Goal 1 = 0 is not on the shelf *)
The reason is that "future goals" are collected at typing time.
Did someone consider making evars of an Ltac/Ltac2 binding automatically future goals so as refine to be Ltac-substitutive?
Hugo Herbelin (Jan 08 2023 at 10:46):An alternative question is how to tell for an evar occurring as part of a open_constr:(...) expression if one wants it to be shelved or as a goal at some position of the non-shelved goals.
Hugo Herbelin (Jan 08 2023 at 10:57):And another related question, probably already discussed, is whether the _ below is supposed to create a goal (shelved or not):
Goal True.
let _ := open_constr:(_) in I.
I rely on the behavior that open_constr:(_) does not create future goals (ever), and do not consider this a bug. If I want it to be not shelved, I wrap the whole thing in unshelve.
Last updated: Sep 09 2024 at 05:02 UTC