The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

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).

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?

If so, an idiom like this forms:

  refine (...); shelve_unifiable. (*produce some evars and shelve their 
goals*)
  ... (*work in main goal's consequent - finally determine that case 
analysis of some hyp is needed*)
  Unshelve. (*bring the dependent evar goals back in focus*)
  all:case ...; intros. (*case analyze similarly across goal and all 
its dependent goals*)

But, all:shelve_unifiable doesn't do anything following that sequence of 
tactics, because the dependent evar goals have been modified.

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.

-- Jonathan