aboutsummaryrefslogtreecommitdiff
path: root/doc/Reference-Manual.tex
diff options
context:
space:
mode:
authorcoq2003-12-11 19:42:29 +0000
committercoq2003-12-11 19:42:29 +0000
commitc4f85702f27d484b3cf8a09627c5cd5bd3ff2b6e (patch)
tree2edb118e615117d8bb74b4b7cbecfe0d8f7505d1 /doc/Reference-Manual.tex
parentad91264affa3a471f1656f2533d9ca75628f37e0 (diff)
Mis-a-jour modules, ajout de Import et Export
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8383 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'doc/Reference-Manual.tex')
-rw-r--r--doc/Reference-Manual.tex2
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/Reference-Manual.tex b/doc/Reference-Manual.tex
index f272a04f6d..8eb7f3eb08 100644
--- a/doc/Reference-Manual.tex
+++ b/doc/Reference-Manual.tex
@@ -17,7 +17,7 @@
\fi
-%\includeonly{RefMan-cic.v,RefMan-ext.v}
+%\includeonly{RefMan-cic.v,RefMan-ext.v,RefMan-modr}
\input{./version.tex}
\input{./macros.tex}% extension .tex pour htmlgen