The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

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.

 

> That seems to have made make happy, but is it right? 
> 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 

--