The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

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