The Coq mailing list

[Patrick Loiseleur <Patrick.Loiseleur AT lri.fr>]

Dear Coq users,

The reference manual is now splitted in two parts :

1) Reference-manual-base.ps, 215 pp., includes the description of
Gallina, a short paragraph about each tactic and command, two chapters
about Grammar/Syntax extentions and Writing tactics.

2) Reference-Manual-addendum.ps, 75 pp., includes more detailed
explanations and examples about the following topics:
  - the extended Cases (C.Cornes)
  - the Coercions (A. Saïbi)
  - the tactic Omega (P. Crégut)
  - printing proofs in natural language (Y. Coscoy)
  - the tactic Ring (S. Boutin and P. Loiseleur)
  - the Program tactic (C. Parent)

Index, page and chapter numbers are shared by the two documents, in
order to make cross-references possible. There is also a on the ftp
server a Postscript file Reference-Manual-all.ps that contains the two
documents.

By popular demand, documentation is also available in the DVI format. 

Small changes on documentation are still possible these days, so
bug-reports and remarks are welcome. 

Best regards,

Patrick Loiseleur