The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

If you have [Definition foo := Set.] and you can't get multiple successes out of [unify foo foo] (where the second success comes from unfolding both [foo]s), which I suspect you can't, then the backtracking of unification isn't accessible from Ltac-land.

On Wed, Apr 27, 2016, 9:29 PM Jonathan Leivent <jonikelee AT gmail.com> wrote:

On 04/27/2016 05:04 AM, Enrico Tassi wrote:
> ...
> In short unification already performs some backtracking, in particular
> when constants are unfolded.  By crafting a chain of aliases (constants
> begin just another name for the same value) one can trick unification
> into trying many "canonical" solutions for the "same" problem.

If so, then there should be open_constrs X and Y such that "unify X Y"
succeeds but "exactly_once (unify X Y)" fails due to multiple
successes.  I tried a few cases involving constant unfolding, but can't
seem to get this to occur.  Can anyone else?

I'm not doubting that canonical structures can do backtracking - but it
might be "confined" backtracking, just like typeclasses backtracking is
confined to within a single invocation of typeclasses eauto, such that
one cannot backtrack back into a successful case from the outside.

-- Jonathan