The Coq mailing list

[Helmut Brandl <helmut.luis.brandl AT gmail.com>]

Thanks.

On Feb 11, 2018 15:33, "Théo Zimmermann" <theo.zimmi AT gmail.com> wrote:

Certainly!

This is Chapter 14 "The Coq Commands": https://github.com/coq/coq/blob/master/doc/refman/RefMan-com.tex

and this is Chapter 2 "Extensions of Gallina" which contains a section about "Libraries and Qualified names": https://github.com/coq/coq/blob/master/doc/refman/RefMan-ext.tex

I found these two by running "git grep COQPATH" in my local clone of the Coq repository.

Cheers,

Théo

Le dim. 11 févr. 2018 à 03:37, Helmut Brandl <helmut.luis.brandl AT gmail.com> a écrit :

Certainly. If it is just a fork of the coq repo, adding a hint to the corresponding docu file and then create a PR, then I am glad if I can help.

Can anybody give me a link to the docu file describing coq makefiles?

Cheers

Helmut

On Feb 10, 2018 8:13 AM, "Théo Zimmermann" <theo.zimmi AT gmail.com> wrote:

Is there any plan to update the reference manual. The actual behaviour of coq is very confusing if you just follow the manual. Or did I overlooked something?

Pull requests are always welcome. See https://github.com/coq/coq/blob/master/CONTRIBUTING.md. The core team of developers has so much to do that it is very important to get external contributions, especially on improving the documentation. If you don't want to do that, you can also open a new issue at https://github.com/coq/coq/issues explaining what you found confusing and suggesting how to improve it, and hopefully someone else will take it from there.

Regards,

Théo