diff options
| author |  Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2015-07-31 17:01:17 +0200 |
|---|---|---|
| committer | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2015-07-31 17:01:17 +0200 |
| commit | ce4c3ddec6c91dc277c922aaac58395c92941710 (patch) | |
| tree | 9414d87506c0c075aed8caa53199c30bb47f2890 /doc/refman/Reference-Manual.tex | |
| parent | 505eb0f0dae9b8a6ac810070d60916b67942b305 (diff) | |
Improve the table of content of the reference manual.
Also remove AsyncProofs.tex from the list of preprocessed files, as it is
doubtful it will ever contains Coq scripts.
Diffstat (limited to 'doc/refman/Reference-Manual.tex')
| -rw-r--r-- | doc/refman/Reference-Manual.tex | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/doc/refman/Reference-Manual.tex b/doc/refman/Reference-Manual.tex index 907b30b3e..ac28e0ba0 100644 --- a/doc/refman/Reference-Manual.tex +++ b/doc/refman/Reference-Manual.tex @@ -114,16 +114,14 @@ Options A and B of the licence are {\em not} elected.} \include{Coercion.v}% \include{CanonicalStructures.v}% \include{Classes.v}% -%%SUPPRIME \include{Natural.v}% \include{Omega.v}% \include{Micromega.v} -%%SUPPRIME \include{Correctness.v}% = preuve de pgms imperatifs \include{Extraction.v}% \include{Program.v}% \include{Polynom.v}% = Ring \include{Nsatz.v}% \include{Setoid.v}% Tactique pour les setoides -\include{AsyncProofs.v}% Paral-ITP +\include{AsyncProofs}% Paral-ITP \include{Universes.v}% Universe polymorphes \include{Misc.v} %BEGIN LATEX |