aboutsummaryrefslogtreecommitdiff
path: root/doc/RecTutorial
diff options
context:
space:
mode:
authornotin2008-08-06 15:34:14 +0000
committernotin2008-08-06 15:34:14 +0000
commit2592766937df60484f15d5050e5bfe6623c83390 (patch)
treeeb5c6f7437882f4c85b7b4ca1d340644f426e02f /doc/RecTutorial
parent99ceb8c7df67a37330820e3e6fbb4a3ccab2a9a5 (diff)
Mise à jour des fichiers README et INSTALL de la doc (bug #1921) + suppression de la dépendance envers aeguill (bug #1922)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11311 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'doc/RecTutorial')
-rw-r--r--doc/RecTutorial/RecTutorial.tex24
1 files changed, 12 insertions, 12 deletions
diff --git a/doc/RecTutorial/RecTutorial.tex b/doc/RecTutorial/RecTutorial.tex
index df8bc9f105..56c4f172a3 100644
--- a/doc/RecTutorial/RecTutorial.tex
+++ b/doc/RecTutorial/RecTutorial.tex
@@ -5,24 +5,24 @@ Pierre Cast\'eran\thanks{Pierre.Casteran@labri.fr}}
\date{May 1998 --- \today}
\usepackage{multirow}
-\usepackage{aeguill}
-%\externaldocument{RefMan-gal.v}
-%\externaldocument{RefMan-ext.v}
-%\externaldocument{RefMan-tac.v}
-%\externaldocument{RefMan-oth}
-%\externaldocument{RefMan-tus.v}
-%\externaldocument{RefMan-syn.v}
-%\externaldocument{Extraction.v}
+% \usepackage{aeguill}
+% \externaldocument{RefMan-gal.v}
+% \externaldocument{RefMan-ext.v}
+% \externaldocument{RefMan-tac.v}
+% \externaldocument{RefMan-oth}
+% \externaldocument{RefMan-tus.v}
+% \externaldocument{RefMan-syn.v}
+% \externaldocument{Extraction.v}
\input{recmacros}
\input{coqartmacros}
\newcommand{\refmancite}[1]{{}}
-%\newcommand{\refmancite}[1]{\cite{coqrefman}}
-%\newcommand{\refmancite}[1]{\cite[#1] {]{coqrefman}}
+% \newcommand{\refmancite}[1]{\cite{coqrefman}}
+% \newcommand{\refmancite}[1]{\cite[#1] {]{coqrefman}}
\usepackage[latin1]{inputenc}
\usepackage[T1]{fontenc}
\usepackage{makeidx}
-%\usepackage{multind}
+% \usepackage{multind}
\usepackage{alltt}
\usepackage{verbatim}
\usepackage{amssymb}
@@ -31,7 +31,7 @@ Pierre Cast\'eran\thanks{Pierre.Casteran@labri.fr}}
\usepackage[dvips]{epsfig}
\usepackage{epic}
\usepackage{eepic}
-\usepackage{ecltree}
+% \usepackage{ecltree}
\usepackage{moreverb}
\usepackage{color}
\usepackage{pifont}