The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

On 07/12/2014 12:34 PM, Matthieu Sozeau wrote:
> Le samedi 12 juillet 2014, Jonathan 
> <jonikelee AT gmail.com>
>  a écrit :
>
> > After pulling the latest trunk version, I had to fix up several things.
> >   One was trying to guess how this -R option to coqdep works if I just want
> > a single directory project.  I guessed this: -R . ""
>
> I guess the name of your package instead of "" would work just as well. The
> point of this -R is to make packages relocatable but inside your project
> you can still use unqualified imports.

OK.  If I use the name of the package, will that be needed as a prefix 
in Require commands?  In other words, if I change from -R . "" to -R . 
Foo, do I also have to change all occurrences of Require somelocalfile 
to Require Foo.somelocalfile?  Or, is the local directory still 
searched, and so no prefix is needed for local files?

> > Also, the automatic naming of hypotheses rules were switched again! I
> > guess I really need some approach that will allow me to comb through my
> > proofs to find references to automatically named hypotheses.  Although,
> > pulling changes to the naming rules is a start ;)
>
> There is an option Set Standard Proposition Elimination Names (or similar,
> Print Options will tell you) to change this behavior.
> Best,
> -- Matthieu

Could you point me to the place in the ML sources for Coq where the 
naming behavior is controlled?  I am wondering how hard it would be to 
put in that add-a-suffix scheme I proposed two weeks ago as a way to 
help find uses of automatic names in proof scripts.  I really don't want 
to depend on any automatic naming convention - it is just too hard right 
now to find all instances of usage of automatically named variables in a 
long proof script, and also too inconvenient to make sure in advance one 
doesn't use them.

-- Jonathan