diff options
Diffstat (limited to 'doc/RecTutorial')
| -rw-r--r-- | doc/RecTutorial/RecTutorial.tex | 24 |
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} |