Stream: Coq devs & plugin devs

Topic: Substitutivity of refine


view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Jason Gross (Jan 08 2023 at 17:07):

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: Mar 28 2024 at 22:01 UTC