The Coq mailing list

["Carlos.SIMPSON" <carlos AT math.unice.fr>]

Hi. Has anybody tried using Coq to automatically generate theorems, and
say store them in a file? 

A vaguely related technical question: is there any way to 
define a Hint Extern with the null pattern i.e. ask that
it be applied to any goal regardless of the pattern of the
head term of the goal? 
I tried 
Hint myhint : myhints := Extern ? EApply mytheorem.
but this didn't work.

Finally, a stupid question: how do you define a .coqrc file
on a PC windows 98? Windows doesnt allow filenames that start with `.'.

---Carlos Simpson