unfold's arbitrary choices are unintuitive

[chaudhuri]

Consider the following:

Kind i type.
Type f i -> i.

Define p : i -> prop by
  nabla x, p (F x) := nabla x, F x = f x.

Theorem works : forall F, p F -> p F.
intros. case H1. search.

Theorem fails : forall F, p F -> p F.
intros. case H1. unfold.

The second case leads to the unprovable goal

============================
 nabla x, f n1 = f x

Currently, even with clause selectors, there is no way to get access to the second conflict-free solution that Tactics.unfold_defs actually finds, which would be:

============================
 nabla x, f x = f x

Proposal: add a (all) cookie to unfold, similar to the (keep) cookie on case, that produces a disjunct of all the conflict-free solutions instead of arbitrarily picking the first.

This issue was brought to my notice by Claudio Sacerdoti Coen.

[chaudhuri]

This now works:

Theorem works_again : forall F, p F -> p F.
intros. case H1. unfold (all). right.
  intros. search.

[ThatDaleMiller]

This behavior happens with the following (slightly) simpler theorems.

Theorem success : nabla x, p (f x). search.

Theorem failure: nabla x, p (f x). intros. unfold. abort.

[chaudhuri]

Right, but using unfold (all) with the current master branch should work. Is this not the case for you?