Remove LaTeX refman, now that migration to Sphinx is complete

14 files changed, 12 insertions, 2068 deletions

diff --git a/.gitignore b/.gitignore
index 267534365..25c0996cb 100644
--- a/.gitignore
+++ b/.gitignore
@@ -96,21 +96,6 @@ doc/faq/axioms.eps
 doc/faq/axioms.eps_t
 doc/faq/axioms.pdf_t
 doc/faq/axioms.png
-doc/refman/.csdp.cache
-doc/refman/trace
-doc/refman/Reference-Manual.ps
-doc/refman/Reference-Manual.html
-doc/refman/Reference-Manual.out
-doc/refman/Reference-Manual.sh
-doc/refman/cover.html
-doc/refman/styles.hva
-doc/refman/coqide-queries.eps
-doc/refman/coqide.eps
-doc/refman/euclid.ml
-doc/refman/euclid.mli
-doc/refman/heapsort.ml
-doc/refman/heapsort.mli
-doc/refman/html/
 doc/stdlib/Library.out
 doc/stdlib/Library.ps
 doc/stdlib/Library.coqdoc.tex
@@ -177,9 +162,6 @@ dev/myinclude
 
 # coqide generated files (when testing)
 *.crashcoqide
-/doc/refman/Reference-Manual.hoptind
-/doc/refman/Reference-Manual.optidx
-/doc/refman/Reference-Manual.optind
 
 user-contrib
 .*.sw*
diff --git a/INSTALL.doc b/INSTALL.doc
index b71115bfa..b424f9f64 100644
--- a/INSTALL.doc
+++ b/INSTALL.doc
@@ -66,8 +66,8 @@ Alternatively, you can use some specific targets:
    make doc-html
         to produce all html documents
 
-   make refman
-        to produce all formats of the reference manual
+   make sphinx
+        to produce the HTML version of the reference manual
 
    make tutorial
         to produce all formats of the tutorial
diff --git a/Makefile b/Makefile
index c31534f36..793afb661 100644
--- a/Makefile
+++ b/Makefile
@@ -235,11 +235,8 @@ docclean:
 	  doc/stdlib/*Library.coqdoc.tex doc/stdlib/library.files \
 	  doc/stdlib/library.files.ls doc/stdlib/FullLibrary.tex
 	rm -f doc/*/*.ps doc/*/*.pdf doc/*/*.eps doc/*/*.pdf_t doc/*/*.eps_t
-	rm -rf doc/refman/html doc/stdlib/html doc/tutorial/tutorial.v.html
-	rm -f doc/refman/euclid.ml doc/refman/euclid.mli
-	rm -f doc/refman/heapsort.ml doc/refman/heapsort.mli
+	rm -rf doc/stdlib/html doc/tutorial/tutorial.v.html
 	rm -f doc/common/version.tex
-	rm -f doc/refman/styles.hva doc/refman/cover.html doc/refman/Reference-Manual.html
 	rm -f doc/coq.tex
 	rm -rf doc/sphinx/_build
 
diff --git a/Makefile.doc b/Makefile.doc
index dc2b9f55d..ce31c5fcb 100644
--- a/Makefile.doc
+++ b/Makefile.doc
@@ -56,29 +56,14 @@ ALLSPHINXOPTS= -d $(SPHINXBUILDDIR)/doctrees $(SPHINXOPTS)
 
 DOCCOMMON:=doc/common/version.tex doc/common/title.tex doc/common/macros.tex
 
-REFMANCOQTEXFILES:=$(addprefix doc/refman/, )
-
-REFMANTEXFILES:=$(addprefix doc/refman/, \
-  headers.sty Reference-Manual.tex) \
-  $(REFMANCOQTEXFILES) \
-
-REFMANEPSFILES:=doc/refman/coqide.eps doc/refman/coqide-queries.eps
-
-REFMANFILES:=$(REFMANTEXFILES) $(DOCCOMMON) $(REFMANEPSFILES) doc/refman/biblio.bib
-
-REFMANPNGFILES:=$(REFMANEPSFILES:.eps=.png)
-
-
 ######################################################################
 ### General rules
 ######################################################################
 
-.PHONY: doc sphinxdoc-html doc-pdf doc-ps refman refman-quick tutorial
-.PHONY: stdlib full-stdlib rectutorial refman-html-dir
+.PHONY: doc sphinxdoc-html doc-pdf doc-ps tutorial
+.PHONY: stdlib full-stdlib rectutorial
 
-INDEXURLS:=doc/refman/html/index_urls.txt
-
-doc: sphinx refman tutorial rectutorial stdlib $(INDEXURLS)
+doc: sphinx tutorial rectutorial stdlib
 
 sphinx: coq
 	$(SHOW)'SPHINXBUILD doc/sphinx'
@@ -87,20 +72,17 @@ sphinx: coq
 	@echo "Build finished. The HTML pages are in $(SPHINXBUILDDIR)/html."
 
 doc-html:\
-  doc/tutorial/Tutorial.v.html doc/refman/html/index.html \
+  doc/tutorial/Tutorial.v.html \
   doc/stdlib/html/index.html doc/RecTutorial/RecTutorial.html
 
 doc-pdf:\
-  doc/tutorial/Tutorial.v.pdf doc/refman/Reference-Manual.pdf \
+  doc/tutorial/Tutorial.v.pdf \
   doc/stdlib/Library.pdf doc/RecTutorial/RecTutorial.pdf
 
 doc-ps:\
-  doc/tutorial/Tutorial.v.ps doc/refman/Reference-Manual.ps \
+  doc/tutorial/Tutorial.v.ps \
   doc/stdlib/Library.ps doc/RecTutorial/RecTutorial.ps
 
-refman: \
-  doc/refman/html/index.html doc/refman/Reference-Manual.ps doc/refman/Reference-Manual.pdf
-
 tutorial: \
   doc/tutorial/Tutorial.v.html doc/tutorial/Tutorial.v.ps doc/tutorial/Tutorial.v.pdf
 
@@ -159,82 +141,6 @@ doc/common/version.tex: config/Makefile
 	printf '\\newcommand{\\coqversion}{$(VERSION)}' > doc/common/version.tex
 
 ######################################################################
-# Reference Manual
-######################################################################
-
-
-### Reference Manual (printable format)
-
-# The second LATEX compilation is necessary otherwise the pages of the index
-# are not correct (don't know why...) - BB
-doc/refman/Reference-Manual.dvi: $(REFMANFILES) doc/refman/Reference-Manual.tex
-	@(cd doc/refman;\
-	$(LATEX) -interaction=batchmode Reference-Manual;\
-	$(BIBTEX) -terse Reference-Manual $(HIDEBIBTEXINFO);\
-	$(LATEX) -interaction=batchmode Reference-Manual > /dev/null;\
-	$(MAKEINDEX) -q Reference-Manual;\
-	$(SHOWMAKEINDEXERROR) Reference-Manual.ilg;\
-	$(MAKEINDEX) -q Reference-Manual.tacidx -o Reference-Manual.tacind;\
-	$(SHOWMAKEINDEXERROR) Reference-Manual.ilg;\
-	$(MAKEINDEX) -q Reference-Manual.comidx -o Reference-Manual.comind;\
-	$(SHOWMAKEINDEXERROR) Reference-Manual.ilg;\
-	$(MAKEINDEX) -q Reference-Manual.optidx -o Reference-Manual.optind;\
-	$(SHOWMAKEINDEXERROR) Reference-Manual.ilg;\
-	$(MAKEINDEX) -q Reference-Manual.erridx -o Reference-Manual.errind;\
-	$(SHOWMAKEINDEXERROR) Reference-Manual.ilg;\
-	$(LATEX) -interaction=batchmode Reference-Manual > /dev/null;\
-	$(LATEX) -interaction=batchmode Reference-Manual > /dev/null;\
-	../tools/show_latex_messages -no-overfull Reference-Manual.log)
-
-doc/refman/Reference-Manual.pdf: doc/refman/Reference-Manual.dvi $(REFMANPNGFILES)
-	(cd doc/refman;\
-	$(PDFLATEX) -interaction=batchmode Reference-Manual.tex;\
-	../tools/show_latex_messages -no-overfull Reference-Manual.log)
-
-### Reference Manual (browsable format)
-
-doc/refman/Reference-Manual.html: doc/refman/styles.hva doc/refman/headers.hva doc/refman/Reference-Manual.dvi # to ensure bbl file
-	(cd doc/refman; BIBINPUTS=.: $(HEVEA) $(HEVEAOPTS) ./styles.hva ./Reference-Manual.tex)
-
-doc/refman/cover.html: doc/common/styles/html/$(HTMLSTYLE)/cover.html
-	sed -e "s/COQVERSION/$(VERSION)/g" $< > $@
-
-doc/refman/styles.hva: doc/common/styles/html/$(HTMLSTYLE)/styles.hva
-	$(INSTALLLIB) $< doc/refman
-
-INDEXES:= doc/refman/html/command-index.html doc/refman/html/tactic-index.html
-
-refman-html-dir $(INDEXES): doc/refman/html/index.html ;
-
-doc/refman/html/index.html: doc/refman/Reference-Manual.html $(REFMANPNGFILES) \
-	       doc/refman/cover.html doc/refman/styles.hva doc/refman/index.html
-	- rm -rf doc/refman/html
-	$(MKDIR) doc/refman/html
-	$(INSTALLLIB) $(REFMANPNGFILES) doc/refman/html
-	(cd doc/refman/html; $(HACHA) -nolinks -tocbis -o toc.html ../styles.hva ../Reference-Manual.html)
-	$(INSTALLLIB) doc/refman/cover.html doc/refman/html/index.html
-	@touch $(INDEXES)
-	(cd doc/common/styles/html/$(HTMLSTYLE);\
-		for f in `find . -name \*.css`; do \
-			$(MKDIR) $$(dirname ../../../../refman/html/$$f);\
-			$(INSTALLLIB) $$f ../../../../refman/html/$$f;\
-		done)
-
-refman-quick:
-	(cd doc/refman;\
-	$(PDFLATEX) -interaction=batchmode Reference-Manual.tex;\
-	../tools/show_latex_messages -no-overfull Reference-Manual.log && \
-	$(HEVEA) $(HEVEAOPTS) ./Reference-Manual.tex)
-
-######################################################################
-# Index file for CoqIDE
-######################################################################
-
-$(INDEXURLS): $(INDEXES)
-	cat $< | grep li-indexenv | grep href= | sed -e 's@.*>\([^<]*\)</span>.*, <a href="\([^"]*\)">.*@\1,\2@' > $@
-
-
-######################################################################
 # Tutorial
 ######################################################################
 
@@ -359,30 +265,20 @@ install-doc-meta:
 	$(INSTALLLIB) doc/LICENSE $(FULLDOCDIR)/LICENSE.doc
 
 install-doc-html: 
-	$(MKDIR) $(addprefix $(FULLDOCDIR)/html/, refman stdlib)
-	(for f in `cd doc/refman/html; find . -type f`; do \
-		$(MKDIR) $$(dirname $(FULLDOCDIR)/html/refman/$$f);\
-		$(INSTALLLIB) doc/refman/html/$$f $(FULLDOCDIR)/html/refman/$$f;\
-	done)
+	$(MKDIR) $(FULLDOCDIR)/html/stdlib
 	$(INSTALLLIB) doc/stdlib/html/* $(FULLDOCDIR)/html/stdlib
 	$(INSTALLLIB) doc/RecTutorial/RecTutorial.html $(FULLDOCDIR)/html/RecTutorial.html
 	$(INSTALLLIB) doc/tutorial/Tutorial.v.html $(FULLDOCDIR)/html/Tutorial.html
 
 install-doc-printable: 
 	$(MKDIR) $(FULLDOCDIR)/ps $(FULLDOCDIR)/pdf
-	$(INSTALLLIB) doc/refman/Reference-Manual.pdf \
-		doc/stdlib/Library.pdf $(FULLDOCDIR)/pdf
-	$(INSTALLLIB) doc/refman/Reference-Manual.ps \
-		doc/stdlib/Library.ps $(FULLDOCDIR)/ps
+	$(INSTALLLIB) doc/stdlib/Library.pdf $(FULLDOCDIR)/pdf
+	$(INSTALLLIB) doc/stdlib/Library.ps $(FULLDOCDIR)/ps
 	$(INSTALLLIB) doc/tutorial/Tutorial.v.pdf $(FULLDOCDIR)/pdf/Tutorial.pdf
 	$(INSTALLLIB) doc/RecTutorial/RecTutorial.pdf $(FULLDOCDIR)/pdf/RecTutorial.pdf
 	$(INSTALLLIB) doc/tutorial/Tutorial.v.ps $(FULLDOCDIR)/ps/Tutorial.ps
 	$(INSTALLLIB) doc/RecTutorial/RecTutorial.ps $(FULLDOCDIR)/ps/RecTutorial.ps
 
-install-doc-index-urls:
-	$(MKDIR) $(FULLDATADIR)
-	$(INSTALLLIB) $(INDEXURLS) $(FULLDATADIR)
-
 install-doc-sphinx:
 	$(MKDIR) $(FULLDOCDIR)/sphinx
 	(for f in `cd doc/sphinx/_build; find . -type f`; do \
@@ -467,13 +363,6 @@ $(OCAMLDOCDIR)/%.pdf: $(OCAMLDOCDIR)/%.tex
 	$(HIDE)(cd $(OCAMLDOCDIR) ; pdflatex -interaction=batchmode $*.tex && pdflatex -interaction=batchmode $*.tex)
 	$(HIDE)(cd doc/tools/; ./show_latex_messages -no-overfull ../../$(OCAMLDOCDIR)/$*.log)
 
-###########################################################################
-# local web server
-###########################################################################
-
-serve-refman-8080: refman
-	cd doc/refman/html; python3 -m http.server 8080
-
 # For emacs:
 # Local Variables:
 # mode: makefile
diff --git a/doc/refman/AddRefMan-pre.tex b/doc/refman/AddRefMan-pre.tex
deleted file mode 100644
index 856a823de..000000000
--- a/doc/refman/AddRefMan-pre.tex
+++ /dev/null
@@ -1,63 +0,0 @@
-%\coverpage{Addendum to the Reference Manual}{\ }
-%\addcontentsline{toc}{part}{Additional documentation}
-%BEGIN LATEX
-\setheaders{Presentation of the Addendum}
-%END LATEX
-\chapter*{Presentation of the Addendum}
-%HEVEA\cutname{addendum.html}
-
-Here you will find several pieces of additional documentation for the
-\Coq\ Reference Manual. Each of this chapters is concentrated on a
-particular topic, that should interest only a fraction of the \Coq\
-users: that's the reason why they are apart from the Reference
-Manual.
-
-\begin{description}
-
-\item[Extended pattern-matching] This chapter details the use of
-  generalized pattern-matching. It is contributed by Cristina Cornes
-  and Hugo Herbelin.
-
-\item[Implicit coercions] This chapter details the use of the coercion
-  mechanism.  It is contributed by Amokrane Saïbi.
-
-%\item[Proof of imperative programs] This chapter explains how to
-%  prove properties of annotated programs with imperative features.
-%  It is contributed by Jean-Christophe Filliâtre
-
-\item[Program extraction] This chapter explains how to extract in practice ML
-  files from $\FW$ terms.   It is contributed by Jean-Christophe
-  Filliâtre and Pierre Letouzey.
-
-\item[Program] This chapter explains the use of the \texttt{Program}
-  vernacular which allows the development of certified
-  programs in \Coq. It is contributed by Matthieu Sozeau and replaces
-  the previous \texttt{Program} tactic by Catherine Parent.
-
-%\item[Natural] This chapter is due to Yann Coscoy. It is the user
-%  manual of the tools he wrote for printing proofs in natural
-%  language. At this time, French and English languages are supported.
-
-\item[omega] \texttt{omega}, written by Pierre Crégut, solves a whole
-  class of arithmetic problems.
-
-\item[The {\tt ring} tactic] This is a tactic to do AC rewriting. This
-  chapter explains how to use it and how it works.
-  The chapter is contributed by Patrick Loiseleur.
-
-\item[The {\tt Setoid\_replace} tactic] This is a
-  tactic to do rewriting on types equipped with specific (only partially
-  substitutive) equality. The chapter is contributed by Clément Renard.
-
-\item[Calling external provers] This chapter describes several tactics
-  which call external provers.
-
-\end{description}
-
-\atableofcontents
-
-
-%%% Local Variables: 
-%%% mode: latex
-%%% TeX-master: "Reference-Manual"
-%%% End: 
diff --git a/doc/refman/Reference-Manual.tex b/doc/refman/Reference-Manual.tex
deleted file mode 100644
index ba4018d77..000000000
--- a/doc/refman/Reference-Manual.tex
+++ /dev/null
@@ -1,134 +0,0 @@
-%\RequirePackage{ifpdf}
-%\ifpdf
-%  \documentclass[11pt,a4paper,pdftex]{book}
-%\else
-  \documentclass[11pt,a4paper]{book}
-%\fi
-
-\usepackage[utf8]{inputenc}
-\usepackage[T1]{fontenc}
-\usepackage{textcomp}
-\usepackage{times}
-\usepackage{url}
-\usepackage{verbatim}
-\usepackage{amsmath}
-\usepackage{amssymb}
-\usepackage{alltt}
-\usepackage{hevea}
-\usepackage{ifpdf}
-\usepackage[headings]{fullpage}
-\usepackage{headers} % in this directory
-\usepackage{multicol}
-\usepackage{xspace}
-\usepackage{pmboxdraw}
-\usepackage{float}
-\usepackage{color}
-  \definecolor{dkblue}{rgb}{0,0.1,0.5}
-  \definecolor{lightblue}{rgb}{0,0.5,0.5}
-  \definecolor{dkgreen}{rgb}{0,0.4,0}
-  \definecolor{dk2green}{rgb}{0.4,0,0}
-  \definecolor{dkviolet}{rgb}{0.6,0,0.8}
-  \definecolor{dkpink}{rgb}{0.2,0,0.6}
-\usepackage{listings}
-  \def\lstlanguagefiles{coq-listing.tex}
-\usepackage{tabularx}
-\usepackage{array,longtable}
-
-\floatstyle{boxed} 
-\restylefloat{figure}
-
-% for coqide
-\ifpdf   % si on est pas en pdflatex
-  \usepackage[pdftex]{graphicx}
-\else
-  \usepackage[dvips]{graphicx}
-\fi
-
-
-%\includeonly{Setoid}
-
-\input{../common/version.tex}
-\input{../common/macros.tex}% extension .tex pour htmlgen
-\input{../common/title.tex}% extension .tex pour htmlgen
-%\input{headers}
-
-\usepackage[linktocpage,colorlinks,bookmarks=true,bookmarksnumbered=true]{hyperref}
-% The manual advises to load hyperref package last to be able to redefine
-% necessary commands.
-% The above should work for both latex and pdflatex. Even if PDF is produced
-% through DVI and PS using dvips and ps2pdf, hyperlinks should still work.
-% linktocpage option makes page numbers, not section names, to be links in
-% the table of contents.
-% colorlinks option colors the links instead of using boxes.
-
-% The command \tocnumber was added to HEVEA in version 1.06-6.
-% It instructs HEVEA to put chapter numbers into the table of
-% content entries. The table of content is produced by HACHA using
-% the options -tocbis -o toc.html. HEVEA produces a warning when
-% a command is not recognized, so versions earlier than 1.06-6 can
-% still be used.
-%HEVEA\tocnumber
-
-\begin{document}
-%BEGIN LATEX
-\sloppy\hbadness=5000
-%END LATEX
-
-%BEGIN LATEX
-\coverpage{Reference Manual}
-{The Coq Development Team}
-{This material may be distributed only subject to the terms and
-conditions set forth in the Open Publication License, v1.0 or later
-(the latest version is presently available at
-\url{http://www.opencontent.org/openpub}).
-Options A and B of the licence are {\em not} elected.}
-%END LATEX
-
-%\defaultheaders
-
-%BEGIN LATEX
-\tableofcontents
-%END LATEX
-
-\part{The language}
-%BEGIN LATEX
-\defaultheaders
-%END LATEX
-
-
-\part{The proof engine}
-\include{RefMan-ltac.v}% Writing tactics
-
-\lstset{language=SSR}
-\lstset{moredelim=[is][]{|*}{*|}}
-\lstset{moredelim=*[is][\itshape\rmfamily]{/*}{*/}}
-
-%BEGIN LATEX
-\RefManCutCommand{BEGINADDENDUM=\thepage}
-%END LATEX
-\part{Addendum to the Reference Manual}
-\include{AddRefMan-pre}%
-%BEGIN LATEX
-\RefManCutCommand{ENDADDENDUM=\thepage}
-%END LATEX
-\nocite{*}
-\bibliographystyle{plain}
-\bibliography{biblio}
-\cutname{biblio.html}
-
-\printrefmanindex{default}{Global Index}{general-index.html}
-\printrefmanindex{tactic}{Tactics Index}{tactic-index.html}
-\printrefmanindex{command}{Vernacular Commands Index}{command-index.html}
-\printrefmanindex{option}{Vernacular Options Index}{option-index.html}
-\printrefmanindex{error}{Index of Error Messages}{error-index.html}
-
-%BEGIN LATEX
-\cleardoublepage
-\phantomsection
-\addcontentsline{toc}{chapter}{\listfigurename}
-\listoffigures
-%END LATEX
-
-\end{document}
-
-
diff --git a/doc/refman/biblio.bib b/doc/refman/biblio.bib
deleted file mode 100644
index e69725838..000000000
--- a/doc/refman/biblio.bib
+++ /dev/null
@@ -1,1397 +0,0 @@
-@String{jfp   = "Journal of Functional Programming"}
-@String{lncs  = "Lecture Notes in Computer Science"}
-@String{lnai  = "Lecture Notes in Artificial Intelligence"}
-@String{SV    = "{Sprin-ger-Verlag}"}
-
-@InProceedings{Aud91,
-  author      = {Ph. Audebaud},
-  booktitle   = {Proceedings of the sixth Conf. on Logic in Computer Science.},
-  publisher   = {IEEE},
-  title       = {Partial {Objects} in the {Calculus of Constructions}},
-  year        = {1991}
-}
-
-@PhDThesis{Aud92,
-  author      = {Ph. Audebaud},
-  school      = {{Universit\'e} Bordeaux I},
-  title       = {Extension du Calcul des Constructions par Points fixes},
-  year        = {1992}
-}
-
-@InProceedings{Audebaud92b,
-  author      = {Ph. Audebaud},
-  booktitle   = {{Proceedings of the 1992 Workshop on Types for Proofs and Programs}},
-  editor      = {{B. Nordstr\"om and K. Petersson and G. Plotkin}},
-  note        = {Also Research Report LIP-ENS-Lyon},
-  pages       = {21--34},
-  title       = {{CC+ : an extension of the Calculus of Constructions with fixpoints}},
-  year        = {1992}
-}
-
-@InProceedings{Augustsson85,
-  author      = {L. Augustsson},
-  title       = {{Compiling Pattern Matching}},
-  booktitle   = {Conference Functional Programming and
-Computer Architecture},
-  year        = {1985}
-}
-
-@Article{BaCo85,
-  author      = {J.L. Bates and R.L. Constable},
-  journal     = {ACM transactions on Programming Languages and Systems},
-  title       = {Proofs as {Programs}},
-  volume      = {7},
-  year        = {1985}
-}
-
-@Book{Bar81,
-  author      = {H.P. Barendregt},
-  publisher   = {North-Holland},
-  title       = {The Lambda Calculus its Syntax and Semantics},
-  year        = {1981}
-}
-
-@TechReport{Bar91,
-  author      = {H. Barendregt},
-  institution = {Catholic University Nijmegen},
-  note        = {In Handbook of Logic in Computer Science, Vol II},
-  number      = {91-19},
-  title       = {Lambda {Calculi with Types}},
-  year        = {1991}
-}
-
-@Article{BeKe92,
-  author      = {G. Bellin and J. Ketonen},
-  journal     = {Theoretical Computer Science},
-  pages       = {115--142},
-  title       = {A decision procedure revisited : Notes on direct logic, linear logic and its implementation},
-  volume      = {95},
-  year        = {1992}
-}
-
-@Book{Bee85,
-  author      = {M.J. Beeson},
-  publisher   = SV,
-  title       = {Foundations of Constructive Mathematics, Metamathematical Studies},
-  year        = {1985}
-}
-
-@Book{Bis67,
-  author      = {E. Bishop},
-  publisher   = {McGraw-Hill},
-  title       = {Foundations of Constructive Analysis},
-  year        = {1967}
-}
-
-@Book{BoMo79,
-  author      = {R.S. Boyer and J.S. Moore},
-  key         = {BoMo79},
-  publisher   = {Academic Press},
-  series      = {ACM Monograph},
-  title       = {A computational logic},
-  year        = {1979}
-}
-
-@MastersThesis{Bou92,
-  author      = {S. Boutin},
-  month       = sep,
-  school      = {{Universit\'e Paris 7}},
-  title       = {Certification d'un compilateur {ML en Coq}},
-  year        = {1992}
-}
-
-@InProceedings{Bou97,
-  title       = {Using reflection to build efficient and certified decision procedure
-s},
-  author      = {S. Boutin},
-  booktitle   = {TACS'97},
-  editor      = {Martin Abadi and Takahashi Ito},
-  publisher   = SV,
-  series      = lncs,
-  volume      = 1281, 
-  year        = {1997}
-}
-
-@PhDThesis{Bou97These,
-  author      = {S. Boutin},
-  title       = {R\'eflexions sur les quotients},
-  school      = {Paris 7},
-  year        = 1997,
-  type        = {th\`ese d'Universit\'e},
-  month       = apr
-}
-
-@Article{Bru72,
-  author      = {N.J. de Bruijn},
-  journal     = {Indag. Math.},
-  title       = {{Lambda-Calculus Notation with Nameless Dummies, a Tool for Automatic Formula Manipulation, with Application to the Church-Rosser Theorem}},
-  volume      = {34},
-  year        = {1972}
-}
-
-
-@InCollection{Bru80,
-  author      = {N.J. de Bruijn},
-  booktitle   = {to H.B. Curry : Essays on Combinatory Logic, Lambda Calculus and Formalism.},
-  editor      = {J.P. Seldin and J.R. Hindley},
-  publisher   = {Academic Press},
-  title       = {A survey of the project {Automath}},
-  year        = {1980}
-}
-
-@TechReport{COQ93,
-  author      = {G. Dowek and A. Felty and H. Herbelin and G. Huet and C. Murthy and C. Parent and C. Paulin-Mohring and B. Werner},
-  institution = {INRIA},
-  month       = may,
-  number      = {154},
-  title       = {{The Coq Proof Assistant User's Guide Version 5.8}},
-  year        = {1993}
-}
-
-@TechReport{COQ02,
-  author      = {The Coq Development Team},
-  institution = {INRIA},
-  month       = Feb,
-  number      = {255},
-  title       = {{The Coq Proof Assistant Reference Manual Version 7.2}},
-  year        = {2002}
-}
-
-@TechReport{CPar93,
-  author      = {C. Parent},
-  institution = {Ecole {Normale} {Sup\'erieure} de {Lyon}},
-  month       = oct,
-  note        = {Also in~\cite{Nijmegen93}},
-  number      = {93-29},
-  title       = {Developing certified programs in the system {Coq}- {The} {Program} tactic},
-  year        = {1993}
-}
-
-@PhDThesis{CPar95,
-  author      = {C. Parent},
-  school      = {Ecole {Normale} {Sup\'erieure} de {Lyon}},
-  title       = {{Synth\`ese de preuves de programmes dans le Calcul des Constructions Inductives}},
-  year        = {1995}
-}
-
-@Book{Caml,
-  author      = {P. Weis and X. Leroy},
-  publisher   = {InterEditions},
-  title       = {Le langage Caml},
-  year        = {1993}
-}
-
-@InProceedings{ChiPotSimp03,
-  author      = {Laurent Chicli and Lo\"{\i}c Pottier and Carlos Simpson},
-  title       = {Mathematical Quotients and Quotient Types in Coq},
-  booktitle   = {TYPES},
-  crossref    = {DBLP:conf/types/2002},
-  year        = {2002}
-}
-
-@TechReport{CoC89,
-  author      = {Projet Formel},
-  institution = {INRIA},
-  number      = {110},
-  title       = {{The Calculus of Constructions. Documentation and user's guide, Version 4.10}},
-  year        = {1989}
-}
-
-@InProceedings{CoHu85a,
-  author      = {Th. Coquand and G. Huet},
-  address     = {Linz},
-  booktitle   = {EUROCAL'85},
-  publisher   = SV,
-  series      = LNCS,
-  title       = {{Constructions : A Higher Order Proof System for Mechanizing Mathematics}},
-  volume      = {203},
-  year        = {1985}
-}
-
-@InProceedings{CoHu85b,
-  author      = {Th. Coquand and G. Huet},
-  booktitle   = {Logic Colloquium'85},
-  editor      = {The Paris Logic Group},
-  publisher   = {North-Holland},
-  title       = {{Concepts Math\'ematiques et Informatiques formalis\'es dans le Calcul des Constructions}},
-  year        = {1987}
-}
-
-@Article{CoHu86,
-  author      = {Th. Coquand and G. Huet},
-  journal     = {Information and Computation},
-  number      = {2/3},
-  title       = {The {Calculus of Constructions}},
-  volume      = {76},
-  year        = {1988}
-}
-
-@InProceedings{CoPa89,
-  author      = {Th. Coquand and C. Paulin-Mohring},
-  booktitle   = {Proceedings of Colog'88},
-  editor      = {P. Martin-L\"of and G. Mints},
-  publisher   = SV,
-  series      = LNCS,
-  title       = {Inductively defined types},
-  volume      = {417},
-  year        = {1990}
-}
-
-@Book{Con86,
-  author      = {R.L. {Constable et al.}},
-  publisher   = {Prentice-Hall},
-  title       = {{Implementing Mathematics with the Nuprl Proof Development System}},
-  year        = {1986}
-}
-
-@PhDThesis{Coq85,
-  author      = {Th. Coquand},
-  month       = jan,
-  school      = {Universit\'e Paris~7},
-  title       = {Une Th\'eorie des Constructions},
-  year        = {1985}
-}
-
-@InProceedings{Coq86,
-  author      = {Th. Coquand},
-  address     = {Cambridge, MA},
-  booktitle   = {Symposium on Logic in Computer Science},
-  publisher   = {IEEE Computer Society Press},
-  title       = {{An Analysis of Girard's Paradox}},
-  year        = {1986}
-}
-
-@InProceedings{Coq90,
-  author      = {Th. Coquand},
-  booktitle   = {Logic and Computer Science},
-  editor      = {P. Oddifredi},
-  note        = {INRIA Research Report 1088, also in~\cite{CoC89}},
-  publisher   = {Academic Press},
-  title       = {{Metamathematical Investigations of a Calculus of Constructions}},
-  year        = {1990}
-}
-
-@InProceedings{Coq91,
-  author      = {Th. Coquand},
-  booktitle   = {Proceedings 9th Int. Congress of Logic, Methodology and Philosophy of Science},
-  title       = {{A New Paradox in Type Theory}},
-  month       = {August},
-  year        = {1991}
-}
-
-@InProceedings{Coq92,
-  author      = {Th. Coquand},
-  title       = {{Pattern Matching with Dependent Types}},
-  year        = {1992},
-  crossref    = {Bastad92}
-}
-
-@InProceedings{Coquand93,
-  author      = {Th. Coquand},
-  booktitle   = {Types for Proofs and Programs},
-  editor      = {H. Barendregt and T. Nipokow},
-  publisher   = SV,
-  series      = LNCS,
-  title       = {{Infinite objects in Type Theory}},
-  volume      = {806},
-  year        = {1993},
-  pages       = {62-78}
-}
-
-@inproceedings{Corbineau08types,
-  author      = {P. Corbineau},
-  title       = {A Declarative Language for the Coq Proof Assistant},
-  editor      = {M. Miculan and I. Scagnetto and F. Honsell},
-  booktitle   = {TYPES '07, Cividale del Friuli, Revised Selected Papers},
-  publisher   = {Springer},
-  series      = LNCS,
-  volume      = {4941},
-  year        = {2007},
-  pages       = {69-84},
-  ee          = {http://dx.doi.org/10.1007/978-3-540-68103-8_5},
-}
-
-@PhDThesis{Cor97,
-  author      = {C. Cornes},
-  month       = nov,
-  school      = {{Universit\'e Paris 7}},
-  title       = {Conception d'un langage de haut niveau de représentation de preuves},
-  type        = {Th\`ese de Doctorat},
-  year        = {1997}
-}
-
-@MastersThesis{Cou94a,
-  author      = {J. Courant},
-  month       = sep,
-  school      = {DEA d'Informatique, ENS Lyon},
-  title       = {Explicitation de preuves par r\'ecurrence implicite},
-  year        = {1994}
-}
-
-@book{Cur58,
-  author      = {Haskell B. Curry and Robert Feys and William Craig},
-  title       = {Combinatory Logic},
-  volume      = 1, 
-  publisher   = "North-Holland",
-  year        = 1958,
-  note        = {{\S{9E}}},
-}
-
-@InProceedings{Del99,
-  author      = {Delahaye, D.},
-  title       = {Information Retrieval in a Coq Proof Library using
-                 Type Isomorphisms},
-  booktitle   = {Proceedings of TYPES '99, L\"okeberg},
-  publisher   = SV,
-  series      = lncs,
-  year        = {1999},
-  url         =
-    "\\{\sf ftp://ftp.inria.fr/INRIA/Projects/coq/David.Delahaye/papers/}"#
-    "{\sf TYPES99-SIsos.ps.gz}"
-}
-
-@InProceedings{Del00,
-  author      = {Delahaye, D.},
-  title       = {A {T}actic {L}anguage for the {S}ystem {{\sf Coq}}},
-  booktitle   = {Proceedings of Logic for Programming and Automated Reasoning
-               (LPAR), Reunion Island},
-  publisher   = SV,
-  series      =  LNCS,
-  volume      = {1955},
-  pages       = {85--95},
-  month       = {November},
-  year        = {2000},
-  url         =
-    "{\sf ftp://ftp.inria.fr/INRIA/Projects/coq/David.Delahaye/papers/}"#
-    "{\sf LPAR2000-ltac.ps.gz}"
-}
-
-@InProceedings{DelMay01,
-  author      = {Delahaye, D. and Mayero, M.},
-  title       = {{\tt Field}: une proc\'edure de d\'ecision pour les nombres r\'eels en {\Coq}},
-  booktitle   = {Journ\'ees Francophones des Langages Applicatifs, Pontarlier},
-  publisher   = {INRIA},
-  month       = {Janvier},
-  year        = {2001},
-  url         =
-    "\\{\sf ftp://ftp.inria.fr/INRIA/Projects/coq/David.Delahaye/papers/}"#
-    "{\sf JFLA2000-Field.ps.gz}"
-}
-
-@TechReport{Dow90,
-  author      = {G. Dowek},
-  institution = {INRIA},
-  number      = {1283},
-  title       = {Naming and Scoping in a Mathematical Vernacular},
-  type        = {Research Report},
-  year        = {1990}
-}
-
-@Article{Dow91a,
-  author      = {G. Dowek},
-  journal     = {Compte-Rendus de l'Acad\'emie des Sciences},
-  note        = {The undecidability of Third Order Pattern Matching in Calculi with Dependent Types or Type Constructors},
-  number      = {12},
-  pages       = {951--956},
-  title       = {L'Ind\'ecidabilit\'e du Filtrage du Troisi\`eme Ordre dans les Calculs avec Types D\'ependants ou Constructeurs de Types}, 
-  volume      = {I, 312},
-  year        = {1991}
-}
-
-@InProceedings{Dow91b,
-  author      = {G. Dowek},
-  booktitle   = {Proceedings of Mathematical Foundation of Computer Science},
-  note        = {Also INRIA Research Report},
-  pages       = {151--160},
-  publisher   = SV,
-  series      = LNCS,
-  title       = {A Second Order Pattern Matching Algorithm in the Cube of Typed $\lambda$-calculi},
-  volume      = {520},
-  year        = {1991}
-}
-                  
-@PhDThesis{Dow91c,
-  author      = {G. Dowek},
-  month       = dec,
-  school      = {Universit\'e Paris 7},
-  title       = {D\'emonstration automatique dans le Calcul des Constructions},
-  year        = {1991}
-}
-
-@Article{Dow92a,
-  author      = {G. Dowek},
-  title       = {The Undecidability of Pattern Matching in Calculi where Primitive Recursive Functions are Representable},
-  year        = 1993,
-  journal     = tcs,
-  volume      = 107,
-  number      = 2,
-  pages       = {349-356}
-}
-
-@Article{Dow94a,
-  author      = {G. Dowek},
-  journal     = {Annals of Pure and Applied Logic},
-  volume      = {69},
-  pages       = {135--155},
-  title       = {Third order matching is decidable},
-  year        = {1994}
-}
-
-@InProceedings{Dow94b,
-  author      = {G. Dowek},
-  booktitle   = {Proceedings of the second international conference on typed lambda calculus and applications},
-  title       = {Lambda-calculus, Combinators and the Comprehension Schema},
-  year        = {1995}
-}
-
-@InProceedings{Dyb91,
-  author      = {P. Dybjer},
-  booktitle   = {Logical Frameworks},
-  editor      = {G. Huet and G. Plotkin},
-  pages       = {59--79},
-  publisher   = {Cambridge University Press},
-  title       = {Inductive sets and families in {Martin-Löf's}
- Type Theory and their set-theoretic semantics: An inversion principle for {Martin-L\"of's} type theory}, 
-  volume      = {14},
-  year        = {1991}
-}
-
-@Article{Dyc92,
-  author      = {Roy Dyckhoff},
-  journal     = {The Journal of Symbolic Logic},
-  month       = sep,
-  number      = {3},
-  title       = {Contraction-free sequent calculi for intuitionistic logic},
-  volume      = {57},
-  year        = {1992}
-}
-
-@MastersThesis{Fil94,
-  author      = {J.-C. Filli\^atre},
-  month       = sep,
-  school      = {DEA d'Informatique, ENS Lyon},
-  title       = {Une proc\'edure de d\'ecision pour le Calcul des Pr\'edicats Direct. Étude et impl\'ementation dans le syst\`eme {\Coq}},
-  year        = {1994}
-}
-
-@TechReport{Filliatre95,
-  author      = {J.-C. Filli\^atre},
-  institution = {LIP-ENS-Lyon},
-  title       = {A decision procedure for Direct Predicate Calculus},
-  type        = {Research report},
-  number      = {96--25},
-  year        = {1995}
-}
-
-@Article{Filliatre03jfp,
-  author      = {J.-C. Filliâtre},
-  title       = {Verification of Non-Functional Programs 
-                 using Interpretations in Type Theory},
-  journal     = jfp,
-  volume      = 13,
-  number      = 4,
-  pages       = {709--745},
-  month       = jul,
-  year        = 2003,
-  note        = {[English translation of \cite{Filliatre99}]},
-  url         = {http://www.lri.fr/~filliatr/ftp/publis/jphd.ps.gz},
-  topics      = {team, lri},
-  type_publi  = {irevcomlec}
-}
-
-@PhDThesis{Filliatre99,
-  author      = {J.-C. Filli\^atre},
-  title       = {Preuve de programmes imp\'eratifs en th\'eorie des types},
-  type        = {Thèse de Doctorat},
-  school      = {Universit\'e Paris-Sud},
-  year        = 1999,
-  month       = {July},
-  url         = {\url{http://www.lri.fr/~filliatr/ftp/publis/these.ps.gz}}
-}
-
-@Unpublished{Filliatre99c,
-  author      = {J.-C. Filli\^atre},
-  title       = {{Formal Proof of a Program: Find}},
-  month       = {January},
-  year        = 2000,
-  note        = {Submitted to \emph{Science of Computer Programming}},
-  url         = {\url{http://www.lri.fr/~filliatr/ftp/publis/find.ps.gz}}
-}
-
-@InProceedings{FilliatreMagaud99,
-  author      = {J.-C. Filli\^atre and N. Magaud},
-  title       = {Certification of sorting algorithms in the system {\Coq}},
-  booktitle   = {Theorem Proving in Higher Order Logics: 
-                 Emerging Trends},
-  year        = 1999,
-  url         = {\url{http://www.lri.fr/~filliatr/ftp/publis/Filliatre-Magaud.ps.gz}}
-}
-
-@Unpublished{Fle90,
-  author      = {E. Fleury},
-  month       = jul,
-  note        = {Rapport de Stage},
-  title       = {Implantation des algorithmes de {Floyd et de Dijkstra} dans le {Calcul des Constructions}},
-  year        = {1990}
-}
-
-@Book{Fourier,
-  author      = {Jean-Baptiste-Joseph Fourier},
-  publisher   = {Gauthier-Villars},
-  title       = {Fourier's method to solve linear 
-                 inequations/equations systems.},
-  year        = {1890}
-}
-
-@InProceedings{Gim94,
-  author      = {E. Gim\'enez},
-  booktitle   = {Types'94 : Types for Proofs and Programs},
-  note        = {Extended version in LIP research report 95-07, ENS Lyon},
-  publisher   = SV,
-  series      = LNCS,
-  title       = {Codifying guarded definitions with recursive schemes},
-  volume      = {996},
-  year        = {1994}
-}
-
-@PhDThesis{Gim96,
-  author      = {E. Gim\'enez},
-  title       = {Un calcul des constructions infinies et son application \'a la v\'erification de syst\`emes communicants},
-  school      = {\'Ecole Normale Sup\'erieure de Lyon},
-  year        = {1996}
-}
-
-@TechReport{Gim98,
-  author      = {E. Gim\'enez},
-  title       = {A Tutorial on Recursive Types in Coq},
-  institution = {INRIA},
-  year        = 1998,
-  month       = mar
-}
-
-@Unpublished{GimCas05,
-  author      = {E. Gim\'enez and P. Cast\'eran},
-  title       = {A Tutorial on [Co-]Inductive Types in Coq},
-  institution = {INRIA},
-  year        = 2005,
-  month       = jan,
-  note        = {available at \url{http://coq.inria.fr/doc}}
-}
-
-@InProceedings{Gimenez95b,
-  author      = {E. Gim\'enez},
-  booktitle   = {Workshop on Types for Proofs and Programs},
-  series      = LNCS,
-  number      = {1158},
-  pages       = {135-152},
-  title       = {An application of co-Inductive types in Coq: 
-                 verification of the Alternating Bit Protocol},
-  editorS     = {S. Berardi and M. Coppo},
-  publisher   = SV,
-  year        = {1995}
-}
-
-@InProceedings{Gir70,
-  author      = {J.-Y. Girard},
-  booktitle   = {Proceedings of the 2nd Scandinavian Logic Symposium},
-  publisher   = {North-Holland},
-  title       = {Une extension de l'interpr\'etation de {G\"odel} \`a l'analyse, et son application \`a l'\'elimination des coupures dans l'analyse et la th\'eorie des types},
-  year        = {1970}
-}
-
-@PhDThesis{Gir72,
-  author      = {J.-Y. Girard},
-  school      = {Universit\'e Paris~7},
-  title       = {Interpr\'etation fonctionnelle et \'elimination des coupures de l'arithm\'etique d'ordre sup\'erieur},
-  year        = {1972}
-}
-
-@Book{Gir89,
-  author      = {J.-Y. Girard and Y. Lafont and P. Taylor},
-  publisher   = {Cambridge University Press},
-  series      = {Cambridge Tracts in Theoretical Computer Science 7},
-  title       = {Proofs and Types},
-  year        = {1989}
-}
-
-@TechReport{Har95,
-  author      = {John Harrison},
-  title       = {Metatheory and Reflection in Theorem Proving: A Survey and Critique},
-  institution = {SRI International Cambridge Computer Science Research Centre,},
-  year        =          1995,
-  type        = {Technical Report},
-  number      = {CRC-053},
-  abstract    = {http://www.cl.cam.ac.uk/users/jrh/papers.html}
-}
-
-@MastersThesis{Hir94,
-  author      = {D. Hirschkoff},
-  month       = sep,
-  school      = {DEA IARFA, Ecole des Ponts et Chauss\'ees, Paris},
-  title       = {Écriture d'une tactique arithm\'etique pour le syst\`eme {\Coq}},
-  year        = {1994}
-}
-
-@InProceedings{HofStr98,
-  author      = {Martin Hofmann and Thomas Streicher},
-  title       = {The groupoid interpretation of type theory},
-  booktitle   = {Proceedings of the meeting Twenty-five years of constructive type theory},
-  publisher   = {Oxford University Press},
-  year        = {1998}
-}
-
-@InCollection{How80,
-  author      = {W.A. Howard},
-  booktitle   = {to H.B. Curry : Essays on Combinatory Logic, Lambda Calculus and Formalism.},
-  editor      = {J.P. Seldin and J.R. Hindley},
-  note        = {Unpublished 1969 Manuscript},
-  publisher   = {Academic Press},
-  title       = {The Formulae-as-Types Notion of Constructions},
-  year        = {1980}
-}
-
-@InProceedings{Hue87tapsoft,
-  author      = {G. Huet},
-  title       = {Programming of Future Generation Computers},
-  booktitle   = {Proceedings of TAPSOFT87},
-       series = LNCS,
-  volume      = 249,
-  pages       = {276--286},
-  year        = 1987,
-  publisher   = SV
-}
-
-@InProceedings{Hue87,
-  author      = {G. Huet},
-  booktitle   = {Programming of Future Generation Computers},
-  editor      = {K. Fuchi and M. Nivat},
-  note        = {Also in \cite{Hue87tapsoft}},
-  publisher   = {Elsevier Science},
-  title       = {Induction Principles Formalized in the {Calculus of Constructions}},
-  year        = {1988}
-}
-
-@InProceedings{Hue88,
-  author      = {G. Huet},
-  booktitle   = {A perspective in Theoretical Computer Science. Commemorative Volume for Gift Siromoney},
-  editor      = {R. Narasimhan},
-  note        = {Also in~\cite{CoC89}},
-  publisher   = {World Scientific Publishing},
-  title       = {{The Constructive Engine}},
-  year        = {1989}
-}
-
-@Unpublished{Hue88b,
-  author      = {G. Huet},
-  title       = {Extending the Calculus of Constructions with Type:Type},
-  year        = 1988,
-  note        = {Unpublished}
-}
-
-@Book{Hue89,
-  editor      = {G. Huet},
-  publisher   = {Addison-Wesley},
-  series      = {The UT Year of Programming Series},
-  title       = {Logical Foundations of Functional Programming},
-  year        = {1989}
-}
-
-@InProceedings{Hue92,
-  author      = {G. Huet},
-  booktitle   = {Proceedings of 12th FST/TCS Conference, New Delhi},
-  pages       = {229--240},
-  publisher   = SV,
-  series      = LNCS,
-  title       = {The Gallina Specification Language : A case study},
-  volume      = {652},
-  year        = {1992}
-}
-
-@Article{Hue94,
-  author      = {G. Huet},
-  journal     = {J. Functional Programming},
-  pages       = {371--394},
-  publisher   = {Cambridge University Press},
-  title       = {Residual theory in $\lambda$-calculus: a formal development},
-  volume      = {4,3},
-  year        = {1994}
-}
-
-@InCollection{HuetLevy79,
-  author      = {G. Huet and J.-J. L\'{e}vy},
-  title       = {Call by Need Computations in Non-Ambigous
-Linear Term Rewriting Systems},
-  note        = {Also research report 359, INRIA, 1979},
-  booktitle   = {Computational Logic, Essays in Honor of
-Alan Robinson},
-  editor      = {J.-L. Lassez and G. Plotkin},
-  publisher   = {The MIT press},
-  year        = {1991}
-}
-
-@Article{KeWe84,
-  author      = {J. Ketonen and R. Weyhrauch},
-  journal     = {Theoretical Computer Science},
-  pages       = {297--307},
-  title       = {A decidable fragment of {P}redicate {C}alculus},
-  volume      = {32},
-  year        = {1984}
-}
-
-@Book{Kle52,
-  author      = {S.C. Kleene},
-  publisher   = {North-Holland},
-  series      = {Bibliotheca Mathematica},
-  title       = {Introduction to Metamathematics},
-  year        = {1952}
-}
-
-@Book{Kri90,
-  author      = {J.-L. Krivine},
-  publisher   = {Masson},
-  series      = {Etudes et recherche en informatique},
-  title       = {Lambda-calcul {types et mod\`eles}},
-  year        = {1990}
-}
-
-@Book{LE92,
-  editor      = {G. Huet and G. Plotkin},
-  publisher   = {Cambridge University Press},
-  title       = {Logical Environments},
-  year        = {1992}
-}
-
-@Book{LF91,
-  editor      = {G. Huet and G. Plotkin},
-  publisher   = {Cambridge University Press},
-  title       = {Logical Frameworks},
-  year        = {1991}
-}
-
-@Article{Laville91,
-  author      = {A. Laville},
-  title       = {Comparison of Priority Rules in Pattern
-Matching and Term Rewriting},
-  journal     = {Journal of Symbolic Computation},
-  volume      = {11},
-  pages       = {321--347},
-  year        = {1991}
-}
-
-@InProceedings{LePa94,
-  author      = {F. Leclerc and C. Paulin-Mohring},
-  booktitle   = {{Types for Proofs and Programs, Types' 93}},
-  editor      = {H. Barendregt and T. Nipkow},
-  publisher   = SV,
-  series      = {LNCS},
-  title       = {{Programming with Streams in Coq. A case study : The Sieve of Eratosthenes}},
-  volume      = {806},
-  year        = {1994}
-}
-
-@TechReport{Leroy90,
-  author      = {X. Leroy},
-  title       = {The {ZINC} experiment: an economical implementation
-of the {ML} language},
-  institution = {INRIA},
-  number      = {117},
-  year        = {1990}
-}
-
-@InProceedings{Let02,
-  author      = {P. Letouzey},
-  title       = {A New Extraction for Coq},
-  booktitle   = {TYPES},
-  year        = 2002,
-  crossref    = {DBLP:conf/types/2002},
-  url         = {draft at \url{http://www.pps.jussieu.fr/~letouzey/download/extraction2002.ps.gz}}
-}
-
-@PhDThesis{Luo90,
-  author      = {Z. Luo},
-  title       = {An Extended Calculus of Constructions},
-  school      = {University of Edinburgh},
-  year        = {1990}
-}
-
-@inproceedings{Luttik97specificationof,
-	Author = {Sebastiaan P. Luttik and Eelco Visser},
-	Booktitle = {2nd International Workshop on the Theory and Practice of Algebraic Specifications (ASF+SDF'97), Electronic Workshops in Computing},
-	Publisher = {Springer-Verlag},
-	Title = {Specification of Rewriting Strategies},
-	Year = {1997}}
-
-@Book{MaL84,
-  author      = {{P. Martin-L\"of}},
-  publisher   = {Bibliopolis},
-  series      = {Studies in Proof Theory},
-  title       = {Intuitionistic Type Theory},
-  year        = {1984}
-}
-
-@Article{MaSi94,
-  author      = {P. Manoury and M. Simonot},
-  title       = {Automatizing Termination Proofs of Recursively Defined Functions.},
-  journal     = {TCS},
-  volume      = {135},
-  number      = {2},
-  year        = {1994},
-  pages       = {319-343},
-}
-
-@InProceedings{Miquel00,
-  author      = {A. Miquel},
-  title       = {A Model for Impredicative Type Systems with Universes,
-Intersection Types and Subtyping},
-  booktitle   = {{Proceedings of the 15th Annual IEEE Symposium on Logic in Computer Science (LICS'00)}},
-  publisher   = {IEEE Computer Society Press},
-  year        = {2000}
-}
-
-@PhDThesis{Miquel01a,
-  author      = {A. Miquel},
-  title       = {Le Calcul des Constructions implicite: syntaxe et s\'emantique},
-  month       = {dec},
-  school      = {{Universit\'e Paris 7}},
-  year        = {2001}
-}
-
-@InProceedings{Miquel01b,
-  author      = {A. Miquel},
-  title       = {The Implicit Calculus of Constructions: Extending Pure Type Systems with an Intersection Type Binder and Subtyping},
-  booktitle   = {{Proceedings of the fifth International Conference on Typed Lambda Calculi and Applications (TLCA01), Krakow, Poland}},
-  publisher   = SV,
-  series      = {LNCS},
-  number      = 2044,
-  year        = {2001}
-}
-
-@InProceedings{MiWer02,
-  author      = {A. Miquel and B. Werner},
-  title       = {The Not So Simple Proof-Irrelevant Model of CC},
-  booktitle   = {TYPES},
-  year        = {2002},
-  pages       = {240-258},
-  ee          = {http://link.springer.de/link/service/series/0558/bibs/2646/26460240.htm},
-  crossref    = {DBLP:conf/types/2002},
-  bibsource   = {DBLP, http://dblp.uni-trier.de}
-}
-
-@proceedings{DBLP:conf/types/2002,
-  editor      = {H. Geuvers and F. Wiedijk},
-  title       = {Types for Proofs and Programs, Second International Workshop,
-                 TYPES 2002, Berg en Dal, The Netherlands, April 24-28, 2002,
-                 Selected Papers},
-  booktitle   = {TYPES},
-  publisher   = SV,
-  series      = LNCS,
-  volume      = {2646},
-  year        = {2003},
-  isbn        = {3-540-14031-X},
-  bibsource   = {DBLP, http://dblp.uni-trier.de}
-}
-
-@InProceedings{Moh89a,
-  author      = {C. Paulin-Mohring},
-  address     = {Austin},
-  booktitle   = {Sixteenth Annual ACM Symposium on Principles of Programming Languages},
-  month       = jan,
-  publisher   = {ACM},
-  title       = {Extracting ${F}_{\omega}$'s programs from proofs in the {Calculus of Constructions}},
-  year        = {1989}
-}
-
-@PhDThesis{Moh89b,
-  author      = {C. Paulin-Mohring},
-  month       = jan,
-  school      = {{Universit\'e Paris 7}},
-  title       = {Extraction de programmes dans le {Calcul des Constructions}},
-  year        = {1989}
-}
-
-@InProceedings{Moh93,
-  author      = {C. Paulin-Mohring},
-  booktitle   = {Proceedings of the conference Typed Lambda Calculi and Applications},
-  editor      = {M. Bezem and J.-F. Groote},
-  note        = {Also LIP research report 92-49, ENS Lyon},
-  number      = {664},
-  publisher   = SV,
-  series      = {LNCS},
-  title       = {{Inductive Definitions in the System Coq - Rules and Properties}},
-  year        = {1993}
-}
-
-@Book{Moh97,
-  author      = {C. Paulin-Mohring},
-  month       = jan,
-  publisher   = {{ENS Lyon}},
-  title       = {{Le syst\`eme Coq. \mbox{Th\`ese d'habilitation}}},
-  year        = {1997}
-}
-
-@MastersThesis{Mun94,
-  author      = {C. Muñoz},
-  month       = sep,
-  school      = {DEA d'Informatique Fondamentale, Universit\'e Paris 7},
-  title       = {D\'emonstration automatique dans la logique propositionnelle intuitionniste},
-  year        = {1994}
-}
-
-@PhDThesis{Mun97d,
-  author      = {C. Mu{\~{n}}oz},
-  title       = {Un calcul de substitutions pour la repr\'esentation
-                 de preuves partielles en th\'eorie de types},
-  school      = {Universit\'e Paris 7},
-  year        = {1997},
-  note        = {Version en anglais disponible comme rapport de 
-                 recherche INRIA RR-3309},        
-  type        = {Th\`ese de Doctorat}
-}
-
-@Book{NoPS90,
-  author      = {B. {Nordstr\"om} and K. Peterson and J. Smith},
-  booktitle   = {Information Processing 83},
-  publisher   = {Oxford Science Publications},
-  series      = {International Series of Monographs on Computer Science},
-  title       = {Programming in {Martin-L\"of's} Type Theory},
-  year        = {1990}
-}
-
-@Article{Nor88,
-  author      = {B. {Nordstr\"om}},
-  journal     = {BIT},
-  title       = {Terminating General Recursion},
-  volume      = {28},
-  year        = {1988}
-}
-
-@Book{Odi90,
-  editor      = {P. Odifreddi},
-  publisher   = {Academic Press},
-  title       = {Logic and Computer Science},
-  year        = {1990}
-}
-
-@InProceedings{PaMS92,
-  author      = {M. Parigot and P. Manoury and M. Simonot},
-  address     = {St. Petersburg, Russia},
-  booktitle   = {Logic Programming and automated reasoning},
-  editor      = {A. Voronkov},
-  month       = jul,
-  number      = {624},
-  publisher   = SV,
-  series      = {LNCS},
-  title       = {{ProPre : A Programming language with proofs}},
-  year        = {1992}
-}
-
-@Article{PaWe92,
-  author      = {C. Paulin-Mohring and B. Werner},
-  journal     = {Journal of Symbolic Computation},
-  pages       = {607--640},
-  title       = {{Synthesis of ML programs in the system Coq}},
-  volume      = {15},
-  year        = {1993}
-}
-
-@Article{Par92,
-  author      = {M. Parigot},
-  journal     = {Theoretical Computer Science},
-  number      = {2},
-  pages       = {335--356},
-  title       = {{Recursive Programming with Proofs}},
-  volume      = {94},
-  year        = {1992}
-}
-
-@InProceedings{Parent95b,
-  author      = {C. Parent},
-  booktitle   = {{Mathematics of Program Construction'95}},
-  publisher   = SV,
-  series      = {LNCS},
-  title       = {{Synthesizing proofs from programs in
-the Calculus of Inductive Constructions}},
-  volume      = {947},
-  year        = {1995}
-}
-
-@InProceedings{Prasad93,
-  author      = {K.V. Prasad},
-  booktitle   = {{Proceedings of CONCUR'93}},
-  publisher   = SV,
-  series      = {LNCS},
-  title       = {{Programming with broadcasts}},
-  volume      = {715},
-  year        = {1993}
-}
-
-@Book{RC95,
-  author      = {di~Cosmo, R.},
-  title       = {Isomorphisms of Types: from $\lambda$-calculus to information
-                 retrieval and language design},
-  series      = {Progress in Theoretical Computer Science},
-  publisher   = {Birkhauser},
-  year        = {1995},
-  note        = {ISBN-0-8176-3763-X}
-}
-
-@TechReport{Rou92,
-  author      = {J. Rouyer},
-  institution = {INRIA},
-  month       = nov,
-  number      = {1795},
-  title       = {{Développement de l'Algorithme d'Unification dans le Calcul des Constructions}},
-  year        = {1992}
-}
-
-@Article{Rushby98,
-  title       = {Subtypes for Specifications: Predicate Subtyping in
-                {PVS}},
-  author      = {John Rushby and Sam Owre and N. Shankar},
-  journal     = {IEEE Transactions on Software Engineering},
-  pages       = {709--720},
-  volume      = 24,
-  number      = 9,
-  month       = sep,
-  year        = 1998
-}
-
-@TechReport{Saibi94,
-  author      = {A. Sa\"{\i}bi},
-  institution = {INRIA},
-  month       = dec,
-  number      = {2345},
-  title       = {{Axiomatization of a lambda-calculus with explicit-substitutions in the Coq System}},
-  year        = {1994}
-}
-
-
-@MastersThesis{Ter92,
-  author      = {D. Terrasse},
-  month       = sep,
-  school      = {IARFA},
-  title       = {{Traduction de TYPOL en COQ. Application \`a Mini ML}},
-  year        = {1992}
-}
-
-@TechReport{ThBeKa92,
-  author      = {L. Th\'ery and Y. Bertot and G. Kahn},
-  institution = {INRIA Sophia},
-  month       = may,
-  number      = {1684},
-  title       = {Real theorem provers deserve real user-interfaces},
-  type        = {Research Report},
-  year        = {1992}
-}
-
-@Book{TrDa89,
-  author      = {A.S. Troelstra and D. van Dalen},
-  publisher   = {North-Holland},
-  series      = {Studies in Logic and the foundations of Mathematics, volumes 121 and 123},
-  title       = {Constructivism in Mathematics, an introduction},
-  year        = {1988}
-}
-
-@PhDThesis{Wer94,
-  author      = {B. Werner},
-  school      = {Universit\'e Paris 7},
-  title       = {Une th\'eorie des constructions inductives},
-  type        = {Th\`ese de Doctorat},
-  year        = {1994}
-}
-
-@PhDThesis{Bar99,
-  author      = {B. Barras},
-  school      = {Universit\'e Paris 7},
-  title       = {Auto-validation d'un système de preuves avec familles inductives},
-  type        = {Th\`ese de Doctorat},
-  year        = {1999}
-}
-
-@Unpublished{ddr98,
-  author      = {D. de Rauglaudre},
-  title       = {Camlp4 version 1.07.2},
-  year        = {1998},
-  note        = {In Camlp4 distribution}
-}
-
-@Article{dowek93,
-  author      = {G. Dowek},
-  title       = {{A Complete Proof Synthesis Method for the Cube of Type Systems}},
-  journal     = {Journal Logic Computation},
-  volume      = {3},
-  number      = {3},
-  pages       = {287--315},
-  month       = {June},
-  year        = {1993}
-}
-
-@InProceedings{manoury94,
-  author      = {P. Manoury},
-  title       = {{A User's Friendly Syntax to Define
-Recursive Functions as Typed $\lambda-$Terms}},
-  booktitle   = {{Types for Proofs and Programs, TYPES'94}},
-  series      = {LNCS},
-  volume      = {996},
-  month       = jun,
-  year        = {1994}
-}
-
-@TechReport{maranget94,
-  author      = {L. Maranget},
-  institution = {INRIA},
-  number      = {2385},
-  title       = {{Two Techniques for Compiling Lazy Pattern Matching}},
-  year        = {1994}
-}
-
-@InProceedings{puel-suarez90,
-  author      = {L.Puel and A. Su\'arez},
-  booktitle   = {{Conference Lisp and Functional Programming}},
-  series      = {ACM},
-  publisher   = SV,
-  title       = {{Compiling Pattern Matching by Term
-Decomposition}},
-  year        = {1990}
-}
-
-@MastersThesis{saidi94,
-  author      = {H. Saidi},
-  month       = sep,
-  school      = {DEA d'Informatique Fondamentale, Universit\'e Paris 7},
-  title       = {R\'esolution d'\'equations dans le syst\`eme T
- de G\"odel},
-  year        = {1994}
-}
-
-@inproceedings{sozeau06,
-  author = {Matthieu Sozeau},
-  title = {Subset Coercions in {C}oq},
-  year = {2007},
-  booktitle = {TYPES'06},
-  pages = {237-252},
-  volume = {4502},
-  publisher = "Springer",
-  series =    {LNCS}
-}
-
-@inproceedings{sozeau08,
-	Author = {Matthieu Sozeau and Nicolas Oury},
-	booktitle = {TPHOLs'08},
-	Pdf = {http://www.lri.fr/~sozeau/research/publications/drafts/classes.pdf},
-	Title = {{F}irst-{C}lass {T}ype {C}lasses},
-	Year = {2008},
-}
-
-@Misc{streicher93semantical,
-  author      = {T. Streicher},
-  title       = {Semantical Investigations into Intensional Type Theory},
-  note        = {Habilitationsschrift, LMU Munchen.},
-  year        = {1993}
-}
-
-@Misc{Pcoq,
-  author      = {Lemme Team},
-  title       = {Pcoq a graphical user-interface for {Coq}},
-  note        = {\url{http://www-sop.inria.fr/lemme/pcoq/}}
-}
-
-@Misc{ProofGeneral,
-  author      = {David Aspinall},
-  title       = {Proof General},
-  note        = {\url{https://proofgeneral.github.io/}}
-}
-
-@Book{CoqArt,
-  title       = {Interactive Theorem Proving and Program Development.
-                 Coq'Art: The Calculus of Inductive Constructions},
-  author      = {Yves Bertot and Pierre Castéran},
-  publisher   = {Springer Verlag},
-  series      = {Texts in Theoretical Computer Science. An EATCS series}, 
-  year        = 2004
-}
-
-@InCollection{wadler87,
-  author      = {P. Wadler},
-  title       = {Efficient  Compilation of Pattern Matching},
-  booktitle   = {The Implementation of Functional Programming
-Languages},
-  editor      = {S.L. Peyton Jones},
-  publisher   = {Prentice-Hall},
-  year        = {1987}
-}
-
-@inproceedings{DBLP:conf/types/CornesT95,
-  author    = {Cristina Cornes and
-               Delphine Terrasse},
-  title     = {Automating Inversion of Inductive Predicates in Coq},
-  booktitle = {TYPES},
-  year      = {1995},
-  pages     = {85-104},
-  crossref  = {DBLP:conf/types/1995},
-  bibsource = {DBLP, http://dblp.uni-trier.de}
-}
-@proceedings{DBLP:conf/types/1995,
-  editor    = {Stefano Berardi and
-               Mario Coppo},
-  title     = {Types for Proofs and Programs, International Workshop TYPES'95,
-               Torino, Italy, June 5-8, 1995, Selected Papers},
-  booktitle = {TYPES},
-  publisher = {Springer},
-  series    = {Lecture Notes in Computer Science},
-  volume    = {1158},
-  year      = {1996},
-  isbn      = {3-540-61780-9},
-  bibsource = {DBLP, http://dblp.uni-trier.de}
-}
-
-@inproceedings{DBLP:conf/types/McBride00,
-  author    = {Conor McBride},
-  title     = {Elimination with a Motive},
-  booktitle = {TYPES},
-  year      = {2000},
-  pages     = {197-216},
-  ee        = {http://link.springer.de/link/service/series/0558/bibs/2277/22770197.htm},
-  crossref  = {DBLP:conf/types/2000},
-  bibsource = {DBLP, http://dblp.uni-trier.de}
-}
-
-@proceedings{DBLP:conf/types/2000,
-  editor    = {Paul Callaghan and
-               Zhaohui Luo and
-               James McKinna and
-               Robert Pollack},
-  title     = {Types for Proofs and Programs, International Workshop, TYPES
-               2000, Durham, UK, December 8-12, 2000, Selected Papers},
-  booktitle = {TYPES},
-  publisher = {Springer},
-  series    = {Lecture Notes in Computer Science},
-  volume    = {2277},
-  year      = {2002},
-  isbn      = {3-540-43287-6},
-  bibsource = {DBLP, http://dblp.uni-trier.de}
-}
-
-@INPROCEEDINGS{sugar,
-    author = {Alessandro Giovini and Teo Mora and Gianfranco Niesi and Lorenzo Robbiano and Carlo Traverso},
-    title = {"One sugar cube, please" or Selection strategies in the Buchberger algorithm},
-    booktitle = { Proceedings of the ISSAC'91, ACM Press},
-    year = {1991},
-    pages = {5--4},
-    publisher = {}
-}
-
-@article{LeeWerner11,
-  author    = {Gyesik Lee and
-               Benjamin Werner},
-  title     = {Proof-irrelevant model of {CC} with predicative induction
-               and judgmental equality},
-  journal   = {Logical Methods in Computer Science},
-  volume    = {7},
-  number    = {4},
-  year      = {2011},
-  ee        = {http://dx.doi.org/10.2168/LMCS-7(4:5)2011},
-  bibsource = {DBLP, http://dblp.uni-trier.de}
-}
-
-@Comment{cross-references, must be at end}
-
-@Book{Bastad92,
-  editor      = {B. Nordstr\"om and K. Petersson and G. Plotkin},
-  publisher   = {Available by ftp at site ftp.inria.fr},
-  title       = {Proceedings of the 1992 Workshop on Types for Proofs and Programs},
-  year        = {1992}
-}
-
-@Book{Nijmegen93,
-  editor      = {H. Barendregt and T. Nipkow},
-  publisher   = SV,
-  series      = LNCS,
-  title       = {Types for Proofs and Programs},
-  volume      = {806},
-  year        = {1994}
-}
-
-@article{ TheOmegaPaper,
-    author = "W. Pugh",
-    title = "The Omega test: a fast and practical integer programming algorithm for dependence analysis",
-    journal = "Communication of the ACM",
-    pages = "102--114",
-    year = "1992",
-}
-
-@inproceedings{CSwcu,
-    hal_id = {hal-00816703},
-    url = {http://hal.inria.fr/hal-00816703},
-    title = {{Canonical Structures for the working Coq user}},
-    author = {Mahboubi, Assia and Tassi, Enrico},
-    booktitle = {{ITP 2013, 4th Conference on Interactive Theorem Proving}},
-    publisher = {Springer},
-    pages = {19-34},
-    address = {Rennes, France},
-    volume = {7998},
-    editor = {Sandrine Blazy and Christine Paulin and David Pichardie },
-    series = {LNCS },
-    doi = {10.1007/978-3-642-39634-2\_5 },
-    year = {2013},
-}
-
-@article{CSlessadhoc,
- author = {Gonthier, Georges and Ziliani, Beta and Nanevski, Aleksandar and Dreyer, Derek},
- title = {How to Make Ad Hoc Proof Automation Less Ad Hoc},
- journal = {SIGPLAN Not.},
- issue_date = {September 2011},
- volume = {46},
- number = {9},
- month = sep,
- year = {2011},
- issn = {0362-1340},
- pages = {163--175},
- numpages = {13},
- url = {http://doi.acm.org/10.1145/2034574.2034798},
- doi = {10.1145/2034574.2034798},
- acmid = {2034798},
- publisher = {ACM},
- address = {New York, NY, USA},
- keywords = {canonical structures, coq, custom proof automation, hoare type theory, interactive theorem proving, tactics, type classes},
-}
-
-@inproceedings{CompiledStrongReduction,
-  author    = {Benjamin Gr{\'{e}}goire and
-               Xavier Leroy},
-  editor    = {Mitchell Wand and
-               Simon L. Peyton Jones},
-  title     = {A compiled implementation of strong reduction},
-  booktitle = {Proceedings of the Seventh {ACM} {SIGPLAN} International Conference
-               on Functional Programming {(ICFP} '02), Pittsburgh, Pennsylvania,
-               USA, October 4-6, 2002.},
-  pages     = {235--246},
-  publisher = {{ACM}},
-  year      = {2002},
-  url       = {http://doi.acm.org/10.1145/581478.581501},
-  doi       = {10.1145/581478.581501},
-  timestamp = {Tue, 11 Jun 2013 13:49:16 +0200},
-  biburl    = {http://dblp.uni-trier.de/rec/bib/conf/icfp/GregoireL02},
-  bibsource = {dblp computer science bibliography, http://dblp.org}
-}
-
-@inproceedings{FullReduction,
-  author    = {Mathieu Boespflug and
-               Maxime D{\'{e}}n{\`{e}}s and
-               Benjamin Gr{\'{e}}goire},
-  editor    = {Jean{-}Pierre Jouannaud and
-               Zhong Shao},
-  title     = {Full Reduction at Full Throttle},
-  booktitle = {Certified Programs and Proofs - First International Conference, {CPP}
-               2011, Kenting, Taiwan, December 7-9, 2011. Proceedings},
-  series    = {Lecture Notes in Computer Science},
-  volume    = {7086},
-  pages     = {362--377},
-  publisher = {Springer},
-  year      = {2011},
-  url       = {http://dx.doi.org/10.1007/978-3-642-25379-9_26},
-  doi       = {10.1007/978-3-642-25379-9_26},
-  timestamp = {Thu, 17 Nov 2011 13:33:48 +0100},
-  biburl    = {http://dblp.uni-trier.de/rec/bib/conf/cpp/BoespflugDG11},
-  bibsource = {dblp computer science bibliography, http://dblp.org}
-}
diff --git a/doc/refman/coq-listing.tex b/doc/refman/coq-listing.tex
deleted file mode 100644
index c69c3b1b8..000000000
--- a/doc/refman/coq-listing.tex
+++ /dev/null
@@ -1,152 +0,0 @@
-%=======================================================================
-% Listings LaTeX package style for Gallina + SSReflect (Assia Mahboubi 2007)
-
-\lstdefinelanguage{SSR} {
-
-% Anything betweeen $ becomes LaTeX math mode
-mathescape=true,
-% Comments may or not include Latex commands
-texcl=false,
-
-
-% Vernacular commands
-morekeywords=[1]{
-From, Section, Module, End, Require, Import, Export, Defensive, Function,
-Variable, Variables, Parameter, Parameters, Axiom, Hypothesis, Hypotheses,
-Notation, Local, Tactic, Reserved, Scope, Open, Close, Bind, Delimit,
-Definition, Let, Ltac, Fixpoint, CoFixpoint, Add, Morphism, Relation,
-Implicit, Arguments, Set, Unset, Contextual, Strict, Prenex, Implicits,
-Inductive, CoInductive, Record, Structure, Canonical, Coercion,
-Theorem, Lemma, Corollary, Proposition, Fact, Remark, Example,
-Proof, Goal, Save, Qed, Defined, Hint, Resolve, Rewrite, View,
-Search, Show, Print, Printing, All, Graph, Projections, inside,
-outside, Locate, Maximal},
-
-% Gallina
-morekeywords=[2]{forall, exists, exists2, fun, fix, cofix, struct,
-      match, with, end, as, in, return, let, if, is, then, else,
-      for, of, nosimpl},
-
-% Sorts
-morekeywords=[3]{Type, Prop},
-
-% Various tactics, some are std Coq subsumed by ssr, for the manual purpose
-morekeywords=[4]{
-         pose, set, move, case, elim, apply, clear,
-            hnf, intro, intros, generalize, rename, pattern, after,
-	    destruct, induction, using, refine, inversion, injection,
-         rewrite, congr, unlock, compute, ring, field,
-            replace, fold, unfold, change, cutrewrite, simpl,
-         have, gen, generally, suff, wlog, suffices, without, loss, nat_norm,
-            assert, cut, trivial, revert, bool_congr, nat_congr, abstract,
-	 symmetry, transitivity, auto, split, left, right, autorewrite},
-
-% Terminators
-morekeywords=[5]{
-         by, done, exact, reflexivity, tauto, romega, omega,
-         assumption, solve, contradiction, discriminate},
-
-
-% Control
-morekeywords=[6]{do, last, first, try, idtac, repeat},
-
-% Various symbols
-% For the ssr manual we turn off the prettyprint of formulas
-% literate=
-%	{->}{{$\rightarrow\,$}}2
-% 	{->}{{\tt ->}}3
-%	{<-}{{$\leftarrow\,$}}2
-% 	{<-}{{\tt <-}}2
-% 	{>->}{{$\mapsto$}}3
-% 	{<=}{{$\leq$}}1
-% 	{>=}{{$\geq$}}1
-% 	{<>}{{$\neq$}}1
-% 	{/\\}{{$\wedge$}}2
-% 	{\\/}{{$\vee$}}2
-% 	{<->}{{$\leftrightarrow\;$}}3
-% 	{<=>}{{$\Leftrightarrow\;$}}3
-% 	{:nat}{{$~\in\mathbb{N}$}}3
-%	{fforall\ }{{$\forall_f\,$}}1
-%	{forall\ }{{$\forall\,$}}1
-%	{exists\ }{{$\exists\,$}}1
-% 	{negb}{{$\neg$}}1
-% 	{spp}{{:*:\,}}1
-% 	{~}{{$\sim$}}1
-% 	{\\in}{{$\in\;$}}1
-% 	{/\\}{$\land\,$}1
-% 	{:*:}{{$*$}}2
-%	{=>}{{$\,\Rightarrow\ $}}1
-% 	{=>}{{\tt =>}}2
-% 	{:=}{{{\tt:=}\,\,}}2
-% 	{==}{{$\equiv$}\,}2
-% 	{!=}{{$\neq$}\,}2
-% 	{^-1}{{$^{-1}$}}1
-% 	{elt'}{elt'}1
-%       {=}{{\tt=}\,\,}2
-%       {+}{{\tt+}\,\,}2,
-literate=
-	{isn't }{{{\ttfamily\color{dkgreen} isn't }}}1,
-
-% Comments delimiters, we do turn this off for the manual
-%comment=[s]{(*}{*)},
-
-% Spaces are not displayed as a special character
-showstringspaces=false,
-
-% String delimiters
-morestring=[b]",
-morestring=[d]",
-
-% Size of tabulations
-tabsize=3,
-
-% Enables ASCII chars 128 to 255
-extendedchars=true,
-
-% Case sensitivity
-sensitive=true,
-
-% Automatic breaking of long lines
-breaklines=true,
-
-% Default style fors listings
-basicstyle=\ttfamily,
-
-% Position of captions is bottom
-captionpos=b,
-
-% Full flexible columns
-columns=[l]fullflexible,
-
-% Style for (listings') identifiers
-identifierstyle={\ttfamily\color{black}},
-% Note : highlighting of Coq identifiers is done through a new
-% delimiter definition through an lstset at the begining of the
-% document. Don't know how to do better.
-
-% Style for declaration keywords
-keywordstyle=[1]{\ttfamily\color{dkviolet}},
-
-% Style for gallina keywords
-keywordstyle=[2]{\ttfamily\color{dkgreen}},
-
-% Style for sorts keywords
-keywordstyle=[3]{\ttfamily\color{lightblue}},
-
-% Style for tactics keywords
-keywordstyle=[4]{\ttfamily\color{dkblue}},
-
-% Style for terminators keywords
-keywordstyle=[5]{\ttfamily\color{red}},
-
-
-%Style for iterators
-keywordstyle=[6]{\ttfamily\color{dkpink}},
-
-% Style for strings
-stringstyle=\ttfamily,
-
-% Style for comments
-commentstyle=\rmfamily,
-
-}
diff --git a/doc/refman/coqide-queries.png b/doc/refman/coqide-queries.png
deleted file mode 100644
index 7a46ac4e6..000000000
--- a/doc/refman/coqide-queries.png
+++ /dev/null
diff --git a/doc/refman/coqide.png b/doc/refman/coqide.png
deleted file mode 100644
index e300401c9..000000000
--- a/doc/refman/coqide.png
+++ /dev/null
diff --git a/doc/refman/headers.hva b/doc/refman/headers.hva
deleted file mode 100644
index 9714a29be..000000000
--- a/doc/refman/headers.hva
+++ /dev/null
@@ -1,44 +0,0 @@
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-% File headers.hva
-% Hevea version of headers.sty
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-% Commands for indexes
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\usepackage{index}
-\makeindex
-
-
-\newindex{tactic}{tacidx}{tacind}{Tactics Index}
-\newindex{command}{comidx}{comind}{Vernacular Commands Index}
-\newindex{option}{optidx}{optind}{Vernacular Options Index}
-\newindex{error}{erridx}{errind}{Index of Error Messages}
-\renewindex{default}{idx}{ind}{Global Index}
-
-\newcommand{\printrefmanindex}[3]{%
-\addcontentsline{toc}{chapter}{#2}%
-\printindex[#1]%
-\cutname{#3}%
-}
-
-\newcommand{\tacindex}[1]{%
-\index{#1@\texttt{#1}}\index[tactic]{#1@\texttt{#1}}}
-\newcommand{\comindex}[1]{%
-\index{#1@\texttt{#1}}\index[command]{#1@\texttt{#1}}}
-\newcommand{\optindex}[1]{%
-\index{#1@\texttt{#1}}\index[option]{#1@\texttt{#1}}}
-\newcommand{\errindex}[1]{\texttt{#1}\index[error]{#1}}
-\newcommand{\errindexbis}[2]{\texttt{#1}\index[error]{#2}}
-\newcommand{\ttindex}[1]{\index{#1@\texttt{#1}}}
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-% For the Addendum table of contents
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\newcommand{\aauthor}[1]{{\LARGE \bf #1} \bigskip}  % 3 \bigskip's that were here originally
-						    % may be good for LaTeX but too much for HTML    
-\newcommand{\atableofcontents}{}
-\newcommand{\achapter}[1]{\chapter{#1}}
-\newcommand{\asection}{\section}
-\newcommand{\asubsection}{\subsection}
-\newcommand{\asubsubsection}{\subsubsection}
diff --git a/doc/refman/headers.sty b/doc/refman/headers.sty
deleted file mode 100644
index fb39f687d..000000000
--- a/doc/refman/headers.sty
+++ /dev/null
@@ -1,88 +0,0 @@
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-% File headers.sty
-% Commands for pretty headers, multiple indexes, and the appendix.
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\usepackage{fancyhdr}
-
-\setlength{\headheight}{14pt}
-
-\pagestyle{fancyplain}
-
-\newcommand{\coqfooter}{\tiny Coq Reference Manual, V\coqversion{}, \today}
-
-\cfoot{}
-\lfoot[{\coqfooter}]{}
-\rfoot[]{{\coqfooter}}
-
-\newcommand{\setheaders}[1]{\rhead[\fancyplain{}{\textbf{#1}}]{\fancyplain{}{\thepage}}\lhead[\fancyplain{}{\thepage}]{\fancyplain{}{\textbf{#1}}}}
-\newcommand{\defaultheaders}{\rhead[\fancyplain{}{\leftmark}]{\fancyplain{}{\thepage}}\lhead[\fancyplain{}{\thepage}]{\fancyplain{}{\rightmark}}}
-
-\renewcommand{\chaptermark}[1]{\markboth{{\bf \thechapter~#1}}{}}
-\renewcommand{\sectionmark}[1]{\markright{\thesection~#1}}
-\renewcommand{\contentsname}{%
-\protect\setheaders{Table of contents}Table of contents}
-\renewcommand{\bibname}{\protect\setheaders{Bibliography}%
-\protect\RefManCutCommand{BEGINBIBLIO=\thepage}%
-\protect\addcontentsline{toc}{chapter}{Bibliography}Bibliography}
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-% Commands for indexes
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\usepackage{index}
-\makeindex
-
-\newindex{tactic}{tacidx}{tacind}{Tactics Index}
-\newindex{command}{comidx}{comind}{Vernacular Commands Index}
-\newindex{option}{optidx}{optind}{Vernacular Options Index}
-\newindex{error}{erridx}{errind}{Index of Error Messages}
-\renewindex{default}{idx}{ind}{Global Index}
-
-\newcommand{\printrefmanindex}[3]{%
-\cleardoublepage%
-\phantomsection%
-\setheaders{#2}%
-\addcontentsline{toc}{chapter}{#2}%
-\printindex[#1]%
-\cutname{#3}%
-}
-
-\newcommand{\tacindex}[1]{%
-\index{#1@\texttt{#1}}\index[tactic]{#1@\texttt{#1}}}
-\newcommand{\comindex}[1]{%
-\index{#1@\texttt{#1}}\index[command]{#1@\texttt{#1}}}
-\newcommand{\optindex}[1]{%
-\index{#1@\texttt{#1}}\index[option]{#1@\texttt{#1}}}
-\newcommand{\errindex}[1]{\texttt{#1}\index[error]{#1}}
-\newcommand{\errindexbis}[2]{\texttt{#1}\index[error]{#2}}
-\newcommand{\ttindex}[1]{\index{#1@\texttt{#1}}}
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-% For the Addendum table of contents
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\newcommand{\aauthor}[1]{{\LARGE \bf #1} \bigskip \bigskip \bigskip}
-\newcommand{\atableofcontents}{\section*{Contents}\@starttoc{atoc}}
-\newcommand{\achapter}[1]{
-  \chapter{#1}\addcontentsline{atoc}{chapter}{#1}}
-\newcommand{\asection}[1]{
-  \section{#1}\addcontentsline{atoc}{section}{#1}}
-\newcommand{\asubsection}[1]{
-  \subsection{#1}\addcontentsline{atoc}{subsection}{#1}}
-\newcommand{\asubsubsection}[1]{
-  \subsubsection{#1}\addcontentsline{atoc}{subsubsection}{#1}}
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-% Reference-Manual.sh is generated to cut the Postscript
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-%\@starttoc{sh}
-\newwrite\RefManCut@out%
-\immediate\openout\RefManCut@out\jobname.sh
-\newcommand{\RefManCutCommand}[1]{%
-\immediate\write\RefManCut@out{#1}}
-\newcommand{\RefManCutClose}{%
-\immediate\closeout\RefManCut@out}
-
-
-%%% Local Variables: 
-%%% mode: latex
-%%% TeX-master: "Reference-Manual"
-%%% End: 
diff --git a/doc/refman/index.html b/doc/refman/index.html
deleted file mode 100644
index b937350e6..000000000
--- a/doc/refman/index.html
+++ /dev/null
@@ -1,14 +0,0 @@
-<HTML>
-
-<HEAD>
-
-<TITLE>The Coq Proof Assistant Reference Manual</TITLE>
-
-</HEAD>
-
-<FRAMESET ROWS=90%,*>
-  <FRAME SRC="cover.html" NAME="UP">
-  <FRAME SRC="menu.html">
-</FRAMESET>
-
-</HTML>
diff --git a/doc/refman/menu.html b/doc/refman/menu.html
deleted file mode 100644
index 7312ad344..000000000
--- a/doc/refman/menu.html
+++ /dev/null
@@ -1,32 +0,0 @@
-<HTML>
-
-<BODY>
-
-<CENTER>
-
-<TABLE BORDER="0" CELLPADDING=10>
-<TR>
-<TD><CENTER><A HREF="cover.html" TARGET="UP"><FONT SIZE=2>Cover page</FONT></A></CENTER></TD>
-<TD><CENTER><A HREF="toc.html" TARGET="UP"><FONT SIZE=2>Table of contents</FONT></A></CENTER></TD>
-<TD><CENTER><A HREF="biblio.html" TARGET="UP"><FONT SIZE=2>
-Bibliography</FONT></A></CENTER></TD>
-<TD><CENTER><A HREF="general-index.html" TARGET="UP"><FONT SIZE=2>
-Global Index
-</FONT></A></CENTER></TD>
-<TD><CENTER><A HREF="tactic-index.html" TARGET="UP"><FONT SIZE=2>
-Tactics Index
-</FONT></A></CENTER></TD>
-<TD><CENTER><A HREF="command-index.html" TARGET="UP"><FONT SIZE=2>
-Vernacular Commands Index
-</FONT></A></CENTER></TD>
-<TD><CENTER><A HREF="option-index.html" TARGET="UP"><FONT SIZE=2>
-Vernacular Options Index
-</FONT></A></CENTER></TD>
-<TD><CENTER><A HREF="error-index.html" TARGET="UP"><FONT SIZE=2>
-Index of Error Messages
-</FONT></A></CENTER></TD>
-</TABLE>
-
-</CENTER>
-
-</BODY></HTML>