aboutsummaryrefslogtreecommitdiff
path: root/doc/RefMan.txt
diff options
context:
space:
mode:
Diffstat (limited to 'doc/RefMan.txt')
-rw-r--r--doc/RefMan.txt4
1 files changed, 2 insertions, 2 deletions
diff --git a/doc/RefMan.txt b/doc/RefMan.txt
index 44422c792e..446ad12848 100644
--- a/doc/RefMan.txt
+++ b/doc/RefMan.txt
@@ -13,7 +13,7 @@ MANUEL DE REFERENCE
\include{RefMan-gal.v}% Gallina BB
\include{RefMan-ext.v}% Gallina extensions HH -fait
\include{RefMan-lib.v}% The coq library BB
-\include{RefMan-cic.v}% The Calculus of Constructions CP
+\include{RefMan-cic.v}% The Calculus of Constructions CP -fait
\include{RefMan-modr}% The module system Jacek
@@ -39,7 +39,7 @@ MANUEL DE REFERENCE
\include{AddRefMan-pre}% CP
-\include{Cases.v}% CP
+\include{Cases.v}% CP -fait
\include{Coercion.v}% HH -fait
%%SUPPRIME \include{Natural.v}%
\include{Omega.v}% JCF - fait