aboutsummaryrefslogtreecommitdiff
path: root/doc
diff options
context:
space:
mode:
authormohring2003-12-03 10:46:34 +0000
committermohring2003-12-03 10:46:34 +0000
commit39cfc84722b167504b86198a101a1b4c70288ced (patch)
tree54f0080b9de5bba62e95c1fc11d377e14eea70c2 /doc
parent7ff1810bafc981ee774c431e1c7f5b99d2700cd7 (diff)
*** empty log message ***
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8376 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'doc')
-rw-r--r--doc/RefMan.txt4
1 files changed, 2 insertions, 2 deletions
diff --git a/doc/RefMan.txt b/doc/RefMan.txt
index ccaa488b83..752462670e 100644
--- a/doc/RefMan.txt
+++ b/doc/RefMan.txt
@@ -35,7 +35,7 @@ MANUEL DE REFERENCE
\include{RefMan-com}% The coq commands (coqc coqtop) HH
%%ajouter nouvelles options -v7 -translate au document de passage
\include{RefMan-uti}% utilities (gallina, do_Makefile, etc) JCF
-%%ajouter coqide Benjamin M
+\include{RefMan-ide}%CoqIde CM
\include{AddRefMan-pre}% CP
@@ -48,7 +48,7 @@ MANUEL DE REFERENCE
%% A SUPPRIMER
%% \include{Correctness.v}% = preuve de pgms imperatifs
\include{Extraction.v}% Pierre L
-\include{Polynom.v}% = Ring JCF
+\include{Polynom.v}% = Ring Julien N
\include{Setoid.v}% Tactique pour les setoides Clement
\addtocontents{sh}{ENDADDENDUM=\thepage}