The Coq mailing list

[Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr>]

On 17/08/2017 20:36, Robbert Krebbers wrote:
> Thanks, simple apply does not suffer from this issue, and at least
> allows me to compile my development in finite time :).
> 
> Do you have any idea what apply is doing what simple apply is not?

IANAAL (I am not an apply lawyer) but as far as my limited understanding
extends, contrarily to the generic apply, simple apply performs
unification without unfolding definitions (no delta rule).

Obviously, developers more versed in the dark art of meta-based
unification can shed more light on this, e.g. Hugo Herbelin or Matthieu
Sozeau. Also, I'd be curious to know how the new unification algorithm
implemented by the latter performs on your examples. Let's hope this is
enough to summon them in the conversation...

PMP

Attachment: signature.asc
Description: OpenPGP digital signature