The Coq mailing list

[Stéphane Glondu <steph AT glondu.net>]

Sean Wilson wrote:
>> Have you tried "Hint Unfold permutation." after your definition?
> 
> I was looking for a way for this to happen automatically without me having 
> to 
> explicitly name definitions. It isn't a huge burden on the user to identify 
> such terms, but I wanted to remove the need for such hints if possible. I 
> suppose another approach is to have the machine identify definitions that 
> are 
> suitable as unfold hints and automatically add them as unfold hints at the 
> point such definitions are entered into Coq. [...]

How do you want Coq to infer automatically which definition should be
added as unfold hints, and which not?

-- 
Stéphane