The Coq mailing list

[Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>]

When using all:shelve_unifiable, is it always supposed to shelve all focused goals that correspond to evars in other focused goals?

It seems like all:shelve_unifiable doesn't shelve a dependent evar goal if it was modified (as by renaming a hypothesis within it, or case analyzing a hypothesis within it, or adding a new hypothesis to it, etc.), even though it still corresponds to an evar in other focused goal(s).

Said like that, it sounds like a bug. Can you provide me with a concrete example of this behaviour?
 

I am trying to understand what the expected usage of refine-produced evars and all:shelve_unifiable is supposed to be.  I noticed that, when doing case analysis in a goal, it helps if that same case analysis is done simultaneously in its dependent evar goals (this can probably be generalized to: the same antecedent-modifying tactics should be done simultaneously across a goal and all its dependent evar goals).  I am guessing that this is the intended expected usage.  Is that correct?

The expected usage is whatever you find convenient, really.
 

Also: if this idiom is intended, it might be helpful if there was an Unshelve_unifiable command to use above so as not to unshelve goals unrelated to the current focused goals.

Sounds like a good idea. I'll try to do that.