aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/Reference-Manual.tex
diff options
context:
space:
mode:
authorGravatar courant <courant@85f007b7-540e-0410-9357-904b9bb8a0f7>2001-04-25 12:04:09 +0000
committerGravatar courant <courant@85f007b7-540e-0410-9357-904b9bb8a0f7>2001-04-25 12:04:09 +0000
commit31fe4b0ab21b606712383448b21ed9b53d55f3b2 (patch)
tree703e0fcded5c95e636e140bf53be4c8555fb165b /doc/Reference-Manual.tex
parent342ab1e68c5941d1d746c8fafc557934cece2ed0 (diff)
Ajout de \begin{coq_eval} Reset Initial. \end{coq_eval} pour remettre les
grammaires de Coq dans un etat coherent. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8208 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 516a3f9d9..1d324b786 100644
--- a/doc/Reference-Manual.tex
+++ b/doc/Reference-Manual.tex
@@ -7,7 +7,7 @@
\makeatletter
-%\includeonly{Polynom.v}
+%\includeonly{RefMan-syn.v}
\input{./macros.tex}% extension .tex pour htmlgen
\input{./title.tex}% extension .tex pour htmlgen