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?
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.
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
Last updated: Dec 07 2023 at 09:01 UTC