The Coq mailing list

[Brian Aydemir <baydemir AT cis.upenn.edu>]

Hi,

I do not understand a couple of the design choices made in the FSets  
library.  Both my questions have to do with the Hints declared in  
FSetInterface.S.

[1] What is the motivation behind adding so many properties to the  
*core* automation database? For example, properties such as inter_1  
and inter_2 seem like they should to interact rather poorly with eauto.

[2] Why are the Hints hidden from the documentation generated by  
coqdoc?  The behavior of (e)auto on some finite-set goals confused me  
until I realized that there were Hints being declared.

Thank you in advance for any insights and clarification.

Cheers,
Brian