aboutsummaryrefslogtreecommitdiff
path: root/doc/Reference-Manual.tex
diff options
context:
space:
mode:
authormarche2003-11-24 13:39:29 +0000
committermarche2003-11-24 13:39:29 +0000
commit580f71e99d5f83b2fe04211cb18f763c05765fbf (patch)
treed614d62cdf66f5238b6c5fae0a654b1ad8b7b281 /doc/Reference-Manual.tex
parent8760a7f81efda41753cf7592d6c3f974df2fd947 (diff)
coqide
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8369 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'doc/Reference-Manual.tex')
-rw-r--r--doc/Reference-Manual.tex8
1 files changed, 8 insertions, 0 deletions
diff --git a/doc/Reference-Manual.tex b/doc/Reference-Manual.tex
index af404d505c..01dece65de 100644
--- a/doc/Reference-Manual.tex
+++ b/doc/Reference-Manual.tex
@@ -5,6 +5,13 @@
\usepackage{verbatim}
\usepackage{palatino}
\usepackage{url}
+% for coqide
+\ifx\pdftexversion\undefined % si on est pas en pdflatex
+ \usepackage[dvips]{graphicx}
+\else
+ \usepackage[pdftex]{graphicx}
+\fi
+
\makeatletter
@@ -51,6 +58,7 @@
\part{Practical tools}
\include{RefMan-com}% The coq commands (coqc coqtop)
\include{RefMan-uti}% utilities (gallina, do_Makefile, etc)
+\include{RefMan-ide}% Coq IDE
\include{AddRefMan-pre}%
\include{Cases.v}%