aboutsummaryrefslogtreecommitdiff
path: root/doc/RefMan.txt
diff options
context:
space:
mode:
authorfilliatr2003-12-16 15:23:07 +0000
committerfilliatr2003-12-16 15:23:07 +0000
commitd418004b79b5f95898eafa0b5376d5afc30cd699 (patch)
tree96000f3e46f559eda96f6d8ea936573592eb5a1b /doc/RefMan.txt
parentd967f95e11f5daa6d3a4e3931ef735a13f9c6142 (diff)
maj Omega
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8400 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'doc/RefMan.txt')
-rw-r--r--doc/RefMan.txt2
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/RefMan.txt b/doc/RefMan.txt
index 3c3d88ba8e..75a762758f 100644
--- a/doc/RefMan.txt
+++ b/doc/RefMan.txt
@@ -42,7 +42,7 @@ MANUEL DE REFERENCE
\include{Cases.v}% CP
\include{Coercion.v}% HH
%%SUPPRIME \include{Natural.v}%
-\include{Omega.v}% JCF
+\include{Omega.v}% JCF - fait
%%Nouvelle version ROmega Pierre Cregut
%%SUPPRIME \include{Program.v}%
%% A SUPPRIMER