Merge PR #6973: [Sphinx] migrate introduction

13 files changed, 1802 insertions, 30 deletions

diff --git a/doc/sphinx/_static/notations.css b/doc/sphinx/_static/notations.css
index 1ae7a7cd7f..9b7b826d58 100644
--- a/doc/sphinx/_static/notations.css
+++ b/doc/sphinx/_static/notations.css
@@ -158,11 +158,6 @@ dt > .property {
   color: #FFFFFF;
 }
 
-/* FIXME: Specific to the RTD theme */
-a:visited {
-    color: #2980B9;
-}
-
 /* Pygments for Coq is confused by ‘…’ */
 code span.error {
     background: inherit !important;
diff --git a/doc/sphinx/biblio.bib b/doc/sphinx/biblio.bib
new file mode 100644
index 0000000000..4a9bd6c1a0
--- /dev/null
+++ b/doc/sphinx/biblio.bib
@@ -0,0 +1,1397 @@
+@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},
+  booktitle   = {Proceedings of the 1992 Workshop on Types for Proofs and Programs}
+}
+
+@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     = {Theoretical Computer Science},
+  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.irif.fr/~letouzey/download/extraction2002.pdf}}
+}
+
+@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/sphinx/conf.py b/doc/sphinx/conf.py
index 0bff41a259..12aeee3f91 100755
--- a/doc/sphinx/conf.py
+++ b/doc/sphinx/conf.py
@@ -10,7 +10,7 @@
 ##         #     (see LICENSE file for the text of the license)         ##
 ##########################################################################
 #
-# Coq 8.5 documentation build configuration file, created by
+# Coq documentation build configuration file, created by
 # sphinx-quickstart on Wed May 11 11:23:13 2016.
 #
 # This file is execfile()d with the current directory set to its
@@ -32,6 +32,9 @@ sys.setrecursionlimit(1500)
 # add these directories to sys.path here. If the directory is relative to the
 # documentation root, use os.path.abspath to make it absolute, like shown here.
 sys.path.append(os.path.abspath('../tools/'))
+sys.path.append(os.path.abspath('../../config/'))
+
+import coq_config
 
 # -- General configuration ------------------------------------------------
 
@@ -64,7 +67,7 @@ master_doc = 'index'
 
 # General information about the project.
 project = 'Coq'
-copyright = '2016, Inria'
+copyright = '1999-2018, Inria'
 author = 'The Coq Development Team'
 
 # The version info for the project you're documenting, acts as replacement for
@@ -72,9 +75,9 @@ author = 'The Coq Development Team'
 # built documents.
 #
 # The short X.Y version.
-version = '8.7'
+version = coq_config.version
 # The full version, including alpha/beta/rc tags.
-release = '8.7.dev'
+release = coq_config.version
 
 # The language for content autogenerated by Sphinx. Refer to documentation
 # for a list of supported languages.
@@ -92,7 +95,7 @@ language = None
 # List of patterns, relative to source directory, that match files and
 # directories to ignore when looking for source files.
 # This patterns also effect to html_static_path and html_extra_path
-exclude_patterns = ['_build', 'Thumbs.db', '.DS_Store']
+exclude_patterns = ['_build', 'Thumbs.db', '.DS_Store', 'introduction.rst']
 
 # The reST default role (used for this markup: `text`) to use for all
 # documents.
@@ -143,6 +146,14 @@ html_theme = 'sphinx_rtd_theme'
 # documentation.
 #html_theme_options = {}
 
+html_context = {
+    'display_github': True,
+    'github_user': 'coq',
+    'github_repo': 'coq',
+    'github_version': 'master',
+    'conf_py_path': '/doc/sphinx/'
+}
+
 # Add any paths that contain custom themes here, relative to this directory.
 import sphinx_rtd_theme
 html_theme_path = [sphinx_rtd_theme.get_html_theme_path()]
@@ -230,9 +241,6 @@ html_use_smartypants = False # FIXME wrap code in <code> tags, otherwise quotesg
 # implements a search results scorer. If empty, the default will be used.
 #html_search_scorer = 'scorer.js'
 
-# Output file base name for HTML help builder.
-htmlhelp_basename = 'Coq85doc'
-
 # -- Options for LaTeX output ---------------------------------------------
 
 ###########################
@@ -264,10 +272,10 @@ latex_additional_files = ["_static/coqnotations.sty"]
 # Grouping the document tree into LaTeX files. List of tuples
 # (source start file, target name, title,
 #  author, documentclass [howto, manual, or own class]).
-latex_documents = [
-    (master_doc, 'Coq85.tex', 'Coq 8.5 Documentation',
-     'The Coq Development Team (edited by C. Pit-Claudel)', 'manual'),
-]
+# latex_documents = [
+#    (master_doc, 'CoqRefMan.tex', 'Coq Documentation',
+#     'The Coq Development Team', 'manual'),
+#]
 
 # The name of an image file (relative to this directory) to place at the top of
 # the title page.
@@ -294,10 +302,10 @@ latex_documents = [
 
 # One entry per manual page. List of tuples
 # (source start file, name, description, authors, manual section).
-man_pages = [
-    (master_doc, 'coq85', 'Coq 8.5 Documentation',
-     [author], 1)
-]
+#man_pages = [
+#    (master_doc, 'coq', 'Coq Documentation',
+#     [author], 1)
+#]
 
 # If true, show URL addresses after external links.
 #man_show_urls = False
@@ -308,11 +316,11 @@ man_pages = [
 # Grouping the document tree into Texinfo files. List of tuples
 # (source start file, target name, title, author,
 #  dir menu entry, description, category)
-texinfo_documents = [
-    (master_doc, 'Coq85', 'Coq 8.5 Documentation',
-     author, 'Coq85', 'One line description of project.',
-     'Miscellaneous'),
-]
+#texinfo_documents = [
+#    (master_doc, 'Coq', 'Coq Documentation',
+#     author, 'Coq', 'One line description of project.',
+#     'Miscellaneous'),
+#]
 
 # Documents to append as an appendix to all manuals.
 #texinfo_appendices = []
@@ -330,10 +338,10 @@ texinfo_documents = [
 # -- Options for Epub output ----------------------------------------------
 
 # Bibliographic Dublin Core info.
-epub_title = project
-epub_author = author
-epub_publisher = author
-epub_copyright = copyright
+#epub_title = project
+#epub_author = author
+#epub_publisher = author
+#epub_copyright = copyright
 
 # The basename for the epub file. It defaults to the project name.
 #epub_basename = project
diff --git a/doc/sphinx/coq-cmdindex.rst b/doc/sphinx/coq-cmdindex.rst
new file mode 100644
index 0000000000..7df6cb36c5
--- /dev/null
+++ b/doc/sphinx/coq-cmdindex.rst
@@ -0,0 +1,5 @@
+.. hack to get index in TOC
+
+-----------------
+Command index
+-----------------
diff --git a/doc/sphinx/coq-exnindex.rst b/doc/sphinx/coq-exnindex.rst
new file mode 100644
index 0000000000..100c57b085
--- /dev/null
+++ b/doc/sphinx/coq-exnindex.rst
@@ -0,0 +1,5 @@
+.. hack to get index in TOC
+
+----------------------
+Errors, warnings index
+----------------------
diff --git a/doc/sphinx/coq-optindex.rst b/doc/sphinx/coq-optindex.rst
new file mode 100644
index 0000000000..f8046a800b
--- /dev/null
+++ b/doc/sphinx/coq-optindex.rst
@@ -0,0 +1,5 @@
+.. hack to get index in TOC
+
+-----------------
+Option index
+-----------------
diff --git a/doc/sphinx/coq-tacindex.rst b/doc/sphinx/coq-tacindex.rst
new file mode 100644
index 0000000000..588104f465
--- /dev/null
+++ b/doc/sphinx/coq-tacindex.rst
@@ -0,0 +1,5 @@
+.. hack to get index in TOC
+
+-------------
+Tactic index
+-------------
diff --git a/doc/sphinx/genindex.rst b/doc/sphinx/genindex.rst
new file mode 100644
index 0000000000..a991c7f9f8
--- /dev/null
+++ b/doc/sphinx/genindex.rst
@@ -0,0 +1,5 @@
+.. hack to get index in TOC
+
+-----
+Index
+-----
diff --git a/doc/sphinx/index.rst b/doc/sphinx/index.rst
index e69de29bb2..7b8bc2bae6 100644
--- a/doc/sphinx/index.rst
+++ b/doc/sphinx/index.rst
@@ -0,0 +1,50 @@
+.. _introduction:
+
+.. include:: preamble.rst
+.. include:: replaces.rst
+
+Introduction
+===========================================
+
+.. include:: introduction.rst
+
+------------------
+Table of contents
+------------------
+
+.. toctree::
+   :caption: The language
+
+.. toctree::
+   :caption: The proof engine
+
+.. toctree::
+   :caption: User extensions
+
+.. toctree::
+   :caption: Practical tools
+
+.. toctree::
+   :caption: Addendum
+
+.. toctree::
+   :caption: Reference
+
+   zebibliography
+
+.. toctree::
+   :caption: Indexes
+	     
+   genindex
+   coq-cmdindex
+   coq-tacindex	      
+   coq-optindex	      
+   coq-exnindex	      
+   
+.. No entries yet
+  * :index:`thmindex`
+
+This material (the Coq Reference Manual) 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
+http://www.opencontent.org/openpub). Options A and B are not elected.
diff --git a/doc/sphinx/introduction.rst b/doc/sphinx/introduction.rst
new file mode 100644
index 0000000000..514745c1bf
--- /dev/null
+++ b/doc/sphinx/introduction.rst
@@ -0,0 +1,119 @@
+------------------------
+Introduction
+------------------------
+
+This document is the Reference Manual of version of the |Coq|  proof
+assistant. A companion volume, the |Coq| Tutorial, is provided for the
+beginners. It is advised to read the Tutorial first. A
+book :cite:`CoqArt` on practical uses of the |Coq| system was
+published in 2004 and is a good support for both the beginner and the
+advanced user.
+
+The |Coq| system is designed to develop mathematical proofs, and
+especially to write formal specifications, programs and to verify that
+programs are correct with respect to their specification. It provides a
+specification language named |Gallina|. Terms of |Gallina| can represent
+programs as well as properties of these programs and proofs of these
+properties. Using the so-called *Curry-Howard isomorphism*, programs,
+properties and proofs are formalized in the same language called
+*Calculus of Inductive Constructions*, that is a
+:math:`\lambda`-calculus with a rich type system. All logical judgments
+in |Coq| are typing judgments. The very heart of the |Coq| system is the
+type-checking algorithm that checks the correctness of proofs, in other
+words that checks that a program complies to its specification. |Coq| also
+provides an interactive proof assistant to build proofs using specific
+programs called *tactics*.
+
+All services of the |Coq| proof assistant are accessible by interpretation
+of a command language called *the vernacular*.
+
+Coq has an interactive mode in which commands are interpreted as the
+user types them in from the keyboard and a compiled mode where commands
+are processed from a file.
+
+-  The interactive mode may be used as a debugging mode in which the
+   user can develop his theories and proofs step by step, backtracking
+   if needed and so on. The interactive mode is run with the `coqtop` 
+   command from the operating system (which we shall assume to be some
+   variety of UNIX in the rest of this document).
+
+-  The compiled mode acts as a proof checker taking a file containing a
+   whole development in order to ensure its correctness. Moreover,
+   |Coq|’s compiler provides an output file containing a compact
+   representation of its input. The compiled mode is run with the `coqc`
+   command from the operating system.
+
+These two modes are documented in Chapter :ref:`thecoqcommands`.
+
+Other modes of interaction with |Coq| are possible: through an emacs shell
+window, an emacs generic user-interface for proof assistant (Proof
+General :cite:`ProofGeneral`) or through a customized
+interface (PCoq :cite:`Pcoq`). These facilities are not
+documented here. There is also a |Coq| Integrated Development Environment
+described in :ref:`coqintegrateddevelopmentenvironment`.
+
+How to read this book
+=====================
+
+This is a Reference Manual, not a User Manual, so it is not made for a
+continuous reading. However, it has some structure that is explained
+below.
+
+-  The first part describes the specification language, |Gallina|.
+   Chapters :ref:`thegallinaspecificationlanguage` and :ref:`extensionsofgallina` describe the concrete
+   syntax as well as the meaning of programs, theorems and proofs in the
+   Calculus of Inductive Constructions. Chapter :ref:`thecoqlibrary` describes the
+   standard library of |Coq|. Chapter :ref:`calculusofinductiveconstructions` is a mathematical description
+   of the formalism. Chapter :ref:`themodulesystem` describes the module
+   system.
+
+-  The second part describes the proof engine. It is divided in five
+   chapters. Chapter :ref:`vernacularcommands` presents all commands (we
+   call them *vernacular commands*) that are not directly related to
+   interactive proving: requests to the environment, complete or partial
+   evaluation, loading and compiling files. How to start and stop
+   proofs, do multiple proofs in parallel is explained in
+   Chapter :ref:`proofhandling`. In Chapter :ref:`tactics`, all commands that
+   realize one or more steps of the proof are presented: we call them
+   *tactics*. The language to combine these tactics into complex proof
+   strategies is given in Chapter :ref:`thetacticlanguage`. Examples of tactics
+   are described in Chapter :ref:`detailedexamplesoftactics`.
+
+-  The third part describes how to extend the syntax of |Coq|. It
+   corresponds to the Chapter :ref:`syntaxextensionsandinterpretationscopes`.
+
+-  In the fourth part more practical tools are documented. First in
+   Chapter :ref:`thecoqcommands`, the usage of `coqc` (batch mode) and
+   `coqtop` (interactive mode) with their options is described. Then,
+   in Chapter :ref:`utilities`, various utilities that come with the
+   |Coq| distribution are presented. Finally, Chapter :ref:`coqintegrateddevelopmentenvironment` 
+   describes the |Coq| integrated development environment.
+
+-  The fifth part documents a number of advanced features, including coercions,
+   canonical structures, typeclasses, program extraction, and specialized
+   solvers and tactics. See the table of contents for a complete list.
+
+At the end of the document, after the global index, the user can find
+specific indexes for tactics, vernacular commands, and error messages.
+
+List of additional documentation
+================================
+
+This manual does not contain all the documentation the user may need
+about |Coq|. Various informations can be found in the following documents:
+
+Tutorial
+    A companion volume to this reference manual, the |Coq| Tutorial, is
+    aimed at gently introducing new users to developing proofs in |Coq|
+    without assuming prior knowledge of type theory. In a second step,
+    the user can read also the tutorial on recursive types (document
+    `RecTutorial.ps`).
+
+Installation
+    A text file `INSTALL` that comes with the sources explains how to
+    install |Coq|.
+
+The |Coq| standard library
+    A commented version of sources of the |Coq| standard library
+    (including only the specifications, the proofs are removed) is given
+    in the additional document `Library.ps`.
diff --git a/doc/sphinx/preamble.rst b/doc/sphinx/preamble.rst
new file mode 100644
index 0000000000..395f558a85
--- /dev/null
+++ b/doc/sphinx/preamble.rst
@@ -0,0 +1,92 @@
+.. preamble::
+
+   \[
+   \newcommand{\alors}{\textsf{then}}
+   \newcommand{\alter}{\textsf{alter}}
+   \newcommand{\as}{\kw{as}}
+   \newcommand{\Assum}[3]{\kw{Assum}(#1)(#2:#3)}
+   \newcommand{\bool}{\textsf{bool}}
+   \newcommand{\case}{\kw{case}}
+   \newcommand{\conc}{\textsf{conc}}
+   \newcommand{\cons}{\textsf{cons}}
+   \newcommand{\consf}{\textsf{consf}}
+   \newcommand{\conshl}{\textsf{cons\_hl}}
+   \newcommand{\Def}[4]{\kw{Def}(#1)(#2:=#3:#4)}
+   \newcommand{\emptyf}{\textsf{emptyf}}
+   \newcommand{\End}{\kw{End}}
+   \newcommand{\endkw}{\kw{end}}
+   \newcommand{\EqSt}{\textsf{EqSt}}
+   \newcommand{\even}{\textsf{even}}
+   \newcommand{\evenO}{\textsf{even_O}}
+   \newcommand{\evenS}{\textsf{even_S}}
+   \newcommand{\false}{\textsf{false}}
+   \newcommand{\filter}{\textsf{filter}}
+   \newcommand{\Fix}{\kw{Fix}}
+   \newcommand{\fix}{\kw{fix}}
+   \newcommand{\for}{\textsf{for}}
+   \newcommand{\forest}{\textsf{forest}}
+   \newcommand{\from}{\textsf{from}}
+   \newcommand{\Functor}{\kw{Functor}}
+   \newcommand{\haslength}{\textsf{has\_length}}
+   \newcommand{\hd}{\textsf{hd}}
+   \newcommand{\ident}{\textsf{ident}}
+   \newcommand{\In}{\kw{in}}
+   \newcommand{\Ind}[4]{\kw{Ind}[#2](#3:=#4)}
+   \newcommand{\ind}[3]{\kw{Ind}~[#1]\left(#2\mathrm{~:=~}#3\right)}
+   \newcommand{\Indp}[5]{\kw{Ind}_{#5}(#1)[#2](#3:=#4)}
+   \newcommand{\Indpstr}[6]{\kw{Ind}_{#5}(#1)[#2](#3:=#4)/{#6}}
+   \newcommand{\injective}{\kw{injective}}
+   \newcommand{\kw}[1]{\textsf{#1}}
+   \newcommand{\lb}{\lambda}
+   \newcommand{\length}{\textsf{length}}
+   \newcommand{\letin}[3]{\kw{let}~#1:=#2~\kw{in}~#3}
+   \newcommand{\List}{\textsf{list}}
+   \newcommand{\lra}{\longrightarrow}
+   \newcommand{\Match}{\kw{match}}
+   \newcommand{\Mod}[3]{{\kw{Mod}}({#1}:{#2}\,\zeroone{:={#3}})}
+   \newcommand{\ModA}[2]{{\kw{ModA}}({#1}=={#2})}
+   \newcommand{\ModS}[2]{{\kw{Mod}}({#1}:{#2})}
+   \newcommand{\ModType}[2]{{\kw{ModType}}({#1}:={#2})}
+   \newcommand{\mto}{.\;}
+   \newcommand{\Nat}{\mathbb{N}}
+   \newcommand{\nat}{\textsf{nat}}
+   \newcommand{\Nil}{\textsf{nil}}
+   \newcommand{\nilhl}{\textsf{nil\_hl}}
+   \newcommand{\nO}{\textsf{O}}
+   \newcommand{\node}{\textsf{node}}
+   \newcommand{\nS}{\textsf{S}}
+   \newcommand{\odd}{\textsf{odd}}
+   \newcommand{\oddS}{\textsf{odd_S}}
+   \newcommand{\ovl}[1]{\overline{#1}}
+   \newcommand{\Pair}{\textsf{pair}}
+   \newcommand{\Prod}{\textsf{prod}}
+   \newcommand{\Prop}{\textsf{Prop}}
+   \newcommand{\return}{\kw{return}}
+   \newcommand{\Set}{\textsf{Set}}
+   \newcommand{\si}{\textsf{if}}
+   \newcommand{\sinon}{\textsf{else}}
+   \newcommand{\Sort}{\cal S}
+   \newcommand{\Str}{\textsf{Stream}}
+   \newcommand{\Struct}{\kw{Struct}}
+   \newcommand{\subst}[3]{#1\{#2/#3\}}
+   \newcommand{\tl}{\textsf{tl}}
+   \newcommand{\tree}{\textsf{tree}}
+   \newcommand{\true}{\textsf{true}}
+   \newcommand{\Type}{\textsf{Type}}
+   \newcommand{\unfold}{\textsf{unfold}}
+   \newcommand{\WEV}[3]{\mbox{$#1[] \vdash #2 \lra  #3$}}
+   \newcommand{\WEVT}[3]{\mbox{$#1[] \vdash #2 \lra$}\\ \mbox{$ #3$}}
+   \newcommand{\WF}[2]{{\cal W\!F}(#1)[#2]}
+   \newcommand{\WFE}[1]{\WF{E}{#1}}
+   \newcommand{\WFT}[2]{#1[] \vdash {\cal W\!F}(#2)}
+   \newcommand{\WFTWOLINES}[2]{{\cal W\!F}\begin{array}{l}(#1)\\\mbox{}[{#2}]\end{array}}
+   \newcommand{\with}{\kw{with}}
+   \newcommand{\WS}[3]{#1[] \vdash #2 <: #3}
+   \newcommand{\WSE}[2]{\WS{E}{#1}{#2}}
+   \newcommand{\WT}[4]{#1[#2] \vdash #3 : #4}
+   \newcommand{\WTE}[3]{\WT{E}{#1}{#2}{#3}}
+   \newcommand{\WTEG}[2]{\WTE{\Gamma}{#1}{#2}}
+   \newcommand{\WTM}[3]{\WT{#1}{}{#2}{#3}}
+   \newcommand{\zeroone}[1]{[{#1}]}
+   \newcommand{\zeros}{\textsf{zeros}}
+   \]
diff --git a/doc/sphinx/replaces.rst b/doc/sphinx/replaces.rst
new file mode 100644
index 0000000000..2c38219b97
--- /dev/null
+++ b/doc/sphinx/replaces.rst
@@ -0,0 +1,78 @@
+.. some handy replacements for common items
+
+.. role:: smallcaps
+
+.. |A_1| replace:: `A`\ :math:`_{1}`
+.. |A_n| replace:: `A`\ :math:`_{n}`
+.. |arg_1| replace:: `arg`\ :math:`_{1}`
+.. |arg_n| replace:: `arg`\ :math:`_{n}`
+.. |bdi| replace:: :math:`\beta\delta\iota`
+.. |binder_1| replace:: `binder`\ :math:`_{1}`
+.. |binder_n| replace:: `binder`\ :math:`_{n}`
+.. |binders_1| replace:: `binders`\ :math:`_{1}`
+.. |binders_n| replace:: `binders`\ :math:`_{n}`
+.. |C_1| replace:: `C`\ :math:`_{1}`
+.. |c_1| replace:: `c`\ :math:`_{1}`
+.. |C_2| replace:: `C`\ :math:`_{2}`
+.. |c_i| replace:: `c`\ :math:`_{i}`
+.. |c_n| replace:: `c`\ :math:`_{n}`
+.. |Cic| replace:: :smallcaps:`Cic`
+.. |class_1| replace:: `class`\ :math:`_{1}`
+.. |class_2| replace:: `class`\ :math:`_{2}`
+.. |Coq| replace:: :smallcaps:`Coq`
+.. |CoqIDE| replace:: :smallcaps:`CoqIDE`
+.. |eq_beta_delta_iota_zeta| replace:: `=`\ :math:`_{\small{\beta\delta\iota\zeta}}`
+.. |Gallina| replace:: :smallcaps:`Gallina`
+.. |ident_0| replace:: `ident`\ :math:`_{0}`
+.. |ident_1,1| replace:: `ident`\ :math:`_{1,1}`
+.. |ident_1,k_1| replace:: `ident`\ :math:`_{1,k_1}`)
+.. |ident_1| replace:: `ident`\ :math:`_{1}`
+.. |ident_2| replace:: `ident`\ :math:`_{2}`
+.. |ident_3| replace:: `ident`\ :math:`_{3}`
+.. |ident_i| replace:: `ident`\ :math:`_{i}`
+.. |ident_j| replace:: `ident`\ :math:`_{j}`
+.. |ident_k| replace:: `ident`\ :math:`_{k}`
+.. |ident_n,1| replace:: `ident`\ :math:`_{n,1}`
+.. |ident_n,k_n| replace:: `ident`\ :math:`_{n,k_n}`
+.. |ident_n| replace:: `ident`\ :math:`_{n}`
+.. |L_tac| replace:: `L`:sub:`tac`
+.. |ML| replace:: :smallcaps:`ML`
+.. |mod_0| replace:: `mod`\ :math:`_{0}`
+.. |mod_1| replace:: `mod`\ :math:`_{1}`
+.. |mod_2| replace:: `mod`\ :math:`_{1}`
+.. |mod_n| replace:: `mod`\ :math:`_{n}`
+.. |module_0| replace:: `module`\ :math:`_{0}`
+.. |module_1| replace:: `module`\ :math:`_{1}`
+.. |module_expression_0| replace:: `module_expression`\ :math:`_{0}`
+.. |module_expression_1| replace:: `module_expression`\ :math:`_{1}`
+.. |module_expression_i| replace:: `module_expression`\ :math:`_{i}`
+.. |module_expression_n| replace:: `module_expression`\ :math:`_{n}`
+.. |module_n| replace:: `module`\ :math:`_{n}`
+.. |module_type_0| replace:: `module_type`\ :math:`_{0}`
+.. |module_type_1| replace:: `module_type`\ :math:`_{1}`
+.. |module_type_i| replace:: `module_type`\ :math:`_{i}`
+.. |module_type_n| replace:: `module_type`\ :math:`_{n}`
+.. |N| replace:: ``N``
+.. |nat| replace:: ``nat``
+.. |Ocaml| replace:: :smallcaps:`OCaml`
+.. |p_1| replace:: `p`\ :math:`_{1}`
+.. |p_i| replace:: `p`\ :math:`_{i}`
+.. |p_n| replace:: `p`\ :math:`_{n}`
+.. |Program| replace:: :strong:`Program`
+.. |t_1| replace:: `t`\ :math:`_{1}`
+.. |t_i| replace:: `t`\ :math:`_{i}`
+.. |t_m| replace:: `t`\ :math:`_{m}`
+.. |t_n| replace:: `t`\ :math:`_{n}`
+.. |term_0| replace:: `term`\ :math:`_{0}`
+.. |term_1| replace:: `term`\ :math:`_{1}`
+.. |term_2| replace:: `term`\ :math:`_{2}`
+.. |term_n| replace:: `term`\ :math:`_{n}`
+.. |type_0| replace:: `type`\ :math:`_{0}`
+.. |type_1| replace:: `type`\ :math:`_{1}`
+.. |type_2| replace:: `type`\ :math:`_{2}`
+.. |type_3| replace:: `type`\ :math:`_{3}`
+.. |type_n| replace:: `type`\ :math:`_{n}`
+.. |x_1| replace:: `x`\ :math:`_{1}`
+.. |x_i| replace:: `x`\ :math:`_{i}`
+.. |x_n| replace:: `x`\ :math:`_{n}`
+.. |Z| replace:: ``Z``
diff --git a/doc/sphinx/zebibliography.rst b/doc/sphinx/zebibliography.rst
new file mode 100644
index 0000000000..0000caa301
--- /dev/null
+++ b/doc/sphinx/zebibliography.rst
@@ -0,0 +1,8 @@
+.. _bibliography:
+
+============
+Bibliography
+============
+
+.. bibliography:: biblio.bib
+   :cited: