The Coq mailing list

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

This is indeed a bug. Or rather was. For it is now fixed.

On 4 September 2014 15:45, Jonathan <jonikelee AT gmail.com> wrote:

On 09/04/2014 08:50 AM, Arnaud Spiwack wrote:

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?

Goal forall a b:nat, exists c:nat, c=a+b.
intros a b.
refine (ex_intro _ _ _).
all:rename a into a'. (*works without this line*)
all:shelve_unifiable.

-- Jonathan