diff options
author | 2017-06-22 13:52:07 +0200 | |
---|---|---|
committer | 2017-08-01 19:28:11 +0200 | |
commit | fc4c6c604db7bd6d973b02d29993daafeabc6f6c (patch) | |
tree | a96d0cad0c47a39c69473b98ab581f9d3992196b /doc | |
parent | 8d85f0876d28a760bca693624f98145e4ee8f331 (diff) |
Remove old doc/rt files.
Diffstat (limited to 'doc')
-rw-r--r-- | doc/Makefile.rt | 43 | ||||
-rw-r--r-- | doc/rt/RefMan-cover.tex | 45 | ||||
-rw-r--r-- | doc/rt/Tutorial-cover.tex | 47 |
3 files changed, 0 insertions, 135 deletions
diff --git a/doc/Makefile.rt b/doc/Makefile.rt deleted file mode 100644 index 6c3281346..000000000 --- a/doc/Makefile.rt +++ /dev/null @@ -1,43 +0,0 @@ -# Makefile for building Coq Technical Reports - -# if coqc,coqtop,coq-tex are not in your PATH, you need the environment -# variable COQBIN to be correctly set -# (COQTOP is autodetected) -# (some files are preprocessed using Coq and some part of the documentation -# is automatically built from the theories sources) - -# To compile documentation, you need the following tools: -# Dvi: latex (latex2e), bibtex, makeindex, dviselect (package RPM dviutils) -# Ps: dvips, psutils (ftp://ftp.dcs.ed.ac.uk/pub/ajcd/psutils.tar.gz) -# Pdf: pdflatex -# Html: -# - hevea: http://para.inria.fr/~maranget/hevea/ -# - htmlSplit: http://coq.inria.fr/~delahaye -# Rapports INRIA: dviselect, rrkit (par Michel Mauny) - -include ./Makefile - -################### -# RT -################### -# Fabrication d'un RT INRIA (utilise rrkit de Michel Mauny) -rt/Reference-Manual-RT.dvi: refman/Reference-Manual.dvi rt/RefMan-cover.tex - dviselect -i refman/Reference-Manual.dvi -o rt/RefMan-body.dvi 3: - (cd rt; $(LATEX) RefMan-cover.tex) - set a=`tail -1 refman/Reference-Manual.log`;\ - set a=expr \("$$a" : '.*(\(.*\) pages.*'\) % 2;\ - (cd rt; if $(TEST) "$$a = 0";\ - then rrkit RefMan-cover.dvi RefMan-body.dvi Reference-Manual-RT.dvi;\ - else rrkit -odd RefMan-cover.dvi RefMan-body.dvi Reference-Manual-RT.dvi;\ - fi) - -# Fabrication d'un RT INRIA (utilise rrkit de Michel Mauny) -rt/Tutorial-RT.dvi : tutorial/Tutorial.v.dvi rt/Tutorial-cover.tex - dviselect -i rt/Tutorial.v.dvi -o rt/Tutorial-body.dvi 3: - (cd rt; $(LATEX) Tutorial-cover.tex) - set a=`tail -1 tutorial/Tutorial.v.log`;\ - set a=expr \("$$a" : '.*(\(.*\) pages.*'\) % 2;\ - (cd rt; if $(TEST) "$$a = 0";\ - then rrkit Tutorial-cover.dvi Tutorial-body.dvi Tutorial-RT.dvi;\ - else rrkit -odd Tutorial-cover.dvi Tutorial-body.dvi Tutorial-RT.dvi;\ - fi) diff --git a/doc/rt/RefMan-cover.tex b/doc/rt/RefMan-cover.tex deleted file mode 100644 index ac1686c25..000000000 --- a/doc/rt/RefMan-cover.tex +++ /dev/null @@ -1,45 +0,0 @@ -\documentstyle[RRcover]{book} - % The use of the style `french' forces the french abstract to appear first. - -\RRtitle{Manuel de r\'ef\'erence du syst\`eme Coq \\ version V7.1} -\RRetitle{The Coq Proof Assistant \\ Reference Manual \\ Version 7.1 -\thanks -{This research was partly supported by ESPRIT Basic Research -Action ``Types'' and by the GDR ``Programmation'' co-financed by MRE-PRC and CNRS.} -} -\RRauthor{Bruno Barras, Samuel Boutin, Cristina Cornes, -Judica\"el Courant, Jean-Christophe Filli\^atre, Eduardo Gim\'enez, -Hugo Herbelin, G\'erard Huet, C\'esar Mu\~noz, Chetan Murthy, -Catherine Parent, Christine Paulin-Mohring, -Amokrane Sa{\"\i}bi, Benjamin Werner} -\authorhead{} -\titlehead{Coq V7.1 Reference Manual} -\RRtheme{2} -\RRprojet{Coq} -\RRNo{0123456789} -\RRdate{May 1997} -%\RRpages{} -\URRocq - -\RRresume{Coq est un syst\`eme permettant le d\'eveloppement et la -v\'erification de preuves formelles dans une logique d'ordre -sup\'erieure incluant un riche langage de d\'efinitions de fonctions. -Ce document constitue le manuel de r\'ef\'erence de la version V7.1 -qui est distribu\'ee par ftp anonyme \`a l'adresse -\url{ftp://ftp.inria.fr/INRIA/coq/}} - -\RRmotcle{Coq, Syst\`eme d'aide \`a la preuve, Preuves formelles, -Calcul des Constructions Inductives} - - -\RRabstract{Coq is a proof assistant based on a higher-order logic -allowing powerful definitions of functions. -Coq V7.1 is available by anonymous -ftp at \url{ftp://ftp.inria.fr/INRIA/coq/}} - -\RRkeyword{Coq, Proof Assistant, Formal Proofs, Calculus of Inductives -Constructions} - -\begin{document} -\makeRT -\end{document} diff --git a/doc/rt/Tutorial-cover.tex b/doc/rt/Tutorial-cover.tex deleted file mode 100644 index aefea8d42..000000000 --- a/doc/rt/Tutorial-cover.tex +++ /dev/null @@ -1,47 +0,0 @@ -\documentstyle[RRcover]{book} - % The use of the style `french' forces the french abstract to appear first. -\RRetitle{ -The Coq Proof Assistant \\ A Tutorial \\ Version 7.1 -\thanks{This research was partly supported by ESPRIT Basic Research -Action ``Types'' and by the GDR ``Programmation'' co-financed by MRE-PRC and CNRS.} -} -\RRtitle{Coq \\ Une introduction \\ V7.1 } -\RRauthor{G\'erard Huet, Gilles Kahn and Christine Paulin-Mohring} -\RRtheme{2} -\RRprojet{{Coq -\\[15pt] -{INRIA Rocquencourt} -{\hskip -5.25pt} -~~{\bf ---}~~ - \def\thefootnote{\arabic{footnote}\hss} -{CNRS - ENS Lyon} -\footnote[1]{LIP URA 1398 du CNRS, -46 All\'ee d'Italie, 69364 Lyon CEDEX 07, France.} -{\hskip -14pt}}} - -%\RRNo{0123456789} -\RRNo{0204} -\RRdate{Ao\^ut 1997} - -\URRocq -\RRresume{Coq est un syst\`eme permettant le d\'eveloppement et la -v\'erification de preuves formelles dans une logique d'ordre -sup\'erieure incluant un riche langage de d\'efinitions de fonctions. -Ce document constitue une introduction pratique \`a l'utilisation de -la version V7.1 qui est distribu\'ee par ftp anonyme \`a l'adresse -\url{ftp://ftp.inria.fr/INRIA/coq/}} - -\RRmotcle{Coq, Syst\`eme d'aide \`a la preuve, Preuves formelles, Calcul -des Constructions Inductives} - -\RRabstract{Coq is a proof assistant based on a higher-order logic -allowing powerful definitions of functions. This document is a -tutorial for the version V7.1 of Coq. This version is available by -anonymous ftp at \url{ftp://ftp.inria.fr/INRIA/coq/}} - -\RRkeyword{Coq, Proof Assistant, Formal Proofs, Calculus of Inductives -Constructions} - -\begin{document} -\makeRT -\end{document} |