From bb6e15cb3d64f2902f98d01b8fe12948a7191095 Mon Sep 17 00:00:00 2001
From: coq
Date: Tue, 30 Dec 2003 09:53:31 +0000
Subject: modif generales claude

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8455 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 doc/Reference-Manual.tex | 18 +++++++++++-------
 1 file changed, 11 insertions(+), 7 deletions(-)

(limited to 'doc/Reference-Manual.tex')

diff --git a/doc/Reference-Manual.tex b/doc/Reference-Manual.tex
index 853189c6fd..4d876f71ed 100644
--- a/doc/Reference-Manual.tex
+++ b/doc/Reference-Manual.tex
@@ -79,13 +79,6 @@
 \nocite{*}
 \bibliographystyle{plain}
 \bibliography{biblio}
-%BEGIN LATEX
-\RefManCutCommand{psselect -q -p-$ENDREFMAN,$BEGINBIBLIO- Reference-Manual.ps Reference-Manual-base.ps}
-\RefManCutCommand{psselect -q -p$BEGINADDENDUM-$ENDADDENDUM Reference-Manual.ps Reference-Manual-addendum.ps}
-\RefManCutCommand{dviselect -i Reference-Manual.dvi -o Reference-Manual-base.dvi 1-$ENDREFMAN $BEGINBIBLIO-}
-\RefManCutCommand{dviselect -i Reference-Manual.dvi -o Reference-Manual-addendum.dvi $BEGINADDENDUM-$ENDADDENDUM}
-\RefManCutClose
-%END LATEX
 
 \printindex
 
@@ -95,6 +88,17 @@
 
 \printindex[error]
 
+\listoffigures
+%\listoftables
+
+%BEGIN LATEX
+\RefManCutCommand{psselect -q -p-$ENDREFMAN,$BEGINBIBLIO- Reference-Manual.ps Reference-Manual-base.ps}
+\RefManCutCommand{psselect -q -p$BEGINADDENDUM-$ENDADDENDUM Reference-Manual.ps Reference-Manual-addendum.ps}
+\RefManCutCommand{dviselect -i Reference-Manual.dvi -o Reference-Manual-base.dvi 1-$ENDREFMAN $BEGINBIBLIO-}
+\RefManCutCommand{dviselect -i Reference-Manual.dvi -o Reference-Manual-addendum.dvi $BEGINADDENDUM-$ENDADDENDUM}
+\RefManCutClose
+%END LATEX
+
 \end{document}
 
 
-- 
cgit v1.2.3

