Merge remote-tracking branch 'OFFICIAL/trunk' into morefresh

30 files changed, 1509 insertions, 1205 deletions

diff --git a/doc/common/macros.tex b/doc/common/macros.tex
index 0e820008ed..077e2f0dfb 100644
--- a/doc/common/macros.tex
+++ b/doc/common/macros.tex
@@ -97,8 +97,7 @@
 \newcommand{\camlpppp}{\textsc{Camlp4}}
 \newcommand{\emacs}{\textsc{GNU Emacs}}
 \newcommand{\ProofGeneral}{\textsc{Proof General}}
-\newcommand{\CIC}{\pCIC}
-\newcommand{\pCIC}{p\textsc{Cic}}
+\newcommand{\CIC}{\textsc{Cic}}
 \newcommand{\iCIC}{\textsc{Cic}}
 \newcommand{\FW}{\ensuremath{F_{\omega}}}
 \newcommand{\Program}{\textsc{Program}}
@@ -199,6 +198,7 @@
 \newcommand{\pattern}{\nterm{pattern}} % pattern for pattern-matching
 \newcommand{\orpattern}{\nterm{or\_pattern}}
 \newcommand{\intropattern}{\nterm{intro\_pattern}}
+\newcommand{\intropatternlist}{\nterm{intro\_pattern\_list}}
 \newcommand{\disjconjintropattern}{\nterm{disj\_conj\_intro\_pattern}}
 \newcommand{\namingintropattern}{\nterm{naming\_intro\_pattern}}
 \newcommand{\termpattern}{\nterm{term\_pattern}} % term with holes
@@ -258,13 +258,13 @@
 \newcommand{\forest}{\mbox{\textsf{forest}}}
 \newcommand{\from}{\mbox{\textsf{from}}}
 \newcommand{\hd}{\mbox{\textsf{hd}}}
-\newcommand{\Length}{\mbox{\textsf{Length}}}
+\newcommand{\haslength}{\mbox{\textsf{has\_length}}}
 \newcommand{\length}{\mbox{\textsf{length}}}
-\newcommand{\LengthA}{\mbox {\textsf{Length\_A}}}
-\newcommand{\List}{\mbox{\textsf{List}}}
-\newcommand{\ListA}{\mbox{\textsf{List\_A}}}
-\newcommand{\LNil}{\mbox{\textsf{Lnil}}}
-\newcommand{\LCons}{\mbox{\textsf{Lcons}}}
+\newcommand{\haslengthA}{\mbox {\textsf{has\_length~A}}}
+\newcommand{\List}{\mbox{\textsf{list}}}
+\newcommand{\ListA}{\mbox{\textsf{list}}~\ensuremath{A}}
+\newcommand{\nilhl}{\mbox{\textsf{nil\_hl}}}
+\newcommand{\conshl}{\mbox{\textsf{cons\_hl}}}
 \newcommand{\nat}{\mbox{\textsf{nat}}}
 \newcommand{\nO}{\mbox{\textsf{O}}}
 \newcommand{\nS}{\mbox{\textsf{S}}}
@@ -281,6 +281,13 @@
 \newcommand{\Type}{\mbox{\textsf{Type}}}
 \newcommand{\unfold}{\mbox{\textsf{unfold}}}
 \newcommand{\zeros}{\mbox{\textsf{zeros}}}
+\newcommand{\even}{\mbox{\textsf{even}}}
+\newcommand{\odd}{\mbox{\textsf{odd}}}
+\newcommand{\evenO}{\mbox{\textsf{even\_O}}}
+\newcommand{\evenS}{\mbox{\textsf{even\_S}}}
+\newcommand{\oddS}{\mbox{\textsf{odd\_S}}}
+\newcommand{\Prod}{\mbox{\textsf{prod}}}
+\newcommand{\Pair}{\mbox{\textsf{pair}}}
 
 %%%%%%%%%
 % Misc. %
@@ -364,6 +371,7 @@
 \newcommand{\myifthenelse}[3]{\kw{if} ~ #1 ~\kw{then} ~ #2 ~ \kw{else} ~ #3}
 \newcommand{\fun}[2]{\item[]{\tt {#1}}. \quad\\ #2}
 \newcommand{\WF}[2]{\ensuremath{{\cal W\!F}(#1)[#2]}}
+\newcommand{\WFTWOLINES}[2]{\ensuremath{{\cal W\!F}\begin{array}{l}(#1)\\\mbox{}[{#2}]\end{array}}}
 \newcommand{\WFE}[1]{\WF{E}{#1}}
 \newcommand{\WT}[4]{\ensuremath{#1[#2] \vdash #3 : #4}}
 \newcommand{\WTE}[3]{\WT{E}{#1}{#2}{#3}}
@@ -393,9 +401,9 @@
 \newcommand{\CIPI}[1]{\CIP{#1}{I}{P}}
 \newcommand{\CIF}[1]{\mbox{$\{#1\}_{f_1.. f_n}$}}
 %BEGIN LATEX
-\newcommand{\NInd}[3]{\mbox{{\sf Ind}$(#1)(\begin{array}[t]{@{}l}#2:=#3
+\newcommand{\NInd}[3]{\mbox{{\sf Ind}$(\begin{array}[t]{@{}l}#2:=#3
                                               \,)\end{array}$}}
-\newcommand{\Ind}[4]{\mbox{{\sf Ind}$(#1)[#2](\begin{array}[t]{@{}l@{}}#3:=#4
+\newcommand{\Ind}[4]{\mbox{{\sf Ind}$[#2](\begin{array}[t]{@{}l@{}}#3:=#4
                                                  \,)\end{array}$}}
 %END LATEX
 %HEVEA \newcommand{\NInd}[3]{\mbox{{\sf Ind}$(#1)(#2:=#3\,)$}}
@@ -413,6 +421,7 @@
 \newcommand{\Fix}[2]{\mbox{\tt Fix}~#1\{#2\}}
 \newcommand{\CoFix}[2]{\mbox{\tt CoFix}~#1\{#2\}}
 \newcommand{\With}[2]{\mbox{\tt ~with~}}
+\newcommand{\letin}[3]{\kw{let}~#1:=#2~\kw{in}~#3}
 \newcommand{\subst}[3]{#1\{#2/#3\}}
 \newcommand{\substs}[4]{#1\{(#2/#3)_{#4}\}}
 \newcommand{\Sort}{\mbox{$\cal S$}}
diff --git a/doc/common/styles/html/coqremote/cover.html b/doc/common/styles/html/coqremote/cover.html
index db82717094..6ec4dc1af0 100644
--- a/doc/common/styles/html/coqremote/cover.html
+++ b/doc/common/styles/html/coqremote/cover.html
@@ -60,7 +60,7 @@
   <li>V8.2 © INRIA 2008-2011</li>
   <li>V8.3 © INRIA 2010-2011</li>
   <li>V8.4 © INRIA 2012-2014</li>
-  <li>V8.5 © INRIA 2015</li>
+  <li>V8.5 © INRIA 2015-2016</li>
 </ul>
 
 <p style="text-indent:0pt">This research was partly supported by IST
diff --git a/doc/common/styles/html/simple/cover.html b/doc/common/styles/html/simple/cover.html
index 1641a1ed37..328bd68daf 100644
--- a/doc/common/styles/html/simple/cover.html
+++ b/doc/common/styles/html/simple/cover.html
@@ -38,7 +38,7 @@
   <li>V8.2 © INRIA 2008-2011</li>
   <li>V8.3 © INRIA 2010-2011</li>
   <li>V8.4 © INRIA 2012-2014</li>
-  <li>V8.5 © INRIA 2015</li>
+  <li>V8.5 © INRIA 2015-2016</li>
 </ul>
 
 <p style="text-indent:0pt">This research was partly supported by IST
diff --git a/doc/common/title.tex b/doc/common/title.tex
index 4716c3156a..0e072b6b65 100644
--- a/doc/common/title.tex
+++ b/doc/common/title.tex
@@ -45,7 +45,7 @@ V\coqversion, \today
 %END LATEX
 \copyright INRIA 1999-2004 ({\Coq} versions 7.x)
 
-\copyright INRIA 2004-2015 ({\Coq} versions 8.x)
+\copyright INRIA 2004-2016 ({\Coq} versions 8.x)
 
 #3
 \end{flushleft}
diff --git a/doc/faq/FAQ.tex b/doc/faq/FAQ.tex
index fbb866e875..48b61827d1 100644
--- a/doc/faq/FAQ.tex
+++ b/doc/faq/FAQ.tex
@@ -228,7 +228,7 @@ kernel is intentionally small to limit the risk of conceptual or
 accidental implementation bugs.
 \item[The Objective Caml compiler] The {\Coq} kernel is written using the
 Objective Caml language but it uses only the most standard features
-(no object, no label ...), so that it is highly unprobable that an
+(no object, no label ...), so that it is highly improbable that an
 Objective Caml bug breaks the consistency of {\Coq} without breaking all
 other kinds of features of {\Coq} or of other software compiled with
 Objective Caml.
@@ -710,7 +710,7 @@ There are also ``simple enough'' propositions for which you can prove
 the equality without requiring any extra axioms.  This is typically
 the case for propositions defined deterministically as a first-order
 inductive predicate on decidable sets. See for instance in question
-\ref{le-uniqueness} an axiom-free proof of the unicity of the proofs of
+\ref{le-uniqueness} an axiom-free proof of the uniqueness of the proofs of
 the proposition {\tt le m n} (less or equal on {\tt nat}).
 
 %  It is an ongoing work of research to natively include proof
@@ -1497,7 +1497,7 @@ while {\assert} is.
 
 \Question{What can I do if \Coq can not infer some implicit argument ?}
 
-You can state explicitely what this implicit argument is. See \ref{implicit}.
+You can state explicitly what this implicit argument is. See \ref{implicit}.
 
 \Question{How can I explicit some implicit argument ?}\label{implicit}
 
@@ -1625,14 +1625,14 @@ Fail Definition max (n p : nat) := if n <= p then p else n.
 As \Coq~ says, the term ``~\texttt{n <= p}~'' is a proposition, i.e. a
 statement that belongs to the mathematical world. There are many ways to
 prove such a proposition, either by some computation, or using some already
-proven theoremas. For instance, proving $3-2 \leq 2^{45503}$ is very easy,
+proven theorems. For instance, proving $3-2 \leq 2^{45503}$ is very easy,
 using some theorems on arithmetical operations. If you compute both numbers
 before comparing them, you risk to use a lot of time and space.
 
 
 On the contrary, a function for computing the greatest of two natural numbers
 is an algorithm  which, called on two natural numbers
-$n$ and $p$, determines wether $n\leq p$ or $p < n$.
+$n$ and $p$, determines whether $n\leq p$ or $p < n$.
 Such a function is a \emph{decision  procedure} for the inequality of
  \texttt{nat}.  The possibility of writing such a procedure comes 
 directly from de decidability of the order $\leq$ on natural numbers.
@@ -1706,7 +1706,7 @@ immediate, whereas one can't wait for  the result of
 
 This is normal. Your definition is a simple recursive function which
 returns a boolean value. Coq's \texttt{le\_lt\_dec} is a \emph{certified
-function}, i.e. a complex object, able not only to tell wether $n\leq p$
+function}, i.e. a complex object, able not only to tell whether $n\leq p$
 or $p<n$, but also of building a complete proof of the correct inequality.
 What make \texttt{le\_lt\_dec} inefficient for computing \texttt{min}
 and \texttt{max} is the building of a huge proof term.
@@ -2404,8 +2404,8 @@ You can use {\tt coqdoc}.
 
 \Question{How can I generate some dependency graph from my development?}
 
-You can use the tool \verb|coqgraph| developped by Philippe Audebaud in 2002.
-This tool transforms dependancies generated by \verb|coqdep| into 'dot' files which can be visualized using the Graphviz software (http://www.graphviz.org/).
+You can use the tool \verb|coqgraph| developed by Philippe Audebaud in 2002.
+This tool transforms dependencies generated by \verb|coqdep| into 'dot' files which can be visualized using the Graphviz software (http://www.graphviz.org/).
 
 \Question{How can I cite some {\Coq} in my latex document?}
 
@@ -2539,7 +2539,7 @@ modifiers keys available through GTK. The straightest way to get
 rid of the problem is to edit by hand your coqiderc (either
 \verb|/home/<user>/.config/coq/coqiderc| under Linux, or \\
 \verb|C:\Documents and Settings\<user>\.config\coq\coqiderc| under Windows) 
-    and replace any occurence of \texttt{MOD4} by \texttt{MOD1}.
+and replace any occurrence of \texttt{MOD4} by \texttt{MOD1}.
 
 
 
@@ -2638,7 +2638,7 @@ existential variable which eventually got erased by some computation.
 You may backtrack to the faulty occurrence of {\eauto} or {\eapply}
 and give the missing argument an explicit value. Alternatively, you
 can use the commands \texttt{Show Existentials.} and
-\texttt{Existential.} to display and instantiate the remainig
+\texttt{Existential.} to display and instantiate the remaining
 existential variables.
 
 
diff --git a/doc/refman/Cases.tex b/doc/refman/Cases.tex
index 4238bf6a57..a95d8114ff 100644
--- a/doc/refman/Cases.tex
+++ b/doc/refman/Cases.tex
@@ -521,6 +521,8 @@ I have a copy of {\tt b} in type {\tt listn 0} resp {\tt listn (S n')}.
 % \end{coq_example}
 
 \paragraph{Patterns in {\tt in}}
+\label{match-in-patterns}
+
 If the type of the matched term is more precise than an inductive applied to
 variables, arguments of the inductive in the {\tt in} branch can be more
 complicated patterns than a variable.
@@ -530,7 +532,7 @@ become impossible branches. In an impossible branch, you can answer
 anything but {\tt False\_rect unit} has the advantage to be subterm of
 anything. % ???
 
-To be concrete: the tail function can be written:
+To be concrete: the {\tt tail} function can be written:
 \begin{coq_example}
 Definition tail n (v: listn (S n)) :=
   match v in listn (S m) return listn m with
diff --git a/doc/refman/Coercion.tex b/doc/refman/Coercion.tex
index e4aa69353d..16006a6adf 100644
--- a/doc/refman/Coercion.tex
+++ b/doc/refman/Coercion.tex
@@ -312,12 +312,13 @@ Conversely, to skip the printing of coercions, use
  {\tt Unset Printing Coercions}.
 By default, coercions are not printed.
 
-\asubsection{\tt Set Printing Coercion {\qualid}.}
-\optindex{Printing Coercion}
+\asubsection{\tt Add Printing Coercion {\qualid}.}
+\comindex{Add Printing Coercion}
+\comindex{Remove Printing Coercion}
 
 This command forces coercion denoted by {\qualid} to be printed.
 To skip the printing of coercion {\qualid}, use
- {\tt Unset Printing Coercion {\qualid}}.
+ {\tt Remove Printing Coercion {\qualid}}.
 By default, a coercion is never printed.
  
 \asection{Classes as Records}
diff --git a/doc/refman/Extraction.tex b/doc/refman/Extraction.tex
index 74c8374de4..a963662f64 100644
--- a/doc/refman/Extraction.tex
+++ b/doc/refman/Extraction.tex
@@ -198,6 +198,11 @@ this constant is not declared in the generated file.
 
 \asubsection{Extra elimination of useless arguments}
 
+The following command provides some extra manual control on the
+code elimination performed during extraction, in a way which
+is independent but complementary to the main elimination
+principles of extraction (logical parts and types).
+
 \begin{description}
 \item \comindex{Extraction Implicit}
  {\tt Extraction Implicit} \qualid\ [ \ident$_1$ \dots\ \ident$_n$ ].
@@ -207,12 +212,27 @@ This experimental command allows declaring some arguments of
 be removed by extraction. Here \qualid\ can be any function or
 inductive constructor, and \ident$_i$ are the names of the concerned
 arguments. In fact, an argument can also be referred by a number
-indicating its position, starting from 1. When an actual extraction
-takes place, an error is raised if the {\tt Extraction Implicit}
+indicating its position, starting from 1.
+\end{description}
+
+When an actual extraction takes place, an error is normally raised if the
+{\tt Extraction Implicit}
 declarations cannot be honored, that is if any of the implicited
-variables still occurs in the final code. This declaration of useless
-arguments is independent but complementary to the main elimination
-principles of extraction (logical parts and types).
+variables still occurs in the final code. This behavior can be relaxed
+via the following option:
+
+\begin{description}
+\item \optindex{Extraction SafeImplicits} {\tt Unset Extraction SafeImplicits.}
+
+Default is Set. When this option is Unset, a warning is emitted
+instead of an error if some implicited variables still occur in the
+final code of an extraction. This way, the extracted code may be
+obtained nonetheless and reviewed manually to locate the source of the issue
+(in the code, some comments mark the location of these remaining
+implicited variables).
+Note that this extracted code might not compile or run properly,
+depending of the use of these remaining implicited variables.
+
 \end{description}
 
 \asubsection{Realizing axioms}\label{extraction:axioms}
diff --git a/doc/refman/Program.tex b/doc/refman/Program.tex
index efcc84ee98..11dd3a0517 100644
--- a/doc/refman/Program.tex
+++ b/doc/refman/Program.tex
@@ -201,7 +201,7 @@ in their context. In this case, the obligations should be transparent
 recursive calls can be checked by the
 kernel's type-checker. There is an optimization in the generation of
 obligations which gets rid of the hypothesis corresponding to the
-functionnal when it is not necessary, so that the obligation can be
+functional when it is not necessary, so that the obligation can be
 declared opaque (e.g. using {\tt Qed}). However, as soon as it appears in the
 context, the proof of the obligation is \emph{required} to be declared transparent.
 
@@ -216,7 +216,7 @@ properties. It will generate obligations, try to solve them
 automatically and fail if some unsolved obligations remain. 
 In this case, one can first define the lemma's
 statement using {\tt Program Definition} and use it as the goal afterwards.
-Otherwise the proof will be started with the elobarted version as a goal.
+Otherwise the proof will be started with the elaborated version as a goal.
 The {\tt Program} prefix can similarly be used as a prefix for {\tt Variable}, {\tt
   Hypothesis}, {\tt Axiom} etc...
 
diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex
index 3fd5ae0b24..1554ee04d3 100644
--- a/doc/refman/RefMan-cic.tex
+++ b/doc/refman/RefMan-cic.tex
@@ -1,89 +1,35 @@
 \chapter[Calculus of Inductive Constructions]{Calculus of Inductive Constructions
 \label{Cic}
 \index{Cic@\textsc{CIC}}
-\index{pCic@p\textsc{CIC}}
-\index{Calculus of (Co)Inductive Constructions}}
+\index{Calculus of Inductive Constructions}}
 
 The underlying formal language of {\Coq} is a {\em Calculus of
-  Constructions} with {\em Inductive Definitions}.  It is presented in
-this chapter.  
-For {\Coq} version V7, this Calculus was known as the
-{\em Calculus of (Co)Inductive Constructions}\index{Calculus of
-  (Co)Inductive Constructions} (\iCIC\ in short).
-The underlying calculus of {\Coq} version V8.0 and up is a weaker
-  calculus where the sort \Set{} satisfies predicative rules. 
-We call this calculus the 
-{\em Predicative Calculus of (Co)Inductive
-  Constructions}\index{Predicative Calculus of
-  (Co)Inductive Constructions} (\pCIC\ in short).
-In Section~\ref{impredicativity} we give the extra-rules for \iCIC. A
-  compiling option of \Coq{} allows type-checking theories in this
-  extended system.
-
-In \CIC\, all objects have a {\em type}. There are types for functions (or
+Inductive Constructions} (\CIC) whose inference rules are presented in
+this chapter. The history of this formalism as well as pointers to related work
+are provided in a separate chapter; see {\em Credits}.
+
+\section[The terms]{The terms\label{Terms}}
+
+The expressions of the {\CIC} are {\em terms} and all terms have a {\em type}.
+There are types for functions (or
 programs), there are atomic types (especially datatypes)... but also
 types for proofs and types for the types themselves.
 Especially, any object handled in the formalism must belong to a
-type.  For instance, the statement {\it ``for all x, P''} is not
-allowed in type theory; you must say instead: {\it ``for all x
-belonging to T, P''}. The expression {\it ``x belonging to T''} is
-written {\it ``x:T''}. One also says: {\it ``x has type T''}.
-The terms of {\CIC} are detailed in Section~\ref{Terms}.
-
-In \CIC\, there is an internal reduction mechanism. In particular, it
-can decide if two programs are {\em intentionally} equal (one
-says {\em convertible}). Convertibility is presented in section 
-\ref{convertibility}.
-
-The remaining sections are concerned with the type-checking of terms.
-The beginner can skip them.
-
-The reader seeking a background on the Calculus of Inductive
-Constructions may read several papers. Giménez and Castéran~\cite{GimCas05}
-provide
-an introduction to inductive and co-inductive definitions in Coq. In
-their book~\cite{CoqArt}, Bertot and Castéran give a precise
-description of the \CIC{} based on numerous practical examples.
-Barras~\cite{Bar99}, Werner~\cite{Wer94} and
-Paulin-Mohring~\cite{Moh97} are the most recent theses dealing with
-Inductive Definitions. Coquand-Huet~\cite{CoHu85a,CoHu85b,CoHu86}
-introduces the Calculus of Constructions. Coquand-Paulin~\cite{CoPa89}
-extended this calculus to inductive definitions. The {\CIC} is a
-formulation of type theory including the possibility of inductive
-constructions, Barendregt~\cite{Bar91} studies the modern form of type
-theory.
+type.  For instance, universal quantification is relative to a type and
+takes the form {\it ``for all x
+of type T, P''}. The expression {\it ``x of type T''} is
+written {\it ``x:T''}. Informally, {\it ``x:T''} can be thought as
+{\it ``x belongs to T''}.
 
-\section[The terms]{The terms\label{Terms}}
-
-In most type theories, one usually makes a syntactic distinction
-between types and terms. This is not the case for \CIC\ which defines
-both types and terms in the same syntactical structure. This is
-because the type-theory itself forces terms and types to be defined in
-a mutual recursive way and also because similar constructions can be
-applied to both terms and types and consequently can share the same
-syntactic structure.
-
-Consider for instance the $\ra$ constructor and assume \nat\ is the
-type of natural numbers. Then $\ra$ is used both to denote
-$\nat\ra\nat$ which is the type of functions from \nat\ to \nat, and
-to denote $\nat \ra \Prop$ which is the type of unary predicates over
-the natural numbers. Consider abstraction which builds functions. It
-serves to build ``ordinary'' functions as $\kw{fun}~x:\nat \Ra ({\tt mult} ~x~x)$ (assuming {\tt mult} is already defined) but may build also 
-predicates over the natural numbers. For instance $\kw{fun}~x:\nat \Ra
-(x=x)$ will
-represent a predicate $P$, informally written in mathematics
-$P(x)\equiv x=x$. If $P$ has type $\nat \ra \Prop$, $(P~x)$ is a
-proposition, furthermore $\kw{forall}~x:\nat,(P~x)$ will represent the type of
-functions which associate to each natural number $n$ an object of
-type $(P~n)$ and consequently represent proofs of the formula
-``$\forall x.P(x)$''.
+The types of types are {\em sorts}. Types and sorts are themselves
+terms so that terms, types and sorts are all components of a common
+syntactic language of terms which is described in
+Section~\ref{cic:terms} but, first, we describe sorts.
 
 \subsection[Sorts]{Sorts\label{Sorts}
 \index{Sorts}}
-When manipulated as terms, types have themselves a type which is called a sort.
-
-There is an infinite well-founded typing hierarchy of sorts whose base
-sorts are {\Prop} and {\Set}.
+All sorts have a type and there is an infinite well-founded
+typing hierarchy of sorts whose base sorts are {\Prop} and {\Set}.
 
 The sort {\Prop} intends to be the type of logical propositions. If
 $M$ is a logical proposition then it denotes the class of terms
@@ -97,7 +43,7 @@ function types over these data types.
 
 {\Prop} and {\Set} themselves can be manipulated as ordinary
 terms. Consequently they also have a type. Because assuming simply
-that {\Set} has type {\Set} leads to an inconsistent theory, the
+that {\Set} has type {\Set} leads to an inconsistent theory~\cite{Coq86}, the
 language of {\CIC} has infinitely many sorts. There are, in addition
 to {\Set} and {\Prop} a hierarchy of universes {\Type$(i)$} for any
 integer $i$.
@@ -109,242 +55,275 @@ sets, namely the sorts {\Set} and {\Type$(j)$} for $j<i$, and all
 products, subsets and function types over these sorts.
 
 Formally, we call {\Sort} the set of sorts which is defined by:
-\[\Sort \equiv \{\Prop,\Set,\Type(i)| i \in \NN\} \]
-\index{Type@{\Type}}
-\index{Prop@{\Prop}}
-\index{Set@{\Set}}
-
-The sorts enjoy the following properties\footnote{In the Reference
-  Manual of versions of Coq prior to 8.4, the level of {\Type} typing
-  {\Prop} and {\Set} was numbered $0$. From Coq 8.4, it started to be
-  numbered $1$ so as to be able to leave room for re-interpreting
-  {\Set} in the hierarchy as {\Type$(0)$}. This change also put the
-  reference manual in accordance with the internal conventions adopted
-  in the implementation.}: {\Prop:\Type$(1)$}, {\Set:\Type$(1)$} and
-{\Type$(i)$:\Type$(i+1)$}.
-
-The user will never mention explicitly the index $i$ when referring to
+\index{Type@{\Type}}%
+\index{Prop@{\Prop}}%
+\index{Set@{\Set}}%
+\[\Sort \equiv \{\Prop,\Set,\Type(i)\;|\; i \in \NN\} \]
+Their properties, such as:
+{\Prop:\Type$(1)$}, {\Set:\Type$(1)$}, and {\Type$(i)$:\Type$(i+1)$},
+are defined in Section~\ref{subtyping-rules}.
+
+The user does not have to mention explicitly the index $i$ when referring to
 the universe \Type$(i)$. One only writes \Type. The
 system itself generates for each instance of \Type\ a new
 index for the universe and checks that the constraints between these
 indexes can be solved. From the user point of view we consequently
-have {\sf Type :Type}.
-
+have {\Type}:{\Type}.
 We shall make precise in the typing rules the constraints between the
 indexes. 
 
 \paragraph{Implementation issues}
-In practice, the {\Type} hierarchy is implemented using algebraic
-universes. An algebraic universe $u$ is either a variable (a qualified
+In practice, the {\Type} hierarchy is implemented using
+{\em algebraic universes}\index{algebraic universe}.
+An algebraic universe $u$ is either a variable (a qualified
 identifier with a number) or a successor of an algebraic universe (an
 expression $u+1$), or an upper bound of algebraic universes (an
 expression $max(u_1,...,u_n)$), or the base universe (the expression
 $0$) which corresponds, in the arity of sort-polymorphic inductive
-types, to the predicative sort {\Set}. A graph of constraints between
+types (see Section \ref{Sort-polymorphism-inductive}),
+to the predicative sort {\Set}. A graph of constraints between
 the universe variables is maintained globally. To ensure the existence
 of a mapping of the universes to the positive integers, the graph of
 constraints must remain acyclic.  Typing expressions that violate the
 acyclicity of the graph of constraints results in a \errindex{Universe
 inconsistency} error (see also Section~\ref{PrintingUniverses}).
 
-\subsection{Constants}
-Besides the sorts, the language also contains constants denoting
-objects in the environment. These constants may denote previously
-defined objects but also objects related to inductive definitions
-(either the type itself or one of its constructors or destructors).
-
-\medskip\noindent {\bf Remark. } In other presentations of \CIC, 
-the inductive objects are not seen as
-external declarations but as first-class terms. Usually the
-definitions are also completely ignored.  This is a nice theoretical
-point of view but not so practical. An inductive definition is
-specified by a possibly huge set of declarations, clearly we want to
-share this specification among the various inductive objects and not
-to duplicate it. So the specification should exist somewhere and the
-various objects should refer to it.  We choose one more level of
-indirection where the objects are just represented as constants and
-the environment gives the information on the kind of object the
-constant refers to.
-
-\medskip
-Our inductive objects will be manipulated as constants declared in the
-environment. This roughly corresponds to the way they are actually
-implemented in the \Coq\ system. It is simple to map this presentation
-in a theory where inductive objects are represented by terms.
+%% HH: This looks to me more like source of confusion than helpful
+
+%% \subsection{Constants}
+
+%% Constants refers to
+%% objects in the global environment. These constants may denote previously
+%% defined objects, but also objects related to inductive definitions
+%% (either the type itself or one of its constructors or destructors).
+
+%% \medskip\noindent {\bf Remark. } In other presentations of \CIC, 
+%% the inductive objects are not seen as
+%% external declarations but as first-class terms. Usually the
+%% definitions are also completely ignored.  This is a nice theoretical
+%% point of view but not so practical. An inductive definition is
+%% specified by a possibly huge set of declarations, clearly we want to
+%% share this specification among the various inductive objects and not
+%% to duplicate it. So the specification should exist somewhere and the
+%% various objects should refer to it.  We choose one more level of
+%% indirection where the objects are just represented as constants and
+%% the environment gives the information on the kind of object the
+%% constant refers to.
+
+%% \medskip
+%% Our inductive objects will be manipulated as constants declared in the
+%% environment. This roughly corresponds to the way they are actually
+%% implemented in the \Coq\ system. It is simple to map this presentation
+%% in a theory where inductive objects are represented by terms.
 
 \subsection{Terms}
+\label{cic:terms}
 
-Terms are built from variables, global names, constructors,
-abstraction, application, local declarations bindings (``let-in''
-expressions) and product.
-
+Terms are built from sorts, variables, constants,
+%constructors, inductive types,
+abstractions, applications, local definitions,
+%case analysis, fixpoints, cofixpoints
+and products.
 From a syntactic point of view, types cannot be distinguished from terms,
-except that they cannot start by an abstraction, and that if a term is
-a sort or a product, it should be a type.
-
+except that they cannot start by an abstraction or a constructor.
 More precisely the language of the {\em Calculus of Inductive
-  Constructions} is built from the following rules:
-
+  Constructions} is built from the following rules.
+%
 \begin{enumerate}
-\item the sorts {\sf Set, Prop, Type} are terms.
-\item names for global constants of the environment are terms.
-\item variables are terms.
-\item if $x$ is a variable and $T$, $U$ are terms then $\forall~x:T,U$
-  ($\kw{forall}~x:T,U$ in \Coq{} concrete syntax) is a term. If $x$
+\item the sorts {\Set}, {\Prop}, ${\Type(i)}$ are terms.
+\item variables, hereafter ranged over by letters $x$, $y$, etc., are terms
+\item constants, hereafter ranged over by letters $c$, $d$, etc.,  are terms.
+%\item constructors, hereafter ranged over by letter $C$, are terms.
+%\item inductive types, hereafter ranged over by letter $I$, are terms.
+\item\index{products} if $x$ is a variable and $T$, $U$ are terms then $\forall~x:T,U$
+  ($\kw{forall}~x:T,~U$ in \Coq{} concrete syntax) is a term. If $x$
   occurs in $U$, $\forall~x:T,U$ reads as {\it ``for all x of type T,
     U''}. As $U$ depends on $x$, one says that $\forall~x:T,U$ is a
-  {\em dependent product}. If $x$ doesn't occurs in $U$ then
-  $\forall~x:T,U$ reads as {\it ``if T then U''}. A non dependent
-  product can be written: $T \rightarrow U$.
-\item if $x$ is a variable and $T$, $U$ are terms then $\lb x:T \mto U$
-  ($\kw{fun}~x:T\Ra U$ in \Coq{} concrete syntax) is a term. This is a
+  {\em dependent product}. If $x$ does not occur in $U$ then
+  $\forall~x:T,U$ reads as {\it ``if T then U''}. A {\em non dependent
+  product} can be written: $T \ra U$.
+\item if $x$ is a variable and $T$, $u$ are terms then $\lb x:T \mto u$
+  ($\kw{fun}~x:T~ {\tt =>}~ u$ in \Coq{} concrete syntax) is a term. This is a
   notation for the $\lambda$-abstraction of
   $\lambda$-calculus\index{lambda-calculus@$\lambda$-calculus}
-  \cite{Bar81}. The term $\lb x:T \mto U$ is a function which maps
-  elements of $T$ to $U$.
-\item if $T$ and $U$ are terms then $(T\ U)$ is a term  
- ($T~U$ in \Coq{} concrete syntax).  The term $(T\ 
-  U)$ reads as {\it ``T applied to U''}.
-\item if $x$ is a variable, and $T$, $U$ are terms then
-  $\kw{let}~x:=T~\kw{in}~U$ is a
-  term which denotes the term $U$ where the variable $x$ is locally
-  bound to $T$. This stands for the common ``let-in'' construction of
-  functional programs such as ML or Scheme.
+  \cite{Bar81}. The term $\lb x:T \mto u$ is a function which maps
+  elements of $T$ to the expression $u$.
+\item if $t$ and $u$ are terms then $(t\ u)$ is a term  
+ ($t~u$ in \Coq{} concrete syntax).  The term $(t\ 
+  u)$ reads as {\it ``t applied to u''}.
+\item if $x$ is a variable, and $t$, $T$ and $u$ are terms then
+  $\kw{let}~x:=t:T~\kw{in}~u$ is a
+  term which denotes the term $u$ where the variable $x$ is locally
+  bound to $t$ of type $T$. This stands for the common ``let-in''
+  construction of functional programs such as ML or Scheme.
+%\item case ...
+%\item fixpoint ...
+%\item cofixpoint ...
 \end{enumerate}
 
-\paragraph{Notations.} Application associates to the left such that
-$(t~t_1\ldots t_n)$ represents $(\ldots (t~t_1)\ldots t_n)$. The
-products and arrows associate to the right such that $\forall~x:A,B\ra C\ra
-D$ represents $\forall~x:A,(B\ra (C\ra D))$.  One uses sometimes
-$\forall~x~y:A,B$ or
-$\lb x~y:A\mto B$ to denote the abstraction or product of several variables
-of the same type. The equivalent formulation is $\forall~x:A, \forall y:A,B$ or
-$\lb x:A \mto \lb y:A \mto B$
-
 \paragraph{Free variables.}
 The notion of free variables is defined as usual.  In the expressions
 $\lb x:T\mto U$ and $\forall x:T, U$ the occurrences of $x$ in $U$
-are bound.  They are represented by de Bruijn indexes in the internal
-structure of terms.
+are bound.
 
 \paragraph[Substitution.]{Substitution.\index{Substitution}}
 The notion of substituting a term $t$ to free occurrences of a
 variable $x$ in a term $u$ is defined as usual. The resulting term
 is written $\subst{u}{x}{t}$.
 
-
-\section[Typed terms]{Typed terms\label{Typed-terms}}
+\paragraph[The logical vs programming readings.]{The logical vs programming readings.}
+
+The constructions of the {\CIC} can be used to express both logical
+and programming notions, accordingly to the Curry-Howard
+correspondence between proofs and programs, and between propositions
+and types~\cite{Cur58,How80,Bru72}.
+
+For instance, let us assume that \nat\ is the type of natural numbers
+with zero element written $0$ and that ${\tt True}$ is the always true
+proposition.  Then $\ra$ is used both to denote $\nat\ra\nat$ which is
+the type of functions from \nat\ to \nat, to denote ${\tt True}\ra{\tt
+  True}$ which is an implicative proposition, to denote $\nat \ra
+\Prop$ which is the type of unary predicates over the natural numbers,
+etc.
+
+Let us assume that ${\tt mult}$ is a function of type $\nat\ra\nat\ra
+\nat$ and ${\tt eqnat}$ a predicate of type $\nat\ra\nat\ra \Prop$.
+The $\lambda$-abstraction can serve to build ``ordinary'' functions as
+in $\lambda x:\nat.({\tt mult}~x~x)$ (i.e. $\kw{fun}~x:\nat ~{\tt =>}~
+{\tt mult} ~x~x$ in {\Coq} notation) but may build also predicates
+over the natural numbers. For instance $\lambda x:\nat.({\tt eqnat}~
+x~0)$ (i.e. $\kw{fun}~x:\nat ~{\tt =>}~ {\tt eqnat}~ x~0$ in {\Coq}
+notation) will represent the predicate of one variable $x$ which
+asserts the equality of $x$ with $0$. This predicate has type $\nat
+\ra \Prop$ and it can be applied to any expression of type ${\nat}$,
+say $t$, to give an object $P~t$ of type \Prop, namely a proposition.
+
+Furthermore $\kw{forall}~x:\nat,\,P\;x$ will represent the type of
+functions which associate to each natural number $n$ an object of type
+$(P~n)$ and consequently represent the type of proofs of the formula
+``$\forall x.\,P(x)$''.
+
+\section[Typing rules]{Typing rules\label{Typed-terms}}
 
 As objects of type theory, terms are subjected to {\em type
-discipline}. The well typing of a term depends on an environment which
-consists in a global environment (see below) and a local context.
-
-\paragraph{Local context.}
-A {\em local context} (or shortly context) is an ordered list of
-declarations of variables. The declaration of some variable $x$ is
-either an assumption, written $x:T$ ($T$ is a type) or a definition,
-written $x:=t:T$.  We use brackets to write contexts. A
+discipline}. The well typing of a term depends on
+a global environment and a local context.
+
+\paragraph{Local context.\index{Local context}}
+A {\em local context} is an ordered list of
+{\em local declarations\index{declaration!local}} of names which we call {\em variables\index{variable}}.
+The declaration of some variable $x$ is
+either a {\em local assumption\index{assumption!local}}, written $x:T$ ($T$ is a type) or a {\em local definition\index{definition!local}},
+written $x:=t:T$.  We use brackets to write local contexts. A
 typical example is $[x:T;y:=u:U;z:V]$.  Notice that the variables
-declared in a context must be distinct. If $\Gamma$ declares some $x$,
+declared in a local context must be distinct. If $\Gamma$ declares some $x$,
 we write $x \in \Gamma$. By writing $(x:T) \in \Gamma$ we mean that
 either $x:T$ is an assumption in $\Gamma$ or that there exists some $t$ such
 that $x:=t:T$ is a definition in $\Gamma$. If $\Gamma$ defines some
-$x:=t:T$, we also write $(x:=t:T) \in \Gamma$.  Contexts must be
-themselves {\em well formed}.  For the rest of the chapter, the
-notation $\Gamma::(y:T)$ (resp. $\Gamma::(y:=t:T)$) denotes the context
-$\Gamma$ enriched with the declaration $y:T$ (resp. $y:=t:T$). The
-notation $[]$ denotes the empty context.  \index{Context}
+$x:=t:T$, we also write $(x:=t:T) \in \Gamma$.
+For the rest of the chapter, the $\Gamma::(y:T)$ denotes the local context
+$\Gamma$ enriched with the local assumption $y:T$.
+Similarly, $\Gamma::(y:=t:T)$ denotes the local context
+$\Gamma$ enriched with the local definition $(y:=t:T)$.
+The notation $[]$ denotes the empty local context.
+By $\Gamma_1; \Gamma_2$ we mean concatenation of the local context $\Gamma_1$
+and the local context $\Gamma_2$.
 
 % Does not seem to be used further...
 % Si dans l'explication WF(E)[Gamma] concernant les constantes
 % definies ds un contexte
 
-We define the inclusion of two contexts $\Gamma$ and $\Delta$ (written
-as $\Gamma \subset \Delta$) as the property, for all variable $x$,
-type $T$ and term $t$, if $(x:T) \in \Gamma$ then $(x:T) \in \Delta$
-and if $(x:=t:T) \in \Gamma$ then $(x:=t:T) \in \Delta$.  
+%We define the inclusion of two local contexts $\Gamma$ and $\Delta$ (written
+%as $\Gamma \subset \Delta$) as the property, for all variable $x$,
+%type $T$ and term $t$, if $(x:T) \in \Gamma$ then $(x:T) \in \Delta$
+%and if $(x:=t:T) \in \Gamma$ then $(x:=t:T) \in \Delta$.
 %We write
 % $|\Delta|$ for the length of the context $\Delta$, that is for the number
 % of declarations (assumptions or definitions) in $\Delta$.
 
-A variable $x$ is said to be free in $\Gamma$ if $\Gamma$ contains a
-declaration $y:T$ such that $x$ is free in $T$.
-
-\paragraph[Environment.]{Environment.\index{Environment}}
-Because we are manipulating global declarations (constants and global
-assumptions), we also need to consider a global environment $E$.
-
-An environment is an ordered list of declarations of global
-names. Declarations are either assumptions or ``standard''
-definitions, that is abbreviations for well-formed terms
-but also definitions of inductive objects. In the latter
-case, an object in the environment will define one or more constants
-(that is types and constructors, see Section~\ref{Cic-inductive-definitions}).
-
-An assumption will be represented in the environment as
-\Assum{\Gamma}{c}{T} which means that $c$ is assumed of some type $T$
-well-defined in some context $\Gamma$. An (ordinary) definition will
-be represented in the environment as \Def{\Gamma}{c}{t}{T} which means
-that $c$ is a constant which is valid in some context $\Gamma$ whose
-value is $t$ and type is $T$.
-
-The rules for inductive definitions (see section
+\paragraph[Global environment.]{Global environment.\index{Global environment}}
+%Because we are manipulating global declarations (global constants and global
+%assumptions), we also need to consider a global environment $E$.
+
+A {\em global environment} is an ordered list of {\em global declarations\index{declaration!global}}.
+Global declarations are either {\em global assumptions\index{assumption!global}} or {\em global
+definitions\index{definition!global}}, but also declarations of inductive objects. Inductive objects themselves declare both inductive or coinductive types and constructors
+(see Section~\ref{Cic-inductive-definitions}).
+
+A {\em global assumption} will be represented in the global environment as
+$(c:T)$ which assumes the name $c$ to be of some type $T$.
+A {\em global definition} will
+be represented in the global environment as $c:=t:T$ which defines
+the name $c$ to have value $t$ and type $T$.
+We shall call such names {\em constants}.
+For the rest of the chapter, the $E;c:T$ denotes the global environment
+$E$ enriched with the global assumption $c:T$.
+Similarly, $E;c:=t:T$ denotes the global environment
+$E$ enriched with the global definition $(c:=t:T)$.
+
+The rules for inductive definitions (see Section
 \ref{Cic-inductive-definitions}) have to be considered as assumption
 rules to which the following definitions apply: if the name $c$ is
 declared in $E$, we write $c \in E$ and if $c:T$ or $c:=t:T$ is
 declared in $E$, we write $(c : T) \in E$.
 
 \paragraph[Typing rules.]{Typing rules.\label{Typing-rules}\index{Typing rules}}
-In the following, we assume $E$ is a valid environment w.r.t.
-inductive definitions.  We define simultaneously two
+In the following, we define simultaneously two
 judgments.  The first one \WTEG{t}{T} means the term $t$ is well-typed
-and has type $T$ in the environment $E$ and context $\Gamma$.  The
-second judgment \WFE{\Gamma} means that the environment $E$ is
-well-formed and the context $\Gamma$ is a valid context in this
-environment.  It also means a third property which makes sure that any
-constant in $E$ was defined in an environment which is included in
-$\Gamma$
-\footnote{This requirement could be relaxed if we instead introduced
-  an explicit mechanism for instantiating constants. At the external
-  level, the Coq engine works accordingly to this view that all the
-  definitions in the environment were built in a sub-context of the
-  current context.}.
-
-A term $t$ is well typed in an environment $E$ iff there exists a
-context $\Gamma$ and a term $T$ such that the judgment \WTEG{t}{T} can
+and has type $T$ in the global environment $E$ and local context $\Gamma$.  The
+second judgment \WFE{\Gamma} means that the global environment $E$ is
+well-formed and the local context $\Gamma$ is a valid local context in this
+global environment.
+% HH: This looks to me complicated. I think it would be better to talk
+% about ``discharge'' as a transformation of global environments,
+% rather than as keeping a local context next to global constants.
+%
+%%  It also means a third property which makes sure that any
+%%constant in $E$ was defined in an environment which is included in
+%%$\Gamma$
+%%\footnote{This requirement could be relaxed if we instead introduced
+%%  an explicit mechanism for instantiating constants. At the external
+%%  level, the Coq engine works accordingly to this view that all the
+%%  definitions in the environment were built in a local sub-context of the
+%%  current local context.}.
+
+A term $t$ is well typed in a global environment $E$ iff there exists a
+local context $\Gamma$ and a term $T$ such that the judgment \WTEG{t}{T} can
 be derived from the following rules.
 \begin{description}
-\item[W-E] \inference{\WF{[]}{[]}}
-\item[W-S]  % Ce n'est pas vrai : x peut apparaitre plusieurs fois dans Gamma
-\inference{\frac{\WTEG{T}{s}~~~~s \in \Sort~~~~x \not\in
-      \Gamma           % \cup E
-      }
-      {\WFE{\Gamma::(x:T)}}~~~~~
-    \frac{\WTEG{t}{T}~~~~x \not\in
-      \Gamma           % \cup E
+\item[W-Empty] \inference{\WF{[]}{}}
+\item[W-Local-Assum]  % Ce n'est pas vrai : x peut apparaitre plusieurs fois dans Gamma
+\inference{\frac{\WTEG{T}{s}~~~~s \in \Sort~~~~x \not\in \Gamma % \cup E
+      }{\WFE{\Gamma::(x:T)}}}
+\item[W-Local-Def]
+\inference{\frac{\WTEG{t}{T}~~~~x \not\in \Gamma % \cup E
      }{\WFE{\Gamma::(x:=t:T)}}}
-\item[Def] \inference{\frac{\WTEG{t}{T}~~~c \notin E \cup \Gamma}
-                      {\WF{E;\Def{\Gamma}{c}{t}{T}}{\Gamma}}}
-\item[Assum] \inference{\frac{\WTEG{T}{s}~~~~s \in \Sort~~~~c \notin E \cup \Gamma}
-                      {\WF{E;\Assum{\Gamma}{c}{T}}{\Gamma}}}
-\item[Ax] \index{Typing rules!Ax}
-\inference{\frac{\WFE{\Gamma}}{\WTEG{\Prop}{\Type(p)}}~~~~~
-\frac{\WFE{\Gamma}}{\WTEG{\Set}{\Type(q)}}}
-\inference{\frac{\WFE{\Gamma}~~~~i<j}{\WTEG{\Type(i)}{\Type(j)}}}
+\item[W-Global-Assum] \inference{\frac{\WTE{}{T}{s}~~~~s \in \Sort~~~~c \notin E}
+                      {\WF{E;c:T}{}}}
+\item[W-Global-Def] \inference{\frac{\WTE{}{t}{T}~~~c \notin E}
+                      {\WF{E;c:=t:T}{}}}
+\item[Ax-Prop] \index{Typing rules!Ax-Prop}
+\inference{\frac{\WFE{\Gamma}}{\WTEG{\Prop}{\Type(1)}}}
+\item[Ax-Set] \index{Typing rules!Ax-Set}
+\inference{\frac{\WFE{\Gamma}}{\WTEG{\Set}{\Type(1)}}}
+\item[Ax-Type] \index{Typing rules!Ax-Type}
+\inference{\frac{\WFE{\Gamma}}{\WTEG{\Type(i)}{\Type(i+1)}}}
 \item[Var]\index{Typing rules!Var}
  \inference{\frac{ \WFE{\Gamma}~~~~~(x:T) \in \Gamma~~\mbox{or}~~(x:=t:T) \in \Gamma~\mbox{for some $t$}}{\WTEG{x}{T}}}
 \item[Const]  \index{Typing rules!Const}
 \inference{\frac{\WFE{\Gamma}~~~~(c:T) \in E~~\mbox{or}~~(c:=t:T) \in E~\mbox{for some $t$} }{\WTEG{c}{T}}}
-\item[Prod]  \index{Typing rules!Prod}
+\item[Prod-Prop]  \index{Typing rules!Prod-Prop}
 \inference{\frac{\WTEG{T}{s}~~~~s \in \Sort~~~
     \WTE{\Gamma::(x:T)}{U}{\Prop}}
       { \WTEG{\forall~x:T,U}{\Prop}}} 
+\item[Prod-Set]  \index{Typing rules!Prod-Set}
 \inference{\frac{\WTEG{T}{s}~~~~s \in\{\Prop, \Set\}~~~~~~
     \WTE{\Gamma::(x:T)}{U}{\Set}}
       { \WTEG{\forall~x:T,U}{\Set}}} 
-\inference{\frac{\WTEG{T}{\Type(i)}~~~~i\leq k~~~
-    \WTE{\Gamma::(x:T)}{U}{\Type(j)}~~~j \leq k}
-    {\WTEG{\forall~x:T,U}{\Type(k)}}}
+\item[Prod-Type]  \index{Typing rules!Prod-Type}
+\inference{\frac{\WTEG{T}{\Type(i)}~~~~
+    \WTE{\Gamma::(x:T)}{U}{\Type(i)}}
+    {\WTEG{\forall~x:T,U}{\Type(i)}}}
 \item[Lam]\index{Typing rules!Lam} 
 \inference{\frac{\WTEG{\forall~x:T,U}{s}~~~~ \WTE{\Gamma::(x:T)}{t}{U}}
         {\WTEG{\lb x:T\mto t}{\forall x:T, U}}}
@@ -353,22 +332,34 @@ be derived from the following rules.
                  {\WTEG{(t\ u)}{\subst{T}{x}{u}}}}
 \item[Let]\index{Typing rules!Let} 
 \inference{\frac{\WTEG{t}{T}~~~~ \WTE{\Gamma::(x:=t:T)}{u}{U}}
-        {\WTEG{\kw{let}~x:=t~\kw{in}~u}{\subst{U}{x}{t}}}}
+        {\WTEG{\letin{x}{t:T}{u}}{\subst{U}{x}{t}}}}
 \end{description}
-    
-\Rem We may have $\kw{let}~x:=t~\kw{in}~u$
+
+\Rem Prod$_1$ and Prod$_2$ typing-rules make sense if we consider the semantic
+difference between {\Prop} and {\Set}:
+\begin{itemize}
+  \item All values of a type that has a sort {\Set} are extractable.
+  \item No values of a type that has a sort {\Prop} are extractable.
+\end{itemize}
+
+\Rem We may have $\kw{let}~x:=t:T~\kw{in}~u$
 well-typed without having $((\lb x:T\mto u)~t)$ well-typed (where
 $T$ is a type of $t$). This is because the value $t$ associated to $x$
 may be used in a conversion rule (see Section~\ref{conv-rules}).
 
 \section[Conversion rules]{Conversion rules\index{Conversion rules}
 \label{conv-rules}}
+
+In \CIC, there is an internal reduction mechanism. In particular, it
+can decide if two programs are {\em intentionally} equal (one
+says {\em convertible}). Convertibility is described in this section.
+
 \paragraph[$\beta$-reduction.]{$\beta$-reduction.\label{beta}\index{beta-reduction@$\beta$-reduction}}
 
 We want to be able to identify some terms as we can identify the
 application of a function to a given argument with its result. For
 instance the identity function over a given type $T$ can be written
-$\lb x:T\mto x$. In any environment $E$ and context $\Gamma$, we want to identify any object $a$ (of type $T$) with the
+$\lb x:T\mto x$. In any global environment $E$ and local context $\Gamma$, we want to identify any object $a$ (of type $T$) with the
 application $((\lb x:T\mto x)~a)$. We define for this a {\em reduction} (or a
 {\em conversion}) rule we call $\beta$:
 \[ \WTEGRED{((\lb x:T\mto
@@ -385,7 +376,7 @@ refer the interested reader to \cite{Coq85}.
 
 \paragraph[$\iota$-reduction.]{$\iota$-reduction.\label{iota}\index{iota-reduction@$\iota$-reduction}}
 A specific conversion rule is associated to the inductive objects in
-the environment.  We shall give later on (see Section~\ref{iotared}) the
+the global environment.  We shall give later on (see Section~\ref{iotared}) the
 precise rules but it just says that a destructor applied to an object
 built from a constructor behaves as expected.  This reduction is
 called $\iota$-reduction and is more precisely studied in
@@ -394,7 +385,7 @@ called $\iota$-reduction and is more precisely studied in
 
 \paragraph[$\delta$-reduction.]{$\delta$-reduction.\label{delta}\index{delta-reduction@$\delta$-reduction}}
 
-We may have defined variables in contexts or constants in the global
+We may have variables defined in local contexts or constants defined in the global
 environment. It is legal to identify such a reference with its value,
 that is to expand (or unfold) it into its value. This
 reduction is called $\delta$-reduction and shows as follows.
@@ -411,34 +402,57 @@ called $\zeta$-reduction and shows as follows.
 
 $$\WTEGRED{\kw{let}~x:=u~\kw{in}~t}{\triangleright_{\zeta}}{\subst{t}{x}{u}}$$
 
-\paragraph{$\eta$-conversion.
-\label{eta}
-\index{eta-conversion@$\eta$-conversion}
+\paragraph{$\eta$-expansion.%
+\label{eta}%
+\index{eta-expansion@$\eta$-expansion}%
 %\index{eta-reduction@$\eta$-reduction}
-}
-An other important concept is $\eta$-conversion. It is to identify any
+}%
+Another important concept is $\eta$-expansion. It is legal to identify any
 term $t$ of functional type $\forall x:T, U$ with its so-called
 $\eta$-expansion $\lb x:T\mto (t\ x)$ for $x$ an arbitrary variable
 name fresh in $t$.
 
-The notion of $\eta$-reduction ${\lb x:T\mto (t\ x)}{\triangleright}{t}$
-(for $x$ not occurring in $t$) is not type-sound because of subtyping
-(think about $\lb x:\Type(1)\mto (f x)$ of type $\forall
-x:\Type(1), \Type(1)$ for $f$ of type $\forall x:\Type(2),
-\Type(1)$). On the other side, $\eta$-expansion requires to know $T$
-and hence requires types. Hence, neither $\eta$-expansion nor
-$\eta$-reduction can be type-safely considered on terms we do not know
-the type. However, $\eta$ can be used as a conversion rule.
+\Rem We deliberately do not define $\eta$-reduction:
+\begin{latexonly}%
+  $$\lb x:T\mto (t\ x)\not\triangleright_\eta\hskip.3em t$$
+\end{latexonly}%
+\begin{htmlonly}
+  $$\lb x:T\mto (t\ x)~\not\triangleright_\eta~t$$
+\end{htmlonly}
+This is because, in general, the type of $t$ need not to be convertible to the type of $\lb x:T\mto (t\ x)$.
+E.g., if we take $f$ such that:
+\begin{latexonly}%
+  $$f\hskip.5em:\hskip.5em\forall x:Type(2),Type(1)$$
+\end{latexonly}%
+\begin{htmlonly}
+  $$f~:~\forall x:Type(2),Type(1)$$
+\end{htmlonly}
+then
+\begin{latexonly}%
+  $$\lb x:Type(1),(f\, x)\hskip.5em:\hskip.5em\forall x:Type(1),Type(1)$$
+\end{latexonly}%
+\begin{htmlonly}
+  $$\lb x:Type(1),(f\, x)~:~\forall x:Type(1),Type(1)$$
+\end{htmlonly}
+We could not allow
+\begin{latexonly}%
+  $$\lb x:Type(1),(f\,x)\hskip.4em\not\triangleright_\eta\hskip.6em f$$
+\end{latexonly}%
+\begin{htmlonly}
+  $$\lb x:Type(1),(f\,x)~\not\triangleright_\eta~f$$
+\end{htmlonly}
+because the type of the reduced term $\forall x:Type(2),Type(1)$
+would not be convertible to the type of the original term $\forall x:Type(1),Type(1)$.
 
 \paragraph[Convertibility.]{Convertibility.\label{convertibility}
 \index{beta-reduction@$\beta$-reduction}\index{iota-reduction@$\iota$-reduction}\index{delta-reduction@$\delta$-reduction}\index{zeta-reduction@$\zeta$-reduction}}
 
-Let us write $\WTEGRED{t}{\triangleright}{u}$ for the contextual closure of the relation $t$ reduces to $u$ in the environment $E$ and context $\Gamma$ with one of the previous reduction $\beta$, $\iota$, $\delta$ or $\zeta$.
+Let us write $\WTEGRED{t}{\triangleright}{u}$ for the contextual closure of the relation $t$ reduces to $u$ in the global environment $E$ and local context $\Gamma$ with one of the previous reduction $\beta$, $\iota$, $\delta$ or $\zeta$.
 
 We say that two terms $t_1$ and $t_2$ are {\em
   $\beta\iota\delta\zeta\eta$-convertible}, or simply {\em
-  convertible}, or {\em equivalent}, in the environment $E$ and
-context $\Gamma$ iff there exist terms $u_1$ and $u_2$ such that
+  convertible}, or {\em equivalent}, in the global environment $E$ and
+local context $\Gamma$ iff there exist terms $u_1$ and $u_2$ such that
 $\WTEGRED{t_1}{\triangleright \ldots \triangleright}{u_1}$ and
 $\WTEGRED{t_2}{\triangleright \ldots \triangleright}{u_2}$ and either
 $u_1$ and $u_2$ are identical, or they are convertible up to
@@ -451,11 +465,13 @@ The convertibility relation allows introducing a new typing rule
 which says that two convertible well-formed types have the same
 inhabitants.
 
+\section[Subtyping rules]{Subtyping rules\index{Subtyping rules}
+\label{subtyping-rules}}
+
 At the moment, we did not take into account one rule between universes
 which says that any term in a universe of index $i$ is also a term in
 the universe of index $i+1$ (this is the {\em cumulativity} rule of
-{\CIC}). This property is included into the
-conversion rule by extending the equivalence relation of
+{\CIC}). This property extends the equivalence relation of
 convertibility into a {\em subtyping} relation inductively defined by:
 \begin{enumerate}
 \item if $\WTEGCONV{t}{u}$ then $\WTEGLECONV{t}{u}$,
@@ -466,7 +482,7 @@ convertibility into a {\em subtyping} relation inductively defined by:
 \item if $\WTEGCONV{T}{U}$ and $\WTELECONV{\Gamma::(x:T)}{T'}{U'}$ then $\WTEGLECONV{\forall~x:T, T'}{\forall~x:U, U'}$.
 \end{enumerate}
 
-The conversion rule is now exactly:
+The conversion rule up to subtyping is now exactly:
 
 \begin{description}\label{Conv}
 \item[Conv]\index{Typing rules!Conv}
@@ -478,7 +494,7 @@ The conversion rule is now exactly:
 \paragraph[Normal form.]{Normal form.\index{Normal form}\label{Normal-form}\label{Head-normal-form}\index{Head normal form}}
 A term which cannot be any more reduced is said to be in {\em normal
   form}. There are several ways (or strategies) to apply the reduction
-rule. Among them, we have to mention the {\em head reduction} which
+rules. Among them, we have to mention the {\em head reduction} which
 will play an important role (see Chapter~\ref{Tactics}). Any term can
 be written as $\lb x_1:T_1\mto \ldots \lb x_k:T_k \mto
 (t_0\ t_1\ldots t_n)$ where
@@ -497,293 +513,122 @@ term is no more an abstraction leads to the {\em $\beta$-head normal
 where $v$ is not an abstraction (nor an application).  Note that the
 head normal form must not be confused with the normal form since some
 $u_i$ can be reducible.
-
+%
 Similar notions of head-normal forms involving $\delta$, $\iota$ and $\zeta$
 reductions or any combination of those can also be defined.
 
-\section{Derived rules for environments}
-
-From the original rules of the type system, one can derive new rules
-which change the context of definition of objects in the environment.
-Because these rules correspond to elementary operations in the \Coq\ 
-engine used in the discharge mechanism at the end of a section, we
-state them explicitly.
-
-\paragraph{Mechanism of substitution.}
+\section[Inductive definitions]{Inductive Definitions\label{Cic-inductive-definitions}}
 
-One rule which can be proved valid, is to replace a term $c$ by its
-value in the environment. As we defined the substitution of a term for
-a variable in a term, one can define the substitution of a term for a
-constant. One easily extends this substitution to contexts and
-environments.
-
-\paragraph{Substitution Property:} 
-\inference{\frac{\WF{E;\Def{\Gamma}{c}{t}{T}; F}{\Delta}}
-           {\WF{E; \subst{F}{c}{t}}{\subst{\Delta}{c}{t}}}}
+% Here we assume that the reader knows what is an inductive definition.
 
+Formally, we can represent any {\em inductive definition\index{definition!inductive}} as \Ind{}{p}{\Gamma_I}{\Gamma_C} where:
+\begin{itemize}
+  \item $\Gamma_I$ determines the names and types of inductive types;
+  \item $\Gamma_C$ determines the names and types of constructors of these inductive types;
+  \item $p$ determines the number of parameters of these inductive types.
+\end{itemize}
+These inductive definitions, together with global assumptions and global definitions, then form the global environment.
+%
+Additionally, for any $p$ there always exists $\Gamma_P=[a_1:A_1;\dots;a_p:A_p]$
+such that each $(t:T)\in\Gamma_I\cup\Gamma_C$ can be written as:
+$\forall\Gamma_P, T^\prime$ where $\Gamma_P$ is called the {\em context of parameters\index{context of parameters}}.
 
-\paragraph{Abstraction.}
+\paragraph{Examples}
 
-One can modify the context of definition of a constant $c$ by
-abstracting a constant with respect to the last variable $x$ of its
-defining context. For doing that, we need to check that the constants
-appearing in the body of the declaration do not depend on $x$, we need
-also to modify the reference to the constant $c$ in the environment
-and context by explicitly applying this constant to the variable $x$.
-Because of the rules for building environments and terms we know the
-variable $x$ is available at each stage where $c$ is mentioned.
-
-\paragraph{Abstracting property:} 
- \inference{\frac{\WF{E; \Def{\Gamma::(x:U)}{c}{t}{T};
-       F}{\Delta}~~~~\WFE{\Gamma}}
-           {\WF{E;\Def{\Gamma}{c}{\lb x:U\mto t}{\forall~x:U,T};
-  \subst{F}{c}{(c~x)}}{\subst{\Delta}{c}{(c~x)}}}}
-
-\paragraph{Pruning the context.} 
-We said the judgment \WFE{\Gamma} means that the defining contexts of
-constants in $E$ are included in $\Gamma$. If one abstracts or
-substitutes the constants with the above rules then it may happen
-that the context $\Gamma$ is now bigger than the one needed for
-defining the constants in $E$. Because defining contexts are growing
-in $E$, the minimum context needed for defining the constants in $E$
-is the same as the one for the last constant. One can consequently
-derive the following property.
-
-\paragraph{Pruning property:}
-\inference{\frac{\WF{E; \Def{\Delta}{c}{t}{T}}{\Gamma}}
-                {\WF{E;\Def{\Delta}{c}{t}{T}}{\Delta}}}
-
-
-\section[Inductive Definitions]{Inductive Definitions\label{Cic-inductive-definitions}}
-
-A (possibly mutual) inductive definition is specified by giving the
-names and the type of the inductive sets or families to be
-defined and the names and types of the constructors of the inductive
-predicates.  An inductive declaration in the environment can
-consequently be represented with two contexts (one for inductive
-definitions, one for constructors).
-
-Stating the rules for inductive definitions in their general form
-needs quite tedious definitions. We shall try to give a concrete
-understanding of the rules by precising them on running examples.  We
-take as examples the type of natural numbers, the type of
-parameterized lists over a type $A$, the relation which states that
-a list has some given length and the mutual inductive definition of trees and
-forests. 
-
-\subsection{Representing an inductive definition}
-\subsubsection{Inductive definitions without parameters}
-As for constants, inductive definitions can be defined in a non-empty
-context. \\
-We write \NInd{\Gamma}{\Gamma_I}{\Gamma_C} an inductive
-definition valid in a context $\Gamma$, a
-context of definitions $\Gamma_I$ and a context of constructors
-$\Gamma_C$.
-\paragraph{Examples.}
-The inductive declaration for the type of natural numbers will be:
-\[\NInd{}{\nat:\Set}{\nO:\nat,\nS:\nat\ra\nat}\]
-In a context with a variable $A:\Set$, the lists of elements in $A$ are
-represented by:
-\[\NInd{A:\Set}{\List:\Set}{\Nil:\List,\cons : A \ra \List \ra
-  \List}\]
- Assuming 
-  $\Gamma_I$ is $[I_1:A_1;\ldots;I_k:A_k]$, and $\Gamma_C$ is
-  $[c_1:C_1;\ldots;c_n:C_n]$, the general typing rules are, 
-  for $1\leq j\leq k$ and $1\leq i\leq n$:
-
-\bigskip
-\inference{\frac{\NInd{\Gamma}{\Gamma_I}{\Gamma_C} \in E}{(I_j:A_j) \in E}}
-
-\inference{\frac{\NInd{\Gamma}{\Gamma_I}{\Gamma_C} \in E}{(c_i:C_i) \in E}}
-
-\subsubsection{Inductive definitions with parameters}
-
-We have to slightly complicate the representation above in order to handle
-the delicate problem of parameters. 
-Let us explain that on the example of \List. With the above definition,
-the type \List\ can only be used in an environment where we
-have a variable $A:\Set$. Generally one want to consider lists of
-elements in different types. For constants this is easily done by abstracting
-the value over the parameter. In the case of inductive definitions we
-have to handle the abstraction over several objects.
-
-One possible way to do that would be to define the type \List\
-inductively as being an inductive family of type $\Set\ra\Set$:
-\[\NInd{}{\List:\Set\ra\Set}{\Nil:(\forall A:\Set,\List~A),
-  \cons : (\forall A:\Set, A \ra \List~A \ra \List~A)}\]
-There are drawbacks to this point of view. The
-information which says that for any $A$, $(\List~A)$ is an inductively defined
-\Set\ has been lost.
-So we introduce two important definitions.
-
-\paragraph{Inductive parameters, real arguments.}
-An inductive definition $\NInd{\Gamma}{\Gamma_I}{\Gamma_C}$ admits 
-$r$ inductive parameters if each type of constructors $(c:C)$ in
-$\Gamma_C$ is such that 
-\[C\equiv \forall
-p_1:P_1,\ldots,\forall p_r:P_r,\forall a_1:A_1, \ldots \forall a_n:A_n,
-(I~p_1~\ldots p_r~t_1\ldots t_q)\]
-with $I$ one of the inductive definitions in $\Gamma_I$. 
-We say that $q$ is the number of real arguments of the constructor
-$c$. 
-\paragraph{Context of parameters.}
-If an inductive definition $\NInd{\Gamma}{\Gamma_I}{\Gamma_C}$ admits 
-$r$ inductive parameters, then there exists a context $\Gamma_P$ of
-size $r$, such that $\Gamma_P=[p_1:P_1;\ldots;p_r:P_r]$ and 
-if $(t:A) \in \Gamma_I,\Gamma_C$ then $A$ can be written as 
-$\forall p_1:P_1,\ldots \forall p_r:P_r,A'$. 
-We call $\Gamma_P$ the context of parameters of the inductive
-definition and use the notation $\forall \Gamma_P,A'$ for the term $A$.
-\paragraph{Remark.}
-If we have a term $t$ in an instance of an
-inductive definition $I$ which starts with a constructor $c$, then the
-$r$ first arguments of $c$ (the parameters) can be deduced from the
-type $T$ of $t$: these are exactly the $r$ first arguments of $I$ in
-the head normal form of $T$.
-\paragraph{Examples.}
-The \List{} definition has $1$ parameter:
-\[\NInd{}{\List:\Set\ra\Set}{\Nil:(\forall A:\Set, \List~A),
-  \cons : (\forall A:\Set, A \ra \List~A \ra \List~A)}\]
-This is also the case for this more complex definition where there is
-a recursive argument on a different instance of \List: 
-\[\NInd{}{\List:\Set\ra\Set}{\Nil:(\forall A:\Set, \List~A),
-  \cons : (\forall A:\Set, A \ra \List~(A \ra A) \ra \List~A)}\]
-But the following definition has $0$ parameters:
-\[\NInd{}{\List:\Set\ra\Set}{\Nil:(\forall A:\Set, \List~A),
-  \cons : (\forall A:\Set, A \ra \List~A \ra \List~(A*A))}\]
-
-%\footnote{
-%The interested reader may compare the above definition with the two 
-%following ones which have very different logical meaning:\\
-%$\NInd{}{\List:\Set}{\Nil:\List,\cons : (A:\Set)A
-%  \ra \List \ra \List}$ \\
-%$\NInd{}{\List:\Set\ra\Set}{\Nil:(A:\Set)(\List~A),\cons : (A:\Set)A
-%  \ra (\List~A\ra A) \ra (\List~A)}$.}
-\paragraph{Concrete syntax.}
-In the Coq system, the context of parameters is given explicitly
-after the name of the inductive definitions and is shared between the
-arities and the type of constructors.
-% The vernacular declaration of polymorphic trees and forests will be:\\
-% \begin{coq_example*}
-% Inductive Tree (A:Set) : Set := 
-%    Node : A -> Forest A -> Tree A
-% with Forest (A : Set) : Set := 
-%    Empty : Forest A
-%  | Cons  : Tree A -> Forest A -> Forest A
-% \end{coq_example*}
-% will correspond in our formalism to:
-% \[\NInd{}{{\tt Tree}:\Set\ra\Set;{\tt Forest}:\Set\ra \Set}
-%   {{\tt Node} : \forall A:\Set, A \ra {\tt Forest}~A \ra {\tt Tree}~A,
-%    {\tt Empty} : \forall A:\Set, {\tt Forest}~A,
-%    {\tt Cons} : \forall A:\Set, {\tt Tree}~A \ra {\tt Forest}~A \ra
-%    {\tt Forest}~A}\]
-We keep track in the syntax of the number of
-parameters. 
-
-Formally the representation of an inductive declaration
-will be 
-\Ind{\Gamma}{p}{\Gamma_I}{\Gamma_C} for an inductive
-definition valid in a context $\Gamma$ with $p$ parameters, a
-context of definitions $\Gamma_I$ and a context of constructors
-$\Gamma_C$.
-
-The definition \Ind{\Gamma}{p}{\Gamma_I}{\Gamma_C} will be
-well-formed exactly when \NInd{\Gamma}{\Gamma_I}{\Gamma_C} is and 
-when $p$ is (less or equal than) the number of parameters in
-\NInd{\Gamma}{\Gamma_I}{\Gamma_C}. 
+    \newcommand\ind[3]{$\mathsf{Ind}~[#1]\left(\hskip-.4em
+    \begin{array}{r @{\mathrm{~:=~}} l}
+      #2 & #3 \\
+    \end{array}
+    \hskip-.4em
+    \right)$}
+    \def\colon{@{\hskip.5em:\hskip.5em}}
 
-\paragraph{Examples}
 The declaration for parameterized lists is:
-\[\Ind{}{1}{\List:\Set\ra\Set}{\Nil:(\forall A:\Set,\List~A),\cons :
-  (\forall A:\Set, A \ra \List~A \ra   \List~A)}\]
+    \vskip.5em
 
-The declaration for the length of lists is:
-\[\Ind{}{1}{\Length:\forall A:\Set, (\List~A)\ra \nat\ra\Prop}
-      {\LNil:\forall A:\Set, \Length~A~(\Nil~A)~\nO,\\ 
-     \LCons :\forall A:\Set,\forall a:A, \forall l:(\List~A),\forall n:\nat, (\Length~A~l~n)\ra (\Length~A~(\cons~A~a~l)~(\nS~n))}\]
+\ind{1}{\List:\Set\ra\Set}{\left[\begin{array}{r \colon l}
+                        \Nil & \forall A:\Set,\List~A \\
+                        \cons & \forall A:\Set, A \ra \List~A \ra \List~A
+                        \end{array}\right]}
+    \vskip.5em
 
-The declaration for a mutual inductive definition of forests and trees is:
-\[\NInd{}{\tree:\Set,\forest:\Set}
-      {\\~~\node:\forest \ra \tree,
-       \emptyf:\forest,\consf:\tree \ra \forest \ra \forest\-}\]
-  
-These representations are the ones obtained as the result of the \Coq\ 
-declaration:
+which corresponds to the result of the \Coq\ declaration:
 \begin{coq_example*}
-Inductive nat : Set :=
-  | O : nat
-  | S : nat -> nat.
 Inductive list (A:Set) : Set :=
   | nil : list A
   | cons : A -> list A -> list A.
 \end{coq_example*}
+
+The declaration for a mutual inductive definition of forests and trees is:
+    \vskip.5em
+\ind{}{\left[\begin{array}{r \colon l}\tree&\Set\\\forest&\Set\end{array}\right]}
+      {\left[\begin{array}{r \colon l}
+            \node & \forest \ra \tree\\
+            \emptyf & \forest\\
+            \consf & \tree \ra \forest \ra \forest\\
+                      \end{array}\right]}
+    \vskip.5em
+ 
+which corresponds to the result of the \Coq\ 
+declaration:
 \begin{coq_example*}
-Inductive Length (A:Set) : list A -> nat -> Prop :=
-  | Lnil : Length A (nil A) O
-  | Lcons :
-      forall (a:A) (l:list A) (n:nat),
-        Length A l n -> Length A (cons A a l) (S n).
 Inductive tree : Set :=
     node : forest -> tree
 with forest : Set :=
   | emptyf : forest
   | consf : tree -> forest -> forest.
 \end{coq_example*}
-% The inductive declaration in \Coq\ is slightly different from the one
-% we described theoretically. The difference is that in the type of
-% constructors the inductive definition is explicitly applied to the
-% parameters variables.
-The \Coq\ type-checker verifies that all
-parameters are applied in the correct manner in the conclusion of the
-type of each constructors:
-
-In particular, the following definition will not be accepted because 
-there is an occurrence of \List\ which is not applied to the parameter
-variable in the conclusion of the type of {\tt cons'}:
-\begin{coq_eval}
-Set Printing Depth 50.
-\end{coq_eval}
-% (********** The following is not correct and should produce **********)
-% (********* Error: The 1st argument of list' must be A in ... *********)
-\begin{coq_example}
-Fail Inductive list' (A:Set) : Set :=
-  | nil' : list' A
-  | cons' : A -> list' A -> list' (A*A).
-\end{coq_example}
-Since \Coq{} version 8.1, there is no restriction about parameters in
-the types of arguments of constructors. The following definition is
-valid:
-\begin{coq_example}
-Inductive list' (A:Set) : Set :=
-  | nil' : list' A
-  | cons' : A -> list' (A->A) -> list' A.
-\end{coq_example}
 
+The declaration for a mutual inductive definition of even and odd is:
+    \newcommand\GammaI{\left[\begin{array}{r \colon l}
+                        \even & \nat\ra\Prop \\
+                        \odd & \nat\ra\Prop
+                      \end{array}
+                \right]}
+    \newcommand\GammaC{\left[\begin{array}{r \colon l}
+                        \evenO & \even~\nO \\
+                        \evenS & \forall n : \nat, \odd~n \ra \even~(\nS~n)\\
+                        \oddS & \forall n : \nat, \even~n \ra \odd~(\nS~n)
+                      \end{array}
+                \right]}
+    \vskip.5em
+    \ind{1}{\GammaI}{\GammaC}
+    \vskip.5em
+which corresponds to the result of the \Coq\ 
+declaration:
+\begin{coq_example*}
+Inductive even : nat -> Prop :=
+  | even_O : even 0
+  | even_S : forall n, odd n -> even (S n)
+with odd : nat -> Prop :=
+  | odd_S : forall n, even n -> odd (S n).
+\end{coq_example*}
 
 \subsection{Types of inductive objects}
-We have to give the type of constants in an environment $E$ which
+We have to give the type of constants in a global environment $E$ which
 contains an inductive declaration.
 
 \begin{description}
-\item[Ind-Const] Assuming 
-  $\Gamma_I$ is $[I_1:A_1;\ldots;I_k:A_k]$, and $\Gamma_C$ is
-  $[c_1:C_1;\ldots;c_n:C_n]$,
-   
-\inference{\frac{\Ind{\Gamma}{p}{\Gamma_I}{\Gamma_C} \in E
-    ~~j=1\ldots k}{(I_j:A_j) \in E}}
-
-\inference{\frac{\Ind{\Gamma}{p}{\Gamma_I}{\Gamma_C} \in E
-    ~~~~i=1.. n}
-   {(c_i:C_i) \in E}}
+\item[Ind]  \index{Typing rules!Ind}
+  \inference{\frac{\WFE{\Gamma}\hskip2em\Ind{}{p}{\Gamma_I}{\Gamma_C} \in E\hskip2em(a:A)\in\Gamma_I}{\WTEG{a}{A}}}
+\item[Constr]  \index{Typing rules!Constr}
+  \inference{\frac{\WFE{\Gamma}\hskip2em\Ind{}{p}{\Gamma_I}{\Gamma_C} \in E\hskip2em(c:C)\in\Gamma_C}{\WTEG{c}{C}}}
 \end{description}
 
+\begin{latexonly}%
 \paragraph{Example.}
-We have $(\List:\Set \ra \Set), (\cons:\forall~A:\Set,A\ra(\List~A)\ra
-(\List~A))$, \\ 
-$(\Length:\forall~A:\Set, (\List~A)\ra\nat\ra\Prop)$, $\tree:\Set$ and $\forest:\Set$.
-
-From now on, we write $\ListA$ instead of $(\List~A)$ and $\LengthA$
-for $(\Length~A)$.
+Provided that our environment $E$ contains inductive definitions we showed before,
+these two inference rules above enable us to conclude that:
+\vskip.5em
+\newcommand\prefix{E[\Gamma]\vdash\hskip.25em}
+$\begin{array}{@{} l}
+   \prefix\even : \nat\ra\Prop\\
+   \prefix\odd : \nat\ra\Prop\\
+   \prefix\evenO : \even~\nO\\
+   \prefix\evenS : \forall~n:\nat, \odd~n \ra \even~(\nS~n)\\
+   \prefix\oddS : \forall~n:\nat, \even~n \ra \odd~(\nS~n)
+ \end{array}$
+\end{latexonly}%
 
 %\paragraph{Parameters.}
 %%The parameters introduce a distortion between the inside specification
@@ -793,30 +638,48 @@ for $(\Length~A)$.
 %%typing rules where the inductive objects are seen as objects
 %%abstracted with respect to the parameters.
 
-%In the definition of \List\ or \Length\, $A$ is a parameter because
-%what is effectively inductively defined is $\ListA$ or $\LengthA$ for
+%In the definition of \List\ or \haslength\, $A$ is a parameter because
+%what is effectively inductively defined is $\ListA$ or $\haslengthA$ for
 %a given $A$ which is constant in the type of constructors.  But when
-%we define $(\LengthA~l~n)$, $l$ and $n$ are not parameters because the
+%we define $(\haslengthA~l~n)$, $l$ and $n$ are not parameters because the
 %constructors manipulate different instances of this family.
 
 \subsection{Well-formed inductive definitions}
 We cannot accept any inductive declaration because some of them lead
-to inconsistent systems. We restrict ourselves to definitions which
+to inconsistent systems.
+We restrict ourselves to definitions which
 satisfy a syntactic criterion of positivity. Before giving the formal
 rules, we need a few definitions:
 
-\paragraph[Definitions]{Definitions\index{Positivity}\label{Positivity}}
-
-A type $T$ is an {\em arity of sort $s$}\index{Arity} if it converts
+\paragraph[Definition]{Definition\index{Arity}\label{Arity}}
+A type $T$ is an {\em arity of sort $s$} if it converts
 to the sort $s$ or to a product $\forall~x:T,U$ with $U$ an arity
-of sort $s$. (For instance $A\ra \Set$ or $\forall~A:\Prop,A\ra
-\Prop$ are arities of sort respectively \Set\ and \Prop).  A {\em type
-  of constructor of $I$}\index{Type of constructor} is either a term
-$(I~t_1\ldots ~t_n)$ or $\fa x:T,C$ with $C$ recursively 
-a {\em type of constructor of $I$}.
+of sort $s$.
+
+\paragraph[Examples]{Examples}
+$A\ra \Set$ is an arity of sort $\Set$.
+$\forall~A:\Prop,A\ra \Prop$ is an arity of sort \Prop.
 
-\smallskip
+\paragraph[Definition]{Definition}
+A type $T$ is an {\em arity} if there is a $s\in\Sort$
+such that $T$ is an arity of sort $s$.
 
+\paragraph[Examples]{Examples}
+$A\ra \Set$ and $\forall~A:\Prop,A\ra \Prop$ are arities.
+
+\paragraph[Definition]{Definition\index{type of constructor}}
+We say that $T$ is a {\em type of constructor of $I$\index{type of constructor}}
+in one of the following two cases:
+\begin{itemize}
+  \item $T$ is $(I~t_1\ldots ~t_n)$
+  \item $T$ is $\forall x:U,T^\prime$ where $T^\prime$ is also a type of constructor of $I$
+\end{itemize}
+
+\paragraph[Examples]{Examples}
+$\nat$ and $\nat\ra\nat$ are types of constructors of $\nat$.\\
+$\forall A:\Type,\List~A$ and $\forall A:\Type,A\ra\List~A\ra\List~A$ are constructors of $\List$.
+
+\paragraph[Definition]{Definition\index{Positivity}\label{Positivity}}
 The type of constructor $T$ will be said to {\em satisfy the positivity
 condition} for a constant $X$ in the following cases:
 
@@ -826,10 +689,10 @@ any $t_i$
 \item $T=\forall~x:U,V$ and $X$ occurs only strictly positively in $U$ and
 the type $V$ satisfies the positivity condition for $X$
 \end{itemize}
-
+%
 The constant $X$ {\em occurs strictly positively} in $T$ in the
 following cases:
-
+%
 \begin{itemize}
 \item $X$ does not occur in $T$
 \item $T$ converts to $(X~t_1 \ldots ~t_n)$ and $X$ does not occur in
@@ -850,7 +713,7 @@ following cases:
 %positively in $T[x:U]u$ if $X$ does not occur in $U$ but occurs
 %strictly positively in $u$
 \end{itemize}
-
+%
 The type of constructor $T$ of $I$ {\em satisfies the nested
 positivity condition} for a constant $X$ in the following
 cases:
@@ -863,40 +726,73 @@ any $u_i$
 the type $V$ satisfies the nested positivity condition for $X$
 \end{itemize}
 
-\paragraph{Example}
-
-$X$ occurs strictly positively in $A\ra X$ or $X*A$ or $({\tt list}~
-X)$ but not in $X \ra A$ or $(X \ra A)\ra A$ nor $({\tt neg}~X)$
-assuming the notion of product and lists were already defined and {\tt
-  neg} is an inductive definition with declaration \Ind{}{A:\Set}{{\tt
-    neg}:\Set}{{\tt neg}:(A\ra{\tt False}) \ra {\tt neg}}.  Assuming
-$X$ has arity ${\tt nat \ra Prop}$ and {\tt ex} is the inductively
-defined existential quantifier, the occurrence of $X$ in ${\tt (ex~
-  nat~ \lb n:nat\mto (X~ n))}$ is also strictly positive.
+%% \begin{latexonly}%
+   \newcommand\vv{\textSFxi}    % │
+   \newcommand\hh{\textSFx}     %   ─
+   \newcommand\vh{\textSFviii}  % ├
+   \newcommand\hv{\textSFii}    %   └
+   \newlength\framecharacterwidth
+   \settowidth\framecharacterwidth{\hh}
+   \newcommand\ws{\hbox{}\hskip\the\framecharacterwidth}
+   \newcommand\ruleref[1]{\hskip.25em\dots\hskip.2em{\em (bullet #1)}}
+%%   \def\captionstrut{\vbox to 1.5em{}}
+
+%%   \begin{figure}[H]
+For instance, if one considers the type
+
+\begin{verbatim}
+Inductive tree (A:Type) : Type :=
+ | leaf : list A
+ | node : A -> (nat -> tree A) -> tree A
+\end{verbatim}
+
+Then every instantiated constructor of $\ListA$ satisfies the nested positivity condition for $\List$
+
+\noindent
+    \ws\ws\ws\ws\vv\\
+    \ws\ws\ws\ws\vh\hh\ws concerning type $\ListA$ of constructor $\Nil$:\\
+    \ws\ws\ws\ws\vv\ws\ws\ws\ws Type $\ListA$ of constructor $\Nil$ satisfies the positivity condition for $\List$\\
+    \ws\ws\ws\ws\vv\ws\ws\ws\ws because $\List$ does not appear in any (real) arguments of the type of that constructor\\
+    \ws\ws\ws\ws\vv\ws\ws\ws\ws (primarily because $\List$ does not have any (real) arguments)\ruleref1\\
+    \ws\ws\ws\ws\vv\\
+    \ws\ws\ws\ws\hv\hh\ws concerning type $\forall~A\ra\ListA\ra\ListA$ of constructor $\cons$:\\
+    \ws\ws\ws\ws\ws\ws\ws\ws\ws Type $\forall~A:\Type,A\ra\ListA\ra\ListA$ of constructor $\cons$\\
+    \ws\ws\ws\ws\ws\ws\ws\ws\ws satisfies the positivity condition for $\List$ because:\\
+    \ws\ws\ws\ws\ws\ws\ws\ws\ws\vv\\
+    \ws\ws\ws\ws\ws\ws\ws\ws\ws\vh\hh\ws $\List$ occurs only strictly positively in $\Type$\ruleref3\\
+    \ws\ws\ws\ws\ws\ws\ws\ws\ws\vv\\
+    \ws\ws\ws\ws\ws\ws\ws\ws\ws\vh\hh\ws $\List$ occurs only strictly positively in $A$\ruleref3\\
+    \ws\ws\ws\ws\ws\ws\ws\ws\ws\vv\\
+    \ws\ws\ws\ws\ws\ws\ws\ws\ws\vh\hh\ws $\List$ occurs only strictly positively in $\ListA$\ruleref4\\
+    \ws\ws\ws\ws\ws\ws\ws\ws\ws\vv\\
+    \ws\ws\ws\ws\ws\ws\ws\ws\ws\hv\hh\ws $\List$ satisfies the positivity condition for $\ListA$\ruleref1
+%%     \caption{\captionstrut A proof that $X$ occurs strictly positively in $\ListA$}
+%%   \end{figure}
+%% \end{latexonly}%
 
 \paragraph{Correctness rules.}
 We shall now describe the rules allowing the introduction of a new
 inductive definition.
 
 \begin{description}
-\item[W-Ind] Let $E$ be an environment and
-  $\Gamma,\Gamma_P,\Gamma_I,\Gamma_C$ are contexts such that
+\item[W-Ind] Let $E$ be a global environment and
+  $\Gamma_P,\Gamma_I,\Gamma_C$ are contexts such that
   $\Gamma_I$ is $[I_1:\forall \Gamma_P,A_1;\ldots;I_k:\forall
   \Gamma_P,A_k]$ and $\Gamma_C$ is 
   $[c_1:\forall \Gamma_P,C_1;\ldots;c_n:\forall \Gamma_P,C_n]$. 
 \inference{
   \frac{
-  (\WTE{\Gamma;\Gamma_P}{A_j}{s'_j})_{j=1\ldots  k}
-  ~~ (\WTE{\Gamma;\Gamma_I;\Gamma_P}{C_i}{s_{q_i}})_{i=1\ldots  n}
+  (\WTE{\Gamma_P}{A_j}{s'_j})_{j=1\ldots  k}
+  ~~ (\WTE{\Gamma_I;\Gamma_P}{C_i}{s_{q_i}})_{i=1\ldots  n}
 }
-  {\WF{E;\Ind{\Gamma}{p}{\Gamma_I}{\Gamma_C}}{\Gamma}}}
+  {\WF{E;\Ind{}{p}{\Gamma_I}{\Gamma_C}}{\Gamma}}}
 provided that the following side conditions hold:
 \begin{itemize}
 \item $k>0$ and all of $I_j$ and $c_i$ are distinct names for $j=1\ldots  k$ and $i=1\ldots  n$,
-\item $p$ is the number of parameters of \NInd{\Gamma}{\Gamma_I}{\Gamma_C}
+\item $p$ is the number of parameters of \NInd{}{\Gamma_I}{\Gamma_C}
   and $\Gamma_P$ is the context of parameters, 
 \item for $j=1\ldots  k$ we have that $A_j$ is an arity of sort $s_j$ and $I_j
-  \notin \Gamma \cup E$,
+  \notin E$,
 \item for $i=1\ldots  n$ we have that $C_i$ is a type of constructor of
   $I_{q_i}$ which satisfies the positivity condition for $I_1 \ldots  I_k$
   and $c_i \notin \Gamma \cup E$.
@@ -905,7 +801,7 @@ provided that the following side conditions hold:
 One can remark that there is a constraint between the sort of the
 arity of the inductive type and the sort of the type of its
 constructors which will always be satisfied for the impredicative sort
-(\Prop) but may fail to define inductive definition 
+{\Prop} but may fail to define inductive definition 
 on sort \Set{} and generate constraints between universes for
 inductive definitions in the {\Type} hierarchy.
 
@@ -938,19 +834,19 @@ Inductive exType (P:Type->Prop) : Type
 %is recursive or not.  We shall write the type $(x:_R T)C$ if it is 
 %a recursive argument and $(x:_P T)C$ if the argument is not recursive.
 
-\paragraph[Sort-polymorphism of inductive families.]{Sort-polymorphism of inductive families.\index{Sort-polymorphism of inductive families}}
+\paragraph[Sort-polymorphism of inductive types.]{Sort-polymorphism of inductive types.\index{Sort-polymorphism of inductive types}}
+\label{Sort-polymorphism-inductive}
 
-From {\Coq} version 8.1, inductive families declared in {\Type} are
+Inductive types declared in {\Type} are
 polymorphic over their arguments in {\Type}.
-
-If $A$ is an arity and $s$ a sort, we write $A_{/s}$ for the arity
+If $A$ is an arity of some sort and $s$ is a sort, we write $A_{/s}$ for the arity
 obtained from $A$ by replacing its sort with $s$. Especially, if $A$
-is well-typed in some environment and context, then $A_{/s}$ is typable
+is well-typed in some global environment and local context, then $A_{/s}$ is typable
 by typability of all products in the Calculus of Inductive Constructions.
 The following typing rule is added to the theory.
 
 \begin{description}
-\item[Ind-Family] Let $\Ind{\Gamma}{p}{\Gamma_I}{\Gamma_C}$ be an
+\item[Ind-Family] Let $\Ind{}{p}{\Gamma_I}{\Gamma_C}$ be an
   inductive definition. Let $\Gamma_P = [p_1:P_1;\ldots;p_{p}:P_{p}]$
   be its context of parameters, $\Gamma_I = [I_1:\forall
     \Gamma_P,A_1;\ldots;I_k:\forall \Gamma_P,A_k]$ its context of
@@ -970,13 +866,13 @@ The following typing rule is added to the theory.
 
 \inference{\frac
 {\left\{\begin{array}{l}
-\Ind{\Gamma}{p}{\Gamma_I}{\Gamma_C} \in E\\
-(E[\Gamma] \vdash q_l : P'_l)_{l=1\ldots r}\\
-(\WTEGLECONV{P'_l}{\subst{P_l}{p_u}{q_u}_{u=1\ldots l-1}})_{l=1\ldots r}\\
+\Ind{}{p}{\Gamma_I}{\Gamma_C} \in E\\
+(E[] \vdash q_l : P'_l)_{l=1\ldots r}\\
+(\WTELECONV{}{P'_l}{\subst{P_l}{p_u}{q_u}_{u=1\ldots l-1}})_{l=1\ldots r}\\
 1 \leq j \leq k
 \end{array}
 \right.}
-{E[\Gamma] \vdash (I_j\,q_1\,\ldots\,q_r:\forall [p_{r+1}:P_{r+1};\ldots;p_{p}:P_{p}], (A_j)_{/s_j})}
+{E[] \vdash I_j\,q_1\,\ldots\,q_r:\forall [p_{r+1}:P_{r+1};\ldots;p_{p}:P_{p}], (A_j)_{/s_j}}
 }
 
 provided that the following side conditions hold:
@@ -984,26 +880,26 @@ provided that the following side conditions hold:
 \begin{itemize}
 \item $\Gamma_{P'}$ is the context obtained from $\Gamma_P$ by
 replacing each $P_l$ that is an arity with $P'_l$ for $1\leq l \leq r$ (notice that
-$P_l$ arity implies $P'_l$ arity since $\WTEGLECONV{P'_l}{ \subst{P_l}{p_u}{q_u}_{u=1\ldots l-1}}$);
+$P_l$ arity implies $P'_l$ arity since $\WTELECONV{}{P'_l}{ \subst{P_l}{p_u}{q_u}_{u=1\ldots l-1}}$);
 \item there are sorts $s_i$, for $1 \leq i \leq k$ such that, for
  $\Gamma_{I'} = [I_1:\forall
     \Gamma_{P'},(A_1)_{/s_1};\ldots;I_k:\forall \Gamma_{P'},(A_k)_{/s_k}]$
-we have $(\WTE{\Gamma;\Gamma_{I'};\Gamma_{P'}}{C_i}{s_{q_i}})_{i=1\ldots  n}$;
-\item the sorts are such that all eliminations, to {\Prop}, {\Set} and
-  $\Type(j)$, are allowed (see section~\ref{elimdep}).
+we have $(\WTE{\Gamma_{I'};\Gamma_{P'}}{C_i}{s_{q_i}})_{i=1\ldots  n}$;
+\item the sorts $s_i$ are such that all eliminations, to {\Prop}, {\Set} and
+  $\Type(j)$, are allowed (see Section~\ref{allowedeleminationofsorts}).
 \end{itemize}
 \end{description}
-
+%
 Notice that if $I_j\,q_1\,\ldots\,q_r$ is typable using the rules {\bf
 Ind-Const} and {\bf App}, then it is typable using the rule {\bf
 Ind-Family}. Conversely, the extended theory is not stronger than the
 theory without {\bf Ind-Family}. We get an equiconsistency result by
-mapping each $\Ind{\Gamma}{p}{\Gamma_I}{\Gamma_C}$ occurring into a
+mapping each $\Ind{}{p}{\Gamma_I}{\Gamma_C}$ occurring into a
 given derivation into as many different inductive types and constructors
 as the number of different (partial) replacements of sorts, needed for
 this derivation, in the parameters that are arities (this is possible
-because $\Ind{\Gamma}{p}{\Gamma_I}{\Gamma_C}$ well-formed implies
-that $\Ind{\Gamma}{p}{\Gamma_{I'}}{\Gamma_{C'}}$ is well-formed and
+because $\Ind{}{p}{\Gamma_I}{\Gamma_C}$ well-formed implies
+that $\Ind{}{p}{\Gamma_{I'}}{\Gamma_{C'}}$ is well-formed and
 has the same allowed eliminations, where
 $\Gamma_{I'}$ is defined as above and $\Gamma_{C'} = [c_1:\forall
 \Gamma_{P'},C_1;\ldots;c_n:\forall \Gamma_{P'},C_n]$). That is,
@@ -1013,7 +909,7 @@ sorts among the types of parameters, and to each signature is
 associated a new inductive definition with fresh names. Conversion is
 preserved as any (partial) instance $I_j\,q_1\,\ldots\,q_r$ or
 $C_i\,q_1\,\ldots\,q_r$ is mapped to the names chosen in the specific
-instance of $\Ind{\Gamma}{p}{\Gamma_I}{\Gamma_C}$.
+instance of $\Ind{}{p}{\Gamma_I}{\Gamma_C}$.
 
 \newcommand{\Single}{\mbox{\textsf{Set}}}
 
@@ -1033,23 +929,21 @@ predicative {\Set}.
 More precisely, an empty or small singleton inductive definition
 (i.e. an inductive definition of which all inductive types are
 singleton -- see paragraph~\ref{singleton}) is set in
-{\Prop}, a small non-singleton inductive family is set in {\Set} (even
+{\Prop}, a small non-singleton inductive type is set in {\Set} (even
 in case {\Set} is impredicative -- see Section~\ref{impredicativity}),
 and otherwise in the {\Type} hierarchy.
-% TODO: clarify the case of a partial application ??
 
 Note that the side-condition about allowed elimination sorts in the
 rule~{\bf Ind-Family} is just to avoid to recompute the allowed
 elimination sorts at each instance of a pattern-matching (see
-section~\ref{elimdep}).
-
+section~\ref{elimdep}).  
 As an example, let us consider the following definition:
 \begin{coq_example*}
 Inductive option (A:Type) : Type := 
 | None : option A 
 | Some : A -> option A.
 \end{coq_example*}
-
+%
 As the definition is set in the {\Type} hierarchy, it is used
 polymorphically over its parameters whose types are arities of a sort
 in the {\Type} hierarchy. Here, the parameter $A$ has this property,
@@ -1057,20 +951,20 @@ hence, if \texttt{option} is applied to a type in {\Set}, the result is
 in {\Set}. Note that if \texttt{option} is applied to a type in {\Prop},
 then, the result is not set in \texttt{Prop} but in \texttt{Set}
 still. This is because \texttt{option} is not a singleton type (see
-section~\ref{singleton}) and it would loose the elimination to {\Set} and
+section~\ref{singleton}) and it would lose the elimination to {\Set} and
 {\Type} if set in {\Prop}.
 
 \begin{coq_example}
 Check (fun A:Set => option A).
 Check (fun A:Prop => option A).
 \end{coq_example}
-
+%
 Here is another example.
-
+%
 \begin{coq_example*}
 Inductive prod (A B:Type) : Type := pair : A -> B -> prod A B.
 \end{coq_example*}
-
+%
 As \texttt{prod} is a singleton type, it will be in {\Prop} if applied
 twice to propositions, in {\Set} if applied twice to at least one type
 in {\Set} and none in {\Type}, and in {\Type} otherwise. In all cases,
@@ -1103,7 +997,7 @@ a strongly normalizing reduction, we cannot accept any sort of
 recursion (even terminating). So the basic idea is to restrict
 ourselves to primitive recursive functions and functionals.
 
-For instance, assuming a parameter $A:\Set$ exists in the context, we
+For instance, assuming a parameter $A:\Set$ exists in the local context, we
 want to build a function \length\ of type $\ListA\ra \nat$ which
 computes the length of the list, so such that $(\length~(\Nil~A)) = \nO$
 and $(\length~(\cons~A~a~l)) = (\nS~(\length~l))$.  We want these
@@ -1121,24 +1015,25 @@ In case the inductive definition is effectively a recursive one, we
 want to capture the extra property that we have built the smallest
 fixed point of this recursive equation.  This says that we are only
 manipulating finite objects. This analysis provides induction
-principles.
-
-For instance, in order to prove $\forall l:\ListA,(\LengthA~l~(\length~l))$
+principles.  
+For instance, in order to prove $\forall l:\ListA,(\haslengthA~l~(\length~l))$
 it is enough to prove:
-
-\noindent $(\LengthA~(\Nil~A)~(\length~(\Nil~A)))$ and
-
-\smallskip
-$\forall a:A, \forall l:\ListA, (\LengthA~l~(\length~l)) \ra
-(\LengthA~(\cons~A~a~l)~(\length~(\cons~A~a~l)))$.
-\smallskip
-
-\noindent which given the conversion equalities satisfied by \length\ is the
+%
+\begin{itemize}
+  \item $(\haslengthA~(\Nil~A)~(\length~(\Nil~A)))$
+  \item $\forall a:A, \forall l:\ListA, (\haslengthA~l~(\length~l)) \ra\\
+        \ra (\haslengthA~(\cons~A~a~l)~(\length~(\cons~A~a~l)))$
+\end{itemize}
+%
+which given the conversion equalities satisfied by \length\ is the
 same as proving:
-$(\LengthA~(\Nil~A)~\nO)$ and $\forall a:A, \forall l:\ListA, 
-(\LengthA~l~(\length~l)) \ra
-(\LengthA~(\cons~A~a~l)~(\nS~(\length~l)))$.
-
+%
+\begin{itemize}
+  \item $(\haslengthA~(\Nil~A)~\nO)$
+  \item $\forall a:A, \forall l:\ListA, (\haslengthA~l~(\length~l)) \ra\\
+        \ra (\haslengthA~(\cons~A~a~l)~(\nS~(\length~l)))$
+\end{itemize}
+%
 One conceptually simple way to do that, following the basic scheme
 proposed by Martin-L\"of in his Intuitionistic Type Theory, is to
 introduce for each inductive definition an elimination operator. At
@@ -1147,7 +1042,7 @@ at the computational level it implements a generic operator for doing
 primitive recursion over the structure.
 
 But this operator is rather tedious to implement and use. We choose in
-this version of Coq to factorize the operator for primitive recursion
+this version of {\Coq} to factorize the operator for primitive recursion
 into two more primitive operations as was first suggested by Th. Coquand
 in~\cite{Coq92}.  One is the definition by pattern-matching. The second one is a definition by guarded fixpoints. 
 
@@ -1158,13 +1053,6 @@ The basic idea of this operator is that we have an object
 $m$ in an inductive type $I$ and we want to prove a property
 which possibly depends on $m$. For this, it is enough to prove the
 property for $m = (c_i~u_1\ldots  u_{p_i})$ for each constructor of $I$.
-
-
-The basic idea of this operator is that we have an object
-$m$ in an inductive type $I$ and we want to prove a property
-which possibly depends on $m$. For this, it is enough to prove the
-property for $m = (c_i~u_1\ldots  u_{p_i})$ for each constructor of $I$.
-
 The \Coq{} term for this proof will be written:
 \[\kw{match}~m~\kw{with}~ (c_1~x_{11}~...~x_{1p_1}) \Ra f_1 ~|~\ldots~|~
   (c_n~x_{n1}~...~x_{np_n}) \Ra f_n~ \kw{end}\]
@@ -1172,7 +1060,7 @@ In this expression, if
 $m$ eventually happens to evaluate to $(c_i~u_1\ldots u_{p_i})$ then
 the expression will behave as specified in its $i$-th branch and
 it will reduce to $f_i$ where the $x_{i1}$\ldots $x_{ip_i}$ are replaced
-by the $u_1\ldots u_p$ according to the $\iota$-reduction.
+by the $u_1\ldots u_{p_i}$ according to the $\iota$-reduction.
 
 Actually, for type-checking a \kw{match\ldots with\ldots end}
 expression we also need to know the predicate $P$ to be proved by case
@@ -1183,7 +1071,7 @@ one corresponds to object $m$. \Coq{} can sometimes infer this
 predicate but sometimes not. The concrete syntax for describing this
 predicate uses the \kw{as\ldots in\ldots return} construction. For
 instance, let us assume that $I$ is an unary predicate with one
-parameter. The predicate is made explicit using the syntax:
+parameter and one argument. The predicate is made explicit using the syntax:
 \[\kw{match}~m~\kw{as}~ x~ \kw{in}~ I~\verb!_!~a~ \kw{return}~ P
  ~\kw{with}~ (c_1~x_{11}~...~x_{1p_1}) \Ra f_1 ~|~\ldots~|~
   (c_n~x_{n1}~...~x_{np_n}) \Ra f_n \kw{end}\]
@@ -1194,13 +1082,16 @@ The \kw{in} part can be
 omitted if the result type does not depend on the arguments of
 $I$. Note that the arguments of $I$ corresponding to parameters
 \emph{must} be \verb!_!, because the result type is not generalized to
-all possible values of the parameters. The other arguments of $I$
-(sometimes called indices in the litterature) have to be variables
-($a$ above) and these variables can occur in $P$ and bound in it.
+all possible values of the parameters.
+The other arguments of $I$
+(sometimes called indices in the literature)
+% NOTE: e.g. http://www.qatar.cmu.edu/~sacchini/papers/types08.pdf
+have to be variables
+($a$ above) and these variables can occur in $P$.
 The expression after \kw{in}
 must be seen as an \emph{inductive type pattern}. Notice that
 expansion of implicit arguments and notations apply to this pattern.
-
+%
 For the purpose of presenting the inference rules, we use a more
 compact notation:
 \[ \Case{(\lb a x \mto P)}{m}{ \lb x_{11}~...~x_{1p_1} \mto f_1 ~|~\ldots~|~
@@ -1234,19 +1125,15 @@ compact notation:
 %  \mbox{\tt =>}~ \false}
 
 \paragraph[Allowed elimination sorts.]{Allowed elimination sorts.\index{Elimination sorts}}
+\label{allowedeleminationofsorts}
 
 An important question for building the typing rule for \kw{match} is
-what can be the type of $P$ with respect to the type of the inductive
-definitions.
-
-We define now a relation \compat{I:A}{B} between an inductive
-definition $I$ of type $A$ and an arity $B$. This relation states that
-an object in the inductive definition $I$ can be eliminated for
-proving a property $P$ of type $B$.
-
-The case of inductive definitions in sorts \Set\ or \Type{} is simple.
-There is no restriction on the sort of the predicate to be
-eliminated. 
+what can be the type of $\lb a x \mto P$ with respect to the type of $m$. If
+$m:I$ and
+$I:A$ and
+$\lb a x \mto P : B$
+then by \compat{I:A}{B} we mean that one can use $\lb a x \mto P$ with $m$ in the above
+match-construct.
 
 \paragraph{Notations.}
 The \compat{I:A}{B} is defined as the smallest relation satisfying the
@@ -1254,14 +1141,17 @@ following rules:
 We write \compat{I}{B} for \compat{I:A}{B} where $A$ is the type of
 $I$.
 
+The case of inductive definitions in sorts \Set\ or \Type{} is simple.
+There is no restriction on the sort of the predicate to be
+eliminated. 
+%
 \begin{description}
 \item[Prod] \inference{\frac{\compat{(I~x):A'}{B'}}
                       {\compat{I:\forall x:A, A'}{\forall x:A, B'}}}
 \item[{\Set} \& \Type] \inference{\frac{
-    s_1 \in \{\Set,\Type(j)\}, 
-    s_2 \in \Sort}{\compat{I:s_1}{I\ra s_2}}}
+    s_1 \in \{\Set,\Type(j)\}~~~~~~~~s_2 \in \Sort}{\compat{I:s_1}{I\ra s_2}}}
 \end{description}
-
+%
 The case of Inductive definitions of sort \Prop{} is a bit more
 complicated, because of our interpretation of this sort. The only
 harmless allowed elimination, is the one when predicate $P$ is also of
@@ -1314,7 +1204,7 @@ a logical property of a computational object.
 In the same spirit, elimination on $P$ of type $I\ra
 \Type$ cannot be allowed because it trivially implies the elimination
 on $P$ of type $I\ra \Set$ by cumulativity. It also implies that there
-is two proofs of the same property which are provably different,
+are two proofs of the same property which are provably different,
 contradicting the proof-irrelevance property which is sometimes a
 useful axiom:
 \begin{coq_example}
@@ -1352,17 +1242,17 @@ eliminations are allowed.
        definition}~~~s \in \Sort}{\compat{I:\Prop}{I\ra s}}
 }
 \end{description}
-
+%
 % A {\em singleton definition} has always an informative content,
 % even if it is a proposition.
-
+%
 A {\em singleton
 definition} has only one constructor and all the arguments of this
 constructor have type \Prop. In that case, there is a canonical
 way to interpret the informative extraction on an object in that type,
 such that the elimination on any sort $s$ is legal.  Typical examples are
 the conjunction of non-informative propositions and the equality. 
-If there is an hypothesis $h:a=b$ in the context, it can be used for
+If there is an hypothesis $h:a=b$ in the local context, it can be used for
 rewriting not only in logical propositions but also in any type.
 % In that case, the term \verb!eq_rec! which was defined as an axiom, is
 % now a term of the calculus.
@@ -1375,34 +1265,56 @@ elimination on any sort is allowed.
 
 \paragraph{Type of branches.}
 Let $c$ be a term of type $C$, we assume $C$ is a type of constructor
-for an inductive definition $I$. Let $P$ be a term that represents the
+for an inductive type $I$. Let $P$ be a term that represents the
 property to be proved.
-We assume $r$ is the number of parameters.
+We assume $r$ is the number of parameters and $p$ is the number of arguments.
 
 We define a new type \CI{c:C}{P} which represents the type of the
 branch corresponding to the $c:C$ constructor.
 \[
 \begin{array}{ll}
-\CI{c:(I_i~p_1\ldots p_r\ t_1 \ldots t_p)}{P} &\equiv (P~t_1\ldots ~t_p~c) \\[2mm]
+\CI{c:(I~p_1\ldots p_r\ t_1 \ldots t_p)}{P} &\equiv (P~t_1\ldots ~t_p~c) \\[2mm]
 \CI{c:\forall~x:T,C}{P} &\equiv \forall~x:T,\CI{(c~x):C}{P} 
 \end{array}
 \]
 We write \CI{c}{P} for \CI{c:C}{P} with $C$ the type of $c$.
 
-\paragraph{Examples.}
-For $\ListA$ the type of $P$ will be $\ListA\ra s$ for $s \in \Sort$. \\ 
-$ \CI{(\cons~A)}{P} \equiv
-\forall a:A, \forall l:\ListA,(P~(\cons~A~a~l))$.
-
-For $\LengthA$, the type of $P$ will be
-$\forall l:\ListA,\forall n:\nat, (\LengthA~l~n)\ra \Prop$ and the expression
-\CI{(\LCons~A)}{P} is defined as:\\ 
-$\forall a:A, \forall l:\ListA, \forall n:\nat, \forall
-h:(\LengthA~l~n), (P~(\cons~A~a~l)~(\nS~n)~(\LCons~A~a~l~n~l))$.\\ 
-If $P$ does not depend on its third argument, we find the more natural
-expression:\\ 
-$\forall a:A, \forall l:\ListA, \forall n:\nat,
-(\LengthA~l~n)\ra(P~(\cons~A~a~l)~(\nS~n))$.
+\paragraph{Example.}
+The following term in concrete syntax:
+\begin{verbatim}
+match t as l return P' with
+| nil _ => t1
+| cons _ hd tl => t2
+end
+\end{verbatim}
+can be represented in abstract syntax as $$\Case{P}{t}{f_1\,|\,f_2}$$
+where
+\begin{eqnarray*}
+  P & = & \lambda~l~.~P^\prime\\
+  f_1 & = & t_1\\
+  f_2 & = & \lambda~(hd:\nat)~.~\lambda~(tl:\List~\nat)~.~t_2
+\end{eqnarray*}
+According to the definition:
+\begin{latexonly}\vskip.5em\noindent\end{latexonly}%
+\begin{htmlonly}
+
+\end{htmlonly}
+$ \CI{(\Nil~\nat)}{P} \equiv \CI{(\Nil~\nat) : (\List~\nat)}{P} \equiv (P~(\Nil~\nat))$
+\begin{latexonly}\vskip.5em\noindent\end{latexonly}%
+\begin{htmlonly}
+
+\end{htmlonly}
+$ \CI{(\cons~\nat)}{P}
+  \equiv\CI{(\cons~\nat) : (\nat\ra\List~\nat\ra\List~\nat)}{P} \equiv\\
+  \equiv\forall n:\nat, \CI{(\cons~\nat~n) : \List~\nat\ra\List~\nat)}{P} \equiv\\
+  \equiv\forall n:\nat, \forall l:\List~\nat, \CI{(\cons~\nat~n~l) : \List~\nat)}{P} \equiv\\
+\equiv\forall n:\nat, \forall l:\List~\nat,(P~(\cons~\nat~n~l))$.
+\begin{latexonly}\vskip.5em\noindent\end{latexonly}%
+\begin{htmlonly}
+
+\end{htmlonly}
+Given some $P$, then \CI{(\Nil~\nat)}{P} represents the expected type of $f_1$, and
+\CI{(\cons~\nat)}{P} represents the expected type of $f_2$.
 
 \paragraph{Typing rule.}
 
@@ -1428,30 +1340,24 @@ following typing rule
 (\WTEG{f_i}{\CI{(c_{p_i}~q_1\ldots  q_r)}{P}})_{i=1\ldots  l}}
 {\WTEG{\Case{P}{c}{f_1|\ldots  |f_l}}{(P\ t_1\ldots  t_s\ c)}}}%\\[3mm]
 
-provided $I$ is an inductive type in a declaration
-\Ind{\Delta}{r}{\Gamma_I}{\Gamma_C} with 
+provided $I$ is an inductive type in a definition
+\Ind{}{r}{\Gamma_I}{\Gamma_C} with 
 $\Gamma_C = [c_1:C_1;\ldots;c_n:C_n]$ and $c_{p_1}\ldots  c_{p_l}$ are the
 only constructors of $I$.
 \end{description}
 
 \paragraph{Example.}
-For \List\ and \Length\ the typing rules for the {\tt match} expression
-are (writing just $t:M$ instead of \WTEG{t}{M}, the environment and
-context being the same in all the judgments).
-
-\[\frac{l:\ListA~~P:\ListA\ra s~~~f_1:(P~(\Nil~A))~~
-      f_2:\forall a:A, \forall l:\ListA, (P~(\cons~A~a~l))}
-    {\Case{P}{l}{f_1~|~f_2}:(P~l)}\]
-
-\[\frac{
-     \begin{array}[b]{@{}c@{}} 
-H:(\LengthA~L~N) \\ P:\forall l:\ListA, \forall n:\nat, (\LengthA~l~n)\ra
-  \Prop\\
- f_1:(P~(\Nil~A)~\nO~\LNil) \\
-   f_2:\forall a:A, \forall l:\ListA, \forall n:\nat, \forall
-  h:(\LengthA~l~n), (P~(\cons~A~a~n)~(\nS~n)~(\LCons~A~a~l~n~h)) 
-      \end{array}}
-    {\Case{P}{H}{f_1~|~f_2}:(P~L~N~H)}\]
+
+Below is a typing rule for the term shown in the previous example:
+\inference{
+  \frac{%
+    \WTEG{t}{(\List~\nat)}~~~~%
+    \WTEG{P}{B}~~~~%
+    \compat{(\List~\nat)}{B}~~~~%
+    \WTEG{f_1}{\CI{(\Nil~\nat)}{P}}~~~~%
+    \WTEG{f_2}{\CI{(\cons~\nat)}{P}}%
+  }
+{\WTEG{\Case{P}{t}{f_1|f_2}}{(P~t)}}}
 
 \paragraph[Definition of $\iota$-reduction.]{Definition of $\iota$-reduction.\label{iotared}
 \index{iota-reduction@$\iota$-reduction}}
@@ -1496,17 +1402,17 @@ The typing rule is the expected one for a fixpoint.
             (\WTE{\Gamma,f_1:A_1,\ldots,f_n:A_n}{t_i}{A_i})_{i=1\ldots n}}
          {\WTEG{\Fix{f_i}{f_1:A_1:=t_1 \ldots f_n:A_n:=t_n}}{A_i}}}
 \end{description}
-
+%
 Any fixpoint definition cannot be accepted because non-normalizing terms
-will lead to proofs of absurdity.
-
+allow proofs of absurdity.
+%
 The basic scheme of recursion that should be allowed is the one needed for 
 defining primitive
 recursive functionals. In that case the fixpoint enjoys a special
 syntactic restriction, namely one of the arguments belongs to an
 inductive type, the function starts with a case analysis and recursive
 calls are done on variables coming from patterns and representing subterms.
-
+%
 For instance in the case of natural numbers, a proof of the induction
 principle of type 
 \[\forall P:\nat\ra\Prop, (P~\nO)\ra(\forall n:\nat, (P~n)\ra(P~(\nS~n)))\ra
@@ -1519,22 +1425,22 @@ can be represented by the term:
     p:\nat\mto (g~p~(h~p))}}
 \end{array}
 \]
-
+%
 Before accepting a fixpoint definition as being correctly typed, we
 check that the definition is ``guarded''. A precise analysis of this
 notion can be found in~\cite{Gim94}.
-
+%
 The first stage is to precise on which argument the fixpoint will be
 decreasing. The type of this argument should be an inductive
 definition.
-
-For doing this the syntax of fixpoints is extended and becomes 
+%
+For doing this, the syntax of fixpoints is extended and becomes 
  \[\Fix{f_i}{f_1/k_1:A_1:=t_1 \ldots f_n/k_n:A_n:=t_n}\]
 where $k_i$ are positive integers.
+Each $k_i$ represents the index of pararameter of $f_i$, on which $f_i$ is decreasing.
 Each $A_i$ should be a type (reducible to a term) starting with at least
 $k_i$ products $\forall y_1:B_1,\ldots \forall y_{k_i}:B_{k_i}, A'_i$ 
-and $B_{k_i}$
-being an instance of an inductive definition.
+and $B_{k_i}$ an is unductive type.
 
 Now in the definition $t_i$, if $f_j$ occurs then it should be applied
 to at least $k_j$ arguments and the $k_j$-th argument should be
@@ -1544,23 +1450,22 @@ syntactically recognized as structurally smaller than $y_{k_i}$
 The definition of being structurally smaller is a bit technical.
 One needs first to  define the notion of 
 {\em recursive arguments of a constructor}\index{Recursive arguments}.
-For an inductive definition \Ind{\Gamma}{r}{\Gamma_I}{\Gamma_C},
-the type of a constructor $c$ has the form
+For an inductive definition \Ind{}{r}{\Gamma_I}{\Gamma_C},
+if the type of a constructor $c$ has the form
 $\forall p_1:P_1,\ldots \forall p_r:P_r, 
 \forall x_1:T_1, \ldots \forall x_r:T_r, (I_j~p_1\ldots 
-p_r~t_1\ldots  t_s)$ the recursive arguments will correspond to $T_i$ in
+p_r~t_1\ldots  t_s)$, then the recursive arguments will correspond to $T_i$ in
 which one of the $I_l$ occurs.
 
-
 The main rules for being structurally smaller are the following:\\
 Given a variable $y$ of type an inductive
 definition in a declaration 
-\Ind{\Gamma}{r}{\Gamma_I}{\Gamma_C}
+\Ind{}{r}{\Gamma_I}{\Gamma_C}
 where $\Gamma_I$ is $[I_1:A_1;\ldots;I_k:A_k]$, and $\Gamma_C$ is
   $[c_1:C_1;\ldots;c_n:C_n]$.
 The terms structurally smaller than $y$ are:
 \begin{itemize}
-\item $(t~u), \lb x:u \mto t$ when $t$ is structurally smaller than $y$ .
+\item $(t~u)$ and $\lb x:u \mto t$ when $t$ is structurally smaller than $y$.
 \item \Case{P}{c}{f_1\ldots f_n} when each $f_i$ is structurally
   smaller than $y$. \\
   If $c$ is $y$ or is structurally smaller than $y$, its type is an inductive
@@ -1611,33 +1516,15 @@ a_{k_i}) \triangleright_{\iota} \substs{t_i}{f_k}{\Fix{f_k}{F}}{k=1\ldots n}
 when $a_{k_i}$ starts with a constructor.
 This last restriction is needed in order to keep strong normalization
 and corresponds to the reduction for primitive recursive operators.
-
-We can illustrate this behavior on examples.
-\begin{coq_example}
-Goal forall n m:nat, plus (S n) m = S (plus n m).
-reflexivity.
-Abort.
-Goal forall f:forest, sizet (node f) = S (sizef f).
-reflexivity.
-Abort.
-\end{coq_example}
-But assuming the definition of a son function from \tree\ to \forest:
-\begin{coq_example}
-Definition sont (t:tree) : forest 
-   := let (f) := t in f.
-\end{coq_example}
-The following is not a conversion but can be proved after a case analysis.
-% (******************************************************************)
-% (** Error: Impossible to unify ....                              **)
-\begin{coq_example}
-Goal forall t:tree, sizet t = S (sizef (sont t)).
-Fail reflexivity.
-destruct t.
-reflexivity.
-\end{coq_example}
-\begin{coq_eval}
-Abort.
-\end{coq_eval}
+%
+The following reductions are now possible:
+\def\plus{\mathsf{plus}}
+\def\tri{\triangleright_\iota}
+\begin{eqnarray*}
+  \plus~(\nS~(\nS~\nO))~(\nS~\nO) & \tri & \nS~(\plus~(\nS~\nO)~(\nS~\nO))\\
+                                  & \tri & \nS~(\nS~(\plus~\nO~(\nS~\nO)))\\
+                                  & \tri & \nS~(\nS~(\nS~\nO))\\
+\end{eqnarray*}
 
 % La disparition de Program devrait rendre la construction Match obsolete
 % \subsubsection{The {\tt Match \ldots with \ldots end} expression}
@@ -1677,6 +1564,87 @@ Abort.
 The principles of mutual induction can be automatically generated 
 using the {\tt Scheme} command described in Section~\ref{Scheme}.
 
+\section{Admissible rules for global environments}
+
+From the original rules of the type system, one can show the
+admissibility of rules which change the local context of definition of
+objects in the global environment. We show here the admissible rules
+that are used used in the discharge mechanism at the end of a section.
+
+% This is obsolete: Abstraction over defined constants actually uses a
+% let-in since there are let-ins in Coq
+
+%% \paragraph{Mechanism of substitution.}
+
+%% One rule which can be proved valid, is to replace a term $c$ by its
+%% value in the global environment. As we defined the substitution of a term for
+%% a variable in a term, one can define the substitution of a term for a
+%% constant. One easily extends this substitution to local contexts and global
+%% environments.
+
+%% \paragraph{Substitution Property:}
+%% \inference{\frac{\WF{E;c:=t:T; E'}{\Gamma}}
+%%            {\WF{E; \subst{E'}{c}{t}}{\subst{\Gamma}{c}{t}}}}
+
+\paragraph{Abstraction.}
+
+One can modify a global declaration by generalizing it over a
+previously assumed constant $c$. For doing that, we need to modify the
+reference to the global declaration in the subsequent global
+environment and local context by explicitly applying this constant to
+the constant $c'$.
+
+Below, if $\Gamma$ is a context of the form
+$[y_1:A_1;\ldots;y_n:A_n]$, we write $\forall
+x:U,\subst{\Gamma}{c}{x}$ to mean
+$[y_1:\forall~x:U,\subst{A_1}{c}{x};\ldots;y_n:\forall~x:U,\subst{A_n}{c}{x}]$
+and
+$\subst{E}{|\Gamma|}{|\Gamma|c}$.
+to mean the parallel substitution
+$\subst{\subst{E}{y_1}{(y_1~c)}\ldots}{y_n}{(y_n~c)}$.
+
+\paragraph{First abstracting property:}
+ \inference{\frac{\WF{E;c:U;E';c':=t:T;E''}{\Gamma}}
+                 {\WF{E;c:U;E';c':=\lb x:U\mto \subst{t}{c}{x}:\forall~x:U,\subst{T}{c}{x};
+                      \subst{E''}{c'}{(c'~c)}}{\subst{\Gamma}{c}{(c~c')}}}}
+
+ \inference{\frac{\WF{E;c:U;E';c':T;E''}{\Gamma}}
+                 {\WF{E;c:U;E';c':\forall~x:U,\subst{T}{c}{x};
+                      \subst{E''}{c'}{(c'~c)}}{\subst{\Gamma}{c}{(c~c')}}}}
+
+ \inference{\frac{\WF{E;c:U;E';\Ind{}{p}{\Gamma_I}{\Gamma_C};E''}{\Gamma}}
+                 {\WFTWOLINES{E;c:U;E';\Ind{}{p+1}{\forall x:U,\subst{\Gamma_I}{c}{x}}{\forall x:U,\subst{\Gamma_C}{c}{x}};\subst{E''}{|\Gamma_I,\Gamma_C|}{|\Gamma_I,\Gamma_C|~c}}{\subst{\Gamma}{|\Gamma_I,\Gamma_C|}{|\Gamma_I,\Gamma_C|~c}}}}
+%
+One can similarly modify a global declaration by generalizing it over
+a previously defined constant~$c'$.  Below, if $\Gamma$ is a context
+of the form $[y_1:A_1;\ldots;y_n:A_n]$, we write $
+\subst{\Gamma}{c}{u}$ to mean
+$[y_1:\subst{A_1}{c}{u};\ldots;y_n:\subst{A_n}{c}{u}]$.
+
+\paragraph{Second abstracting property:}
+ \inference{\frac{\WF{E;c:=u:U;E';c':=t:T;E''}{\Gamma}}
+           {\WF{E;c:=u:U;E';c':=(\letin{x}{u:U}{\subst{t}{c}{x}}):\subst{T}{c}{u};E''}{\Gamma}}}
+
+ \inference{\frac{\WF{E;c:=u:U;E';c':T;E''}{\Gamma}}
+           {\WF{E;c:=u:U;E';c':\subst{T}{c}{u};E''}{\Gamma}}}
+
+ \inference{\frac{\WF{E;c:=u:U;E';\Ind{}{p}{\Gamma_I}{\Gamma_C};E''}{\Gamma}}
+                 {\WF{E;c:=u:U;E';\Ind{}{p}{\subst{\Gamma_I}{c}{u}}{\subst{\Gamma_C}{c}{u}};E''}{\Gamma}}}
+
+\paragraph{Pruning the local context.}
+If one abstracts or substitutes constants with the above rules then it
+may happen that some declared or defined constant does not occur any
+more in the subsequent global environment and in the local context. One can
+consequently derive the following property.
+
+\paragraph{First pruning property:}
+\inference{\frac{\WF{E;c:U;E'}{\Gamma} \qquad c \mbox{ does not occur in $E'$ and $\Gamma$}}
+                {\WF{E;E'}{\Gamma}}}
+ 
+\paragraph{Second pruning property:}
+\inference{\frac{\WF{E;c:=u:U;E'}{\Gamma} \qquad c \mbox{ does not occur in $E'$ and $\Gamma$}}
+                {\WF{E;E'}{\Gamma}}}
+ 
 \section{Co-inductive types}
 The implementation contains also co-inductive definitions, which are
 types inhabited by infinite objects. 
@@ -1684,14 +1652,14 @@ More information on co-inductive definitions can be found
 in~\cite{Gimenez95b,Gim98,GimCas05}.
 %They are described in Chapter~\ref{Co-inductives}.
 
-\section[\iCIC : the Calculus of Inductive Construction with
-  impredicative \Set]{\iCIC : the Calculus of Inductive Construction with
+\section[The Calculus of Inductive Construction with
+  impredicative \Set]{The Calculus of Inductive Construction with
   impredicative \Set\label{impredicativity}}
 
-\Coq{} can be used as a type-checker for \iCIC{}, the original 
+\Coq{} can be used as a type-checker for the
 Calculus of Inductive Constructions with an impredicative sort \Set{}
 by using the compiler option \texttt{-impredicative-set}.
-
+%
 For example, using the ordinary \texttt{coqtop} command, the following
 is rejected.
 % (** This example should fail *******************************
@@ -1727,8 +1695,6 @@ impredicative system for sort \Set{} become:
       \{\Type(i)\}}
          {\compat{I:\Set}{I\ra s}}}
 \end{description}
-     
-
 
 %%% Local Variables: 
 %%% mode: latex
diff --git a/doc/refman/RefMan-com.tex b/doc/refman/RefMan-com.tex
index 6335dfd324..6f85849888 100644
--- a/doc/refman/RefMan-com.tex
+++ b/doc/refman/RefMan-com.tex
@@ -5,9 +5,9 @@
 
 There are three \Coq~commands: 
 \begin{itemize}
-\item {\tt coqtop}: The \Coq\ toplevel (interactive mode) ; 
-\item {\tt coqc} : The \Coq\ compiler (batch compilation).
-\item {\tt coqchk} : The \Coq\ checker (validation of compiled libraries)
+\item {\tt coqtop}: the \Coq\ toplevel (interactive mode);
+\item {\tt coqc}: the \Coq\ compiler (batch compilation);
+\item {\tt coqchk}: the \Coq\ checker (validation of compiled libraries).
 \end{itemize}
 The options are (basically) the same for the first two commands, and
 roughly described below. You can also look at the \verb!man! pages of
@@ -39,11 +39,10 @@ The {\tt coqc} command takes a name {\em file} as argument.  Then it
 looks for a vernacular file named {\em file}{\tt .v}, and tries to
 compile it into a {\em file}{\tt .vo} file (See ~\ref{compiled}).
 
-\Warning The name {\em file} must be a regular {\Coq} identifier, as
-defined in the Section~\ref{lexical}. It
-must only contain letters, digits or underscores
-(\_). Thus it can be \verb+/bar/foo/toto.v+ but cannot be
-\verb+/bar/foo/to-to.v+.
+\Warning The name {\em file} should be a regular {\Coq} identifier, as
+defined in Section~\ref{lexical}. It should contain only letters, digits
+or underscores (\_). For instance, \verb+/bar/foo/toto.v+ is valid, but
+\verb+/bar/foo/to-to.v+ is invalid.
 
 \section[Customization]{Customization at launch time}
 
@@ -64,7 +63,7 @@ directories to the load path of \Coq.
 It is possible to skip the loading of the resource file with the
 option \verb:-q:.
 
-\section{By environment variables\label{EnvVariables}
+\subsection{By environment variables\label{EnvVariables}
 \index{Environment variables}\label{envars}}
 
 Load path can be specified to the \Coq\ system by setting up
@@ -87,20 +86,19 @@ code. The list of highlight tags can be retrieved with the {\tt -list-tags}
 command-line option of {\tt coqtop}.
 
 \subsection{By command line options\index{Options of the command line}
-\label{vmoption}
 \label{coqoptions}}
 
 The following command-line options are recognized by the commands {\tt
   coqc} and {\tt coqtop}, unless stated otherwise:
 
 \begin{description}
-\item[{\tt -I} {\em directory}, {\tt -include} {\em directory}]\
+\item[{\tt -I} {\em directory}, {\tt -include} {\em directory}]\ %
 
-Add physical path {\em directory} to the {\ocaml} loadpath.
+  Add physical path {\em directory} to the {\ocaml} loadpath.
 
   \SeeAlso Section~\ref{Libraries} and the command {\tt Declare ML Module} Section \ref{compiled}.
 
-\item[\texttt{-Q} \emph{directory} {\dirpath}]\
+\item[{\tt -Q} {\em directory} {\dirpath}]\ %
 
   Add physical path \emph{directory} to the list of directories where
   {\Coq} looks for a file and bind it to the the logical directory
@@ -110,152 +108,184 @@ Add physical path {\em directory} to the {\ocaml} loadpath.
 
   \SeeAlso Section~\ref{Libraries}.
 
-\item[{\tt -R} {\em directory} {\dirpath}]\
+\item[{\tt -R} {\em directory} {\dirpath}]\ %
 
   Do as \texttt{-Q} \emph{directory} {\dirpath} but make the
   subdirectory structure of \emph{directory} recursively visible so
   that the recursive contents of physical \emph{directory} is available
   from {\Coq} using short or partially qualified names.
-  
+
   \SeeAlso Section~\ref{Libraries}.
 
-\item[{\tt -top} {\dirpath}, {\tt -notop}]\ 
+\item[{\tt -top} {\dirpath}]\ %
+
+  Set the toplevel module name to {\dirpath} instead of {\tt Top}. Not
+  valid for {\tt coqc} as the toplevel module name is inferred from the
+  name of the output file.
+
+\item[{\tt -notop}]\ %
+
+  Use the empty logical path for the toplevel module name instead of {\tt
+    Top}. Not valid for {\tt coqc} as the toplevel module name is
+  inferred from the name of the output file.
+
+\item[{\tt -exclude-dir} {\em directory}]\ %
 
-  This sets the toplevel module name to {\dirpath}/the empty logical path instead
-  of {\tt Top}. Not valid for {\tt coqc}.
+  Exclude any subdirectory named {\em directory} while
+  processing options such as {\tt -R} and {\tt -Q}. By default, only the
+  conventional version control management directories named {\tt CVS} and
+  {\tt \_darcs} are excluded.
 
-\item[{\tt -exclude-dir} {\em subdirectory}]\ 
+\item[{\tt -nois}]\ %
 
-  This tells to exclude any subdirectory named {\em subdirectory}
-  while processing option {\tt -R}. Without this option only the
-  conventional version control management subdirectories named {\tt
-  CVS} and {\tt \_darcs} are excluded.
+  Start from an empty state instead of loading the {\tt Init.Prelude}
+  module.
 
-\item[{\tt -nois}]\ 
+\item[{\tt -init-file} {\em file}]\ %
 
-  Cause \Coq~to begin with an empty state.
+  Load {\em file} as the resource file instead of loading the default
+  resource file from the standard configuration directories.
 
-\item[{\tt -init-file} {\em file}, {\tt -q}]\ 
+\item[{\tt -q}]\ %
 
-  Take {\em file} as the resource file. /
-  Cause \Coq~not to load the resource file.
+  Do not to load the default resource file.
 
-\item[{\tt -load-ml-source} {\em file}]\ 
+\item[{\tt -load-ml-source} {\em file}]\ %
 
   Load the {\ocaml} source file {\em file}.
 
-\item[{\tt -load-ml-object} {\em file}]\ 
+\item[{\tt -load-ml-object} {\em file}]\ %
 
   Load the {\ocaml} object file {\em file}.
 
-\item[{\tt -l[v]} {\em file}, {\tt -load-vernac-source[-verbose]} {\em file}]\ 
+\item[{\tt -l} {\em file}, {\tt -load-vernac-source} {\em file}]\ %
+
+  Load and execute the {\Coq} script from {\em file.v}.
+
+\item[{\tt -lv} {\em file}, {\tt -load-vernac-source-verbose} {\em
+    file}]\ %
+
+  Load and execute the {\Coq} script from {\em file.v}.
+  Output its content on the standard input as it is executed.
+
+\item[{\tt -load-vernac-object} {\dirpath}]\ %
 
-  Load \Coq~file {\em file}{\tt .v} optionally with copy it contents on the
-  standard input.
+  Load \Coq~compiled library {\dirpath}. This is equivalent to running
+  {\tt Require} {\dirpath}.
 
-\item[{\tt -load-vernac-object} {\em file}]\ 
+\item[{\tt -require} {\dirpath}]\ %
 
-  Load \Coq~compiled file {\em file}{\tt .vo}
+  Load \Coq~compiled library {\dirpath} and import it. This is equivalent
+  to running {\tt Require Import} {\dirpath}.
 
-\item[{\tt -require} {\em file}]\ 
+\item[{\tt -batch}]\ %
 
-  Load \Coq~compiled file {\em file}{\tt .vo} and import it ({\tt
-    Require} {\em file}).
+  Exit just after argument parsing. Available for {\tt coqtop} only.
 
-\item[{\tt -compile} {\em file},{\tt -compile-verbose} {\em file}, {\tt -batch}]\ 
+\item[{\tt -compile} {\em file.v}]\ %
 
-  {\tt coqtop} options only used internally by {\tt coqc}.
+  Compile file {\em file.v} into {\em file.vo}. This options imply {\tt
+    -batch} (exit just after argument parsing). It is available only
+  for {\tt coqtop}, as this behavior is the purpose of {\tt coqc}.
 
-  This compiles file {\em file}{\tt .v} into {\em file}{\tt .vo} without/with a
-  copy of the contents of the file on standard input.  This option implies options
-  {\tt -batch} (exit just after arguments parsing). It is only
-  available for {\tt coqtop}.
+\item[{\tt -compile-verbose} {\em file.v}]\ %
 
-\item[{\tt -verbose}]\ 
+  Same as {\tt -compile} but also output the content of {\em file.v} as
+  it is compiled.
 
-  This option is only for {\tt coqc}. It tells to compile the file with
-  a copy of its contents on standard input.
+\item[{\tt -verbose}]\ %
+
+  Output the content of the input file as it is compiled. This option is
+  available for {\tt coqc} only; it is the counterpart of {\tt
+    -compile-verbose}.
 
 %Mostly unused in the code
-%\item[{\tt -debug}]\ 
+%\item[{\tt -debug}]\ %
 %
 %  Switch on the debug flag.
 
-\item[{\tt -with-geoproof} (yes|no)]\ 
+\item[{\tt -with-geoproof} (yes|no)]\ %
 
-  Activate or not special functions for Geoproof within {\CoqIDE} (default is yes).
+  Enable or not special functions for Geoproof within {\CoqIDE} (default
+  is yes).
 
-\item[{\tt -color} (on|off|auto)]\
+\item[{\tt -color} (on|off|auto)]\ %
 
-  Activate or not the coloring of output of {\tt coqtop}. The default, auto,
-  means that {\tt coqtop} will dynamically decide whether to activate it
-  depending if the output channels of {\tt coqtop} can handle ANSI styles.
+  Enable or not the coloring of output of {\tt coqtop}. Default is auto,
+  meaning that {\tt coqtop} dynamically decides, depending on whether the
+  output channel supports ANSI escape sequences.
 
-\item[{\tt -beautify}]\ 
+\item[{\tt -beautify}]\ %
 
-  While compiling {\em file}, pretty prints each command just after having parsing
-  it in {\em file}{\tt .beautified} in order to get old-fashion
-  syntax/definitions/notations.
+  Pretty-print each command to {\em file.beautified} when compiling {\em
+    file.v}, in order to get old-fashioned syntax/definitions/notations.
 
-\item[{\tt -emacs}, {\tt -ide-slave}]\ 
+\item[{\tt -emacs}, {\tt -ide-slave}]\ %
 
-  Start a special main loop to communicate with ide.
+  Start a special toplevel to communicate with a specific IDE.
 
-\item[{\tt -impredicative-set}]\ 
+\item[{\tt -impredicative-set}]\ %
 
   Change the logical theory of {\Coq} by declaring the sort {\tt Set}
-  impredicative; warning: this is known to be inconsistent with
+  impredicative. Warning: this is known to be inconsistent with
   some standard axioms of classical mathematics such as the functional
-  axiom of choice or the principle of description
+  axiom of choice or the principle of description.
 
-\item[{\tt -type-in-type}]\
+\item[{\tt -type-in-type}]\ %
 
-  This collapses the universe hierarchy of {\Coq} making the logic inconsistent.
+  Collapse the universe hierarchy of {\Coq}. Warning: this makes the
+  logic inconsistent.
 
-\item[{\tt -compat} {\em version}] \mbox{}
+\item[{\tt -compat} {\em version}]\ %
 
-  Attempt to maintain some of the incompatible changes in their {\em version}
-  behavior.
+  Attempt to maintain some backward-compatibility with a previous version.
 
-\item[{\tt -dump-glob} {\em file}]\ 
+\item[{\tt -dump-glob} {\em file}]\ %
 
-  This dumps references for global names in file {\em file}
-  (to be used by coqdoc, see~\ref{coqdoc})
+  Dump references for global names in file {\em file} (to be used
+  by {\tt coqdoc}, see~\ref{coqdoc}). By default, if {\em file.v} is being
+  compiled, {\em file.glob} is used.
 
-\item[{\tt -no-hash-consing}] \mbox{}
+\item[{\tt -no-glob}]\ %
 
-\item[{\tt -vm}]\ 
+  Disable the dumping of references for global names.
 
-  This activates the use of the bytecode-based conversion algorithm
-  for the current session (see Section~\ref{SetVirtualMachine}).
+%\item[{\tt -no-hash-consing}]\ %
 
-\item[{\tt -image} {\em file}]\ 
+\item[{\tt -image} {\em file}]\ %
 
-  This option sets the binary image to be used by {\tt coqc} to be {\em file}
+  Set the binary image to be used by {\tt coqc} to be {\em file}
   instead of the standard one. Not of general use.
 
-\item[{\tt -bindir} {\em directory}]\ 
+\item[{\tt -bindir} {\em directory}]\ %
+
+  Set the directory containing {\Coq} binaries to be used by {\tt coqc}.
+  It is equivalent to doing \texttt{export COQBIN=}{\em directory} before
+  launching {\tt coqc}.
+
+\item[{\tt -where}]\ %
+
+  Print the location of \Coq's standard library and exit.
 
-  Set for {\tt coqc} the directory containing \Coq\ binaries.
-  It is equivalent to do \texttt{export COQBIN=}{\em directory}
-  before launching {\tt coqc}.
+\item[{\tt -config}]\ %
 
-\item[{\tt -where}, {\tt -config}, {\tt -filteropts}]\ 
+  Print the locations of \Coq's binaries, dependencies, and libraries, then exit.
 
-  Print the \Coq's standard library location or \Coq's binaries, dependencies,
-  libraries locations or the list of command line arguments that {\tt coqtop} has
-  recognize as options and exit.
+\item[{\tt -filteropts}]\ %
 
-\item[{\tt -v}]\ 
+  Print the list of command line arguments that {\tt coqtop} has
+  recognized as options and exit.
 
-  Print the \Coq's version and exit.
+\item[{\tt -v}]\ %
 
-\item[{\tt -list-tags}]\
+  Print \Coq's version and exit.
 
-  Print the highlight tags known by \Coq as well as their currently associated
-  color.
+\item[{\tt -list-tags}]\ %
 
-\item[{\tt -h}, {\tt --help}]\ 
+  Print the highlight tags known by {\Coq} as well as their currently associated
+  color and exit.
+
+\item[{\tt -h}, {\tt --help}]\ %
 
   Print a short usage and exit.
 
@@ -299,18 +329,21 @@ Command-line options {\tt -I}, {\tt -R}, {\tt -where} and
 {\tt -impredicative-set} are supported by {\tt coqchk} and have the
 same meaning as for {\tt coqtop}. Extra options are:
 \begin{description}
-\item[{\tt -norec} $module$]\ 
+\item[{\tt -norec} {\em module}]\ %
+
+  Check {\em module} but do not check its dependencies.
 
-  Check $module$ but do not force check of its dependencies.
-\item[{\tt -admit} $module$] \
+\item[{\tt -admit} {\em module}]\ %
 
-  Do not check $module$ and any of its dependencies, unless
+  Do not check {\em module} and any of its dependencies, unless
   explicitly required.
-\item[{\tt -o}]\ 
+
+\item[{\tt -o}]\ %
 
   At exit, print a summary about the context. List the names of all
   assumptions and variables (constants without body).
-\item[{\tt -silent}]\ 
+
+\item[{\tt -silent}]\ %
 
   Do not write progress information in standard output.
 \end{description}
diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex
index d21c91201d..51e881bff4 100644
--- a/doc/refman/RefMan-ext.tex
+++ b/doc/refman/RefMan-ext.tex
@@ -226,6 +226,7 @@ Definition c := {| y := 3; x := 5 |}.
 This syntax can be disabled globally for printing by
 \begin{quote}
 {\tt Unset Printing Records.}
+\optindex{Printing Records}
 \end{quote}
 For a given type, one can override this using either
 \begin{quote}
@@ -253,6 +254,7 @@ Reset Initial.
 
 \Rem An experimental syntax for projections based on a dot notation is
 available. The command to activate it is
+\optindex{Printing Projections}
 \begin{quote}
 {\tt Set Printing Projections.}
 \end{quote}
@@ -283,12 +285,15 @@ To deactivate the printing of projections, use
 {\tt Unset Printing Projections}.
 
 \subsection{Primitive Projections}
+\optindex{Primitive Projections}
+\optindex{Printing Primitive Projection Parameters}
+\optindex{Printing Primitive Projection Compatibility}
 \index{Primitive projections}
 \label{prim-proj}
 
 The option {\tt Set Primitive Projections} turns on the use of primitive
 projections when defining subsequent records. Primitive projections
-extended the calculus of inductive constructions with a new binary term
+extended the Calculus of Inductive Constructions with a new binary term
 constructor {\tt r.(p)} representing a primitive projection p applied to
 a record object {\tt r} (i.e., primitive projections are always
 applied). Even if the record type has parameters, these do not appear at
@@ -313,6 +318,12 @@ for the usual defined ones.
   % - [pattern x at n], [rewrite x at n] and in general abstraction and selection
   %   of occurrences may fail due to the disappearance of parameters.
 
+For compatibility, the parameters still appear to the user when printing terms
+even though they are absent in the actual AST manipulated by the kernel. This
+can be changed by unsetting the {\tt Printing Primitive Projection Parameters}
+flag. Further compatibility printing can be deactivated thanks to the
+{\tt Printing Primitive Projection Compatibility} option which governs the
+printing of pattern-matching over primitive records.
 
 \section{Variants and extensions of {\mbox{\tt match}}
 \label{Extensions-of-match}
@@ -1249,7 +1260,7 @@ possible, the correct argument will be automatically generated.
 
 \end{ErrMsgs}
 
-\subsection{Declaration of implicit arguments for a constant
+\subsection{Declaration of implicit arguments
 \comindex{Arguments}}
 \label{ImplicitArguments}
 
@@ -1262,7 +1273,7 @@ a priori and a posteriori.
 \subsubsection{Implicit Argument Binders}
 
 In the first setting, one wants to explicitly give the implicit
-arguments of a constant as part of its definition. To do this, one has
+arguments of a declared object as part of its definition. To do this, one has
 to surround the bindings of implicit arguments by curly braces:
 \begin{coq_eval}
 Reset Initial.
@@ -1299,7 +1310,7 @@ usual implicit arguments disambiguation syntax.
 
 \subsubsection{Declaring Implicit Arguments}
 
-To set implicit arguments for a constant a posteriori, one can use the
+To set implicit arguments a posteriori, one can use the
 command:
 \begin{quote}
 \tt Arguments {\qualid} \nelist{\possiblybracketedident}{}
@@ -1378,7 +1389,7 @@ Check (fun l => map length l = map (list nat) nat length l).
 \Rem To know which are the implicit arguments of an object, use the command
 {\tt Print Implicit} (see \ref{PrintImplicit}).
 
-\subsection{Automatic declaration of implicit arguments for a constant}
+\subsection{Automatic declaration of implicit arguments}
 
 {\Coq} can also automatically detect what are the implicit arguments
 of a defined object. The command is just
@@ -1581,7 +1592,7 @@ Implicit arguments names can be redefined using the following syntax:
 \end{quote}
 
 Without the {\tt rename} flag, {\tt Arguments} can be used to assert
-that a given constant has the expected number of arguments and that
+that a given object has the expected number of arguments and that
 these arguments are named as expected.
 
 \noindent {\bf Example (continued): }
@@ -1997,13 +2008,13 @@ variables, use
 \end{quote}
 
 \subsection{Solving existential variables using tactics}
-\ttindex{\textdollar( \ldots )\textdollar}
+\ttindex{ltac:( \ldots )}
 
 \def\expr{\textrm{\textsl{tacexpr}}}
 
 Instead of letting the unification engine try to solve an existential variable
 by itself, one can also provide an explicit hole together with a tactic to solve
-it. Using the syntax {\tt \textdollar(\expr)\textdollar}, the user can put a
+it. Using the syntax {\tt ltac:(\expr)}, the user can put a
 tactic anywhere a term is expected. The order of resolution is not specified and
 is implementation-dependent. The inner tactic may use any variable defined in
 its scope, including repeated alternations between variables introduced by term
@@ -2011,7 +2022,7 @@ binding as well as those introduced by tactic binding. The expression {\expr}
 can be any tactic expression as described at section~\ref{TacticLanguage}.
 
 \begin{coq_example*}
-Definition foo (x : nat) : nat := $( exact x )$.
+Definition foo (x : nat) : nat := ltac:(exact x).
 \end{coq_example*}
 
 This construction is useful when one wants to define complicated terms using
diff --git a/doc/refman/RefMan-gal.tex b/doc/refman/RefMan-gal.tex
index 9b527053c3..fcccd9cb4b 100644
--- a/doc/refman/RefMan-gal.tex
+++ b/doc/refman/RefMan-gal.tex
@@ -311,7 +311,7 @@ called \CIC). The formal presentation of {\CIC} is given in Chapter
 {\annotation} & ::= & {\tt \{ struct} {\ident} {\tt \}} \\ 
 &&\\
 {\caseitem} & ::= & {\term} \zeroone{{\tt as} \name}
-     \zeroone{{\tt in} \pattern} \\
+     \zeroone{{\tt in} \qualid \sequence{\pattern}{}} \\
 &&\\
 {\ifitem} & ::= & \zeroone{{\tt as} {\name}} {\returntype} \\
 &&\\
@@ -322,7 +322,7 @@ called \CIC). The formal presentation of {\CIC} is given in Chapter
 {\multpattern} & ::= & \nelist{\pattern}{\tt ,}\\
 &&\\
 {\pattern} & ::= & {\qualid} \nelist{\pattern}{}  \\
- & $|$ & {\tt @} {\qualid} \sequence{\pattern}{} \\
+ & $|$ & {\tt @} {\qualid} \nelist{\pattern}{} \\
 
  & $|$ & {\pattern} {\tt as} {\ident}             \\
  & $|$ & {\pattern} {\tt \%} {\ident}         \\
@@ -468,8 +468,8 @@ proposition $B$ or the functional dependent product from $A$ to $B$ (a
 construction usually written $\Pi_{x:A}.B$ in set theory).
 
 Non dependent product types have a special notation: ``$A$ {\tt ->}
-$B$'' stands for ``{\tt forall \_:}$A${\tt ,}~$B$''. The non dependent
-product is used both to denote the propositional implication and
+$B$'' stands for ``{\tt forall \_:}$A${\tt ,}~$B$''. The {\em non dependent
+product} is used both to denote the propositional implication and
 function types.
 
 \subsection{Applications
@@ -496,9 +496,8 @@ arguments is used for making explicit the value of implicit arguments
 The expression ``{\term}~{\tt :}~{\type}'' is a type cast
 expression. It enforces the type of {\term} to be {\type}.
 
-``{\term}~{\tt <:}~{\type}'' locally sets up the virtual machine (as if option
-{\tt Virtual Machine} were on, see \ref{SetVirtualMachine}) for checking that
-{\term} has type {\type}.
+``{\term}~{\tt <:}~{\type}'' locally sets up the virtual machine for checking
+that {\term} has type {\type}.
 
 \subsection{Inferable subterms
 \label{hole}
@@ -609,17 +608,20 @@ the type of each branch can depend on the type dependencies specific
 to the branch and the whole pattern-matching expression has a type
 determined by the specific dependencies in the type of the term being
 matched. This dependency of the return type in the annotations of the
-inductive type is expressed using a {\tt
-``in~I~\_~$\ldots$~\_~\ident$_1$~$\ldots$~\ident$_n$}'' clause, where
+inductive type is expressed using a 
+  ``in~I~\_~$\ldots$~\_~\pattern$_1$~$\ldots$~\pattern$_n$'' clause, where
 \begin{itemize}
 \item $I$ is the inductive type of the term being matched;
 
-\item the names \ident$_i$'s correspond to the arguments of the
-inductive type that carry the annotations: the return type is dependent
-on them;
-
-\item the {\_}'s denote the family parameters of the inductive type:
+\item the {\_}'s are matching the parameters of the inductive type:
 the return type is not dependent on them.
+
+\item the \pattern$_i$'s are matching the annotations of the inductive
+  type: the return type is dependent on them
+
+\item in the basic case which we describe below, each \pattern$_i$ is a
+  name \ident$_i$; see \ref{match-in-patterns} for the general case
+
 \end{itemize}
 
 For instance, in the following example:
@@ -971,7 +973,7 @@ are the names of its constructors and {\type$_1$}, {\ldots},
 {\type$_n$} their respective types. The types of the constructors have
 to satisfy a {\em positivity condition} (see Section~\ref{Positivity})
 for {\ident}.  This condition ensures the soundness of the inductive
-definition.  If this is the case, the constants {\ident},
+definition.  If this is the case, the names {\ident},
 {\ident$_1$}, {\ldots}, {\ident$_n$} are added to the environment with
 their respective types.  Accordingly to the universe where
 the inductive type lives ({\it e.g.} its type {\sort}), {\Coq} provides a
@@ -990,7 +992,7 @@ Inductive nat : Set :=
 \end{coq_example}
 
 The type {\tt nat} is defined as the least \verb:Set: containing {\tt
-  O} and closed by the {\tt S} constructor. The constants {\tt nat},
+  O} and closed by the {\tt S} constructor. The names {\tt nat},
 {\tt O} and {\tt S} are added to the environment.
 
 Now let us have a look at the elimination principles. They are three
@@ -1101,7 +1103,7 @@ Inductive list (A:Set) : Set :=
 \end{coq_example*}
 
 Note that in the type of {\tt nil} and {\tt cons}, we write {\tt
-  (list A)} and not just {\tt list}.\\ The constants {\tt nil} and
+  (list A)} and not just {\tt list}.\\ The constructors {\tt nil} and
 {\tt cons} will have respectively types:
 
 \begin{coq_example}
diff --git a/doc/refman/RefMan-ide.tex b/doc/refman/RefMan-ide.tex
index c8d05013b3..c6fbd1c538 100644
--- a/doc/refman/RefMan-ide.tex
+++ b/doc/refman/RefMan-ide.tex
@@ -215,12 +215,13 @@ mouse button, press the key you want for the new shortcut, and release
 the mouse button afterwards. If your system does not allow it, you may still 
 edit this configuration file by hand, but this is more involved.
 
-\section{Using unicode symbols}
+\section{Using Unicode symbols}
 
-\CoqIDE{} supports unicode character encoding in its text windows,
-consequently a large set of symbols is available for notations.
+\CoqIDE{} is based on GTK+ and inherits from it support for Unicode in
+its text windows. Consequently a large set of symbols is available for
+notations.
 
-\subsection{Displaying unicode symbols}
+\subsection{Displaying Unicode symbols}
 
 You just need to define suitable notations as described in
 Chapter~\ref{Addoc-syntax}. For example, to use the mathematical symbols
@@ -236,31 +237,33 @@ file \verb|utf8.v| of \Coq{} library, so you may enable them just by
 \verb|Require utf8| inside \CoqIDE{}, or equivalently, by starting
 \CoqIDE{} with \verb|coqide -l utf8|.
 
-However, there are some issues when using such unicode symbols: you of
+However, there are some issues when using such Unicode symbols: you of
 course need to use a character font which supports them. In the Fonts
-section of the preferences, the Preview line displays some unicode symbols, so
+section of the preferences, the Preview line displays some Unicode symbols, so
 you could figure out if the selected font is OK. Related to this, one
-thing you may need to do is choose whether Gtk should use antialiased
+thing you may need to do is choose whether GTK+ should use antialiased
 fonts or not, by setting the environment variable \verb|GDK_USE_XFT|
 to 1 or 0 respectively.
 
 \subsection{Defining an input method for non ASCII symbols}
 
-To input an Unicode symbol, a general method is to press both the
-CONTROL and the SHIFT keys, and type the hexadecimal code of the
+To input a Unicode symbol, a general method provided by GTK+
+is to simultaneously press the
+Control, Shift and ``u'' keys, release, then type the hexadecimal code of the
 symbol required, for example \verb|2200| for the $\forall$ symbol.
 A list of symbol codes is available at \url{http://www.unicode.org}. 
 
-This method obviously doesn't scale, that's why the preferred alternative is to
-use an Input Method Editor. On POSIX systems (Linux distros, BSD variants and
-MacOS X), you can use \texttt{uim} version 1.6 or later which provides a \LaTeX{}-style
+An alternative method which does not require to know the hexadecimal
+code of the character is to use an Input Method Editor. On POSIX
+systems (Linux distributions, BSD variants and MacOS X), you can use
+\texttt{uim} version 1.6 or later which provides a \LaTeX{}-style
 input method.
 
 To configure \texttt{uim}, execute \texttt{uim-pref-gtk} as your regular user.
 In the "Global Settings" group set the default Input Method to "ELatin" (don't
 forget to tick the checkbox "Specify default IM"). In the "ELatin" group set the
 layout to "TeX", and remember the content of the "[ELatin] on" field (by default
-"<Control>\textbackslash"). You can now execute CoqIDE with the following commands (assuming
+Control-\textbackslash). You can now execute CoqIDE with the following commands (assuming
 you use a Bourne-style shell):
 
 \begin{verbatim}
@@ -268,7 +271,7 @@ $ export GTK_IM_MODULE=uim
 $ coqide
 \end{verbatim}
 
-Activate the ELatin Input Method with Ctrl-\textbackslash, then type the
+Activate the ELatin Input Method with Control-\textbackslash, then type the
 sequence "\verb=\Gamma=". You will see the sequence being
 replaced by $\Gamma$ as soon as you type the second "a".
 
@@ -286,7 +289,7 @@ detect its character encoding.)
 If you choose something else than UTF-8, then missing characters will
 be written encoded by \verb|\x{....}| or \verb|\x{........}| where
 each dot is an hexadecimal digit: the number between braces is the
-hexadecimal UNICODE index for the missing character.
+hexadecimal Unicode index for the missing character.
 
 
 %%% Local Variables: 
diff --git a/doc/refman/RefMan-lib.tex b/doc/refman/RefMan-lib.tex
index 7227f4b7b6..4ebb484e7c 100644
--- a/doc/refman/RefMan-lib.tex
+++ b/doc/refman/RefMan-lib.tex
@@ -17,10 +17,11 @@ The \Coq\ library is structured into two parts:
 
 In addition, user-provided libraries or developments are provided by
 \Coq\ users' community. These libraries and developments are available
-for download at \texttt{http://coq.inria.fr} (see
+for download at \url{http://coq.inria.fr} (see
 Section~\ref{Contributions}).
 
-The chapter briefly reviews the \Coq\ libraries.
+The chapter briefly reviews the \Coq\ libraries whose contents can
+also be browsed at \url{http://coq.inria.fr/stdlib}.
 
 \section[The basic library]{The basic library\label{Prelude}}
 
@@ -799,7 +800,9 @@ At the end, it defines data-types at the {\Type} level.
 \subsection{Tactics}
 
 A few tactics defined at the user level are provided in the initial
-state\footnote{This is in module {\tt Tactics.v}}.
+state\footnote{This is in module {\tt Tactics.v}}. They are listed at
+\url{http://coq.inria.fr/stdlib} (paragraph {\tt Init}, link {\tt
+  Tactics}).
 
 \section{The standard library}
 
@@ -842,7 +845,7 @@ Chapter~\ref{Other-commands}).
 The different modules of the \Coq\ standard library are described in the
 additional document \verb!Library.dvi!. They are also accessible on the WWW
 through the \Coq\ homepage
-\footnote{\texttt{http://coq.inria.fr}}.
+\footnote{\url{http://coq.inria.fr}}.
 
 \subsection[Notations for integer arithmetics]{Notations for integer arithmetics\index{Arithmetical notations}}
 
@@ -1035,7 +1038,7 @@ intros; split_Rmult.
 
 \end{itemize}
 
-All this tactics has been written with the tactic language Ltac
+These tactics has been written with the tactic language Ltac
 described in Chapter~\ref{TacticLanguage}.
 
 \begin{coq_eval}
diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex
index 7011f1ef89..cc7e6b53bf 100644
--- a/doc/refman/RefMan-ltac.tex
+++ b/doc/refman/RefMan-ltac.tex
@@ -367,7 +367,8 @@ There is a for loop that repeats a tactic {\num} times:
 \begin{quote}
 {\tt do} {\num} {\tacexpr}
 \end{quote}
-{\tacexpr} is evaluated to $v$. $v$ must be a tactic value. $v$ is
+{\tacexpr} is evaluated to $v$ which must be a tactic value.
+This tactic value $v$ is
 applied {\num} times. Supposing ${\num}>1$, after the first
 application of $v$, $v$ is applied, at least once, to the generated
 subgoals and so on. It fails if the application of $v$ fails before
@@ -394,7 +395,8 @@ We can catch the tactic errors with:
 \begin{quote}
 {\tt try} {\tacexpr}
 \end{quote}
-{\tacexpr} is evaluated to $v$. $v$ must be a tactic value. $v$ is
+{\tacexpr} is evaluated to $v$ which must be a tactic value.
+The tactic value $v$ is
 applied to each focused goal independently. If the application of $v$
 fails in a goal, it catches the error and leaves the goal
 unchanged. If the level of the exception is positive, then the
@@ -406,7 +408,8 @@ We can check if a tactic made progress with:
 \begin{quote}
 {\tt progress} {\tacexpr}
 \end{quote}
-{\tacexpr} is evaluated to $v$. $v$ must be a tactic value. $v$ is
+{\tacexpr} is evaluated to $v$ which must be a tactic value.
+The tactic value $v$ is
 applied to each focued subgoal independently. If the application of
 $v$ to one of the focused subgoal produced subgoals equal to the
 initial goals (up to syntactical equality), then an error of level 0
@@ -422,7 +425,7 @@ We can branch with the following structure:
 {\tacexpr}$_1$ {\tt +} {\tacexpr}$_2$
 \end{quote}
 {\tacexpr}$_1$ and {\tacexpr}$_2$ are evaluated to $v_1$ and
-$v_2$. $v_1$ and $v_2$ must be tactic values. $v_1$ is applied to each
+$v_2$ which must be tactic values. The tactic value $v_1$ is applied to each
 focused goal independently and if it fails or a later tactic fails,
 then the proof backtracks to the current goal and $v_2$ is applied.
 
@@ -462,7 +465,7 @@ Yet another way of branching without backtracking is the following structure:
 {\tacexpr}$_1$ {\tt ||} {\tacexpr}$_2$
 \end{quote}
 {\tacexpr}$_1$ and {\tacexpr}$_2$ are evaluated to $v_1$ and
-$v_2$. $v_1$ and $v_2$ must be tactic values. $v_1$ is applied in each
+$v_2$ which must be tactic values. The tactic value $v_1$ is applied in each
 subgoal independently and if it fails \emph{to progress} then $v_2$ is
 applied. {\tacexpr}$_1$ {\tt ||} {\tacexpr}$_2$ is equivalent to {\tt
   first [} {\tt progress} {\tacexpr}$_1$ {\tt |} {\tt progress}
@@ -494,7 +497,8 @@ single success \emph{a posteriori}:
 \begin{quote}
 {\tt once} {\tacexpr}
 \end{quote}
-{\tacexpr} is evaluated to $v$. $v$ must be a tactic value. $v$ is
+{\tacexpr} is evaluated to $v$ which must be a tactic value.
+The tactic value $v$ is
 applied but only its first success is used. If $v$ fails, {\tt once}
 {\tacexpr} fails like $v$. If $v$ has a least one success, {\tt once}
 {\tacexpr} succeeds once, but cannot produce more successes.
@@ -505,7 +509,8 @@ Coq provides an experimental way to check that a tactic has \emph{exactly one} s
 \begin{quote}
 {\tt exactly\_once} {\tacexpr}
 \end{quote}
-{\tacexpr} is evaluated to $v$. $v$ must be a tactic value. $v$ is
+{\tacexpr} is evaluated to $v$ which must be a tactic value.
+The tactic value $v$ is
 applied if it has at most one success. If $v$ fails, {\tt
   exactly\_once} {\tacexpr} fails like $v$. If $v$ has a exactly one
 success, {\tt exactly\_once} {\tacexpr} succeeds like $v$. If $v$ has
@@ -592,7 +597,8 @@ amount of time:
 \begin{quote}
 {\tt timeout} {\num} {\tacexpr}
 \end{quote}
-{\tacexpr} is evaluated to $v$. $v$ must be a tactic value. $v$ is
+{\tacexpr} is evaluated to $v$ which must be a tactic value.
+The tactic value $v$ is
 applied normally, except that it is interrupted after ${\num}$ seconds
 if it is still running. In this case the outcome is a failure.
 
@@ -691,6 +697,13 @@ variables of the form {\tt @?id} that occur in head position of an
 application. For these variables, the matching is second-order and
 returns a functional term.
 
+Alternatively, when a metavariable of the form {\tt ?id} occurs under
+binders, say $x_1$, \ldots, $x_n$ and the expression matches, the
+metavariable is instantiated by a term which can then be used in any
+context which also binds the variables $x_1$, \ldots, $x_n$ with
+same types. This provides with a primitive form of matching
+under context which does not require manipulating a functional term.
+
 If the matching with {\cpattern}$_1$ succeeds, then {\tacexpr}$_1$ is
 evaluated into some value by substituting the pattern matching
 instantiations to the metavariables. If {\tacexpr}$_1$ evaluates to a
@@ -1088,7 +1101,7 @@ using the syntax:
 {\tt Ltac} {\qualid} {\ident}$_1$ ... {\ident}$_n$ {\tt ::=}
 {\tacexpr}
 \end{quote}
-A previous definition of \qualid must exist in the environment.
+A previous definition of {\qualid} must exist in the environment.
 The new definition will always be used instead of the old one and
 it goes accross module boundaries.
 
diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex
index c444b5ae05..aea2bae38d 100644
--- a/doc/refman/RefMan-oth.tex
+++ b/doc/refman/RefMan-oth.tex
@@ -975,8 +975,8 @@ the constants {\qualid$_1$} {\ldots} {\qualid$_n$} in tactics using
 $\delta$-conversion (unfolding a constant is replacing it by its
 definition).
 
-{\tt Opaque} has also on effect on the conversion algorithm of {\Coq},
-telling it to delay the unfolding of a constant as mush as possible when
+{\tt Opaque} has also an effect on the conversion algorithm of {\Coq},
+telling it to delay the unfolding of a constant as much as possible when
 {\Coq} has to check the conversion (see Section~\ref{conv-rules})
 of two distinct applied constants.
 
@@ -1083,26 +1083,6 @@ perform a {\tt Ltac \ident\ := {\rm\sl convtactic}}.
 
 \SeeAlso sections \ref{Conversion-tactics}
 
-\subsection{\tt Set Virtual Machine
-\label{SetVirtualMachine}
-\optindex{Virtual Machine}}
-
-This activates the bytecode-based conversion algorithm.
-
-\subsection{\tt Unset Virtual Machine
-\optindex{Virtual Machine}}
-
-This deactivates the bytecode-based conversion algorithm.
-
-\subsection{\tt Test Virtual Machine
-\optindex{Virtual Machine}}
-
-This tells if the bytecode-based conversion algorithm is
-activated. The default behavior is to have the bytecode-based
-conversion algorithm deactivated.
-
-\SeeAlso sections~\ref{vmcompute} and~\ref{vmoption}.
-
 \section{Controlling the locality of commands}
 
 \subsection{{\tt Local}, {\tt Global}
diff --git a/doc/refman/RefMan-pre.tex b/doc/refman/RefMan-pre.tex
index f45072ca43..cb2ab5dc2f 100644
--- a/doc/refman/RefMan-pre.tex
+++ b/doc/refman/RefMan-pre.tex
@@ -956,20 +956,20 @@ Ltac language dependent subgoals, deep backtracking and multiple goal
 handling, along with miscellaneous features and an improved potential
 for future modifications. Dependent subgoals allow statements in a
 goal to mention the proof of another. Proofs of unsolved subgoals
-appear as existential variables. Primitive backtracking make it
+appear as existential variables. Primitive backtracking makes it
 possible to write a tactic with several possible outcomes which are
 tried successively when subsequent tactics fail. Primitives are also
 available to control the backtracking behavior of tactics. Multiple
 goal handling paves the way for smarter automation tactics. It is
 currently used for simple goal manipulation such as goal reordering.
 
-The way Coq processes a document in batch and interactive mode has
+The way {\Coq} processes a document in batch and interactive mode has
 been redesigned by Enrico Tassi with help from Bruno Barras.  Opaque
 proofs, the text between Proof and Qed, can be processed
 asynchronously, decoupling the checking of definitions and statements
 from the checking of proofs.  It improves the responsiveness of
 interactive development, since proofs can be processed in the
-background.  Similarly compilation of a file can be split into two
+background.  Similarly, compilation of a file can be split into two
 phases: the first one checking only definitions and statements and the
 second one checking proofs.  A file resulting from the first
 phase~--~with the .vio extension~--~can be already Required.  All .vio
@@ -977,13 +977,13 @@ files can be turned into complete .vo files in parallel.  The same
 infrastructure also allows terminating tactics to be run in parallel
 on a set of goals via the \verb=par:= goal selector.
 
-CoqIDE was modified to cope with asynchronous checking of the
-document.  Its source code was also made separate from that of Coq, so
-that CoqIDE no longer has a special status among user interfaces,
-paving the way for decoupling its release cycle from that of Coq in
+{\CoqIDE} was modified to cope with asynchronous checking of the
+document.  Its source code was also made separate from that of {\Coq}, so
+that {\CoqIDE} no longer has a special status among user interfaces,
+paving the way for decoupling its release cycle from that of {\Coq} in
 the future.
 
-Carst Tankink developed a Coq back end for user interfaces built on
+Carst Tankink developed a {\Coq} back-end for user interfaces built on
 Makarius Wenzel's Prover IDE framework (PIDE), like PIDE/jEdit (with
 help from Makarius Wenzel) or PIDE/Coqoon (with help from Alexander
 Faithfull and Jesper Bengtson).  The development of such features was
@@ -1017,7 +1017,7 @@ principles such as propositional extensionality and univalence, thanks to
 Maxime Dénès and Bruno Barras. To ensure compatibility with the
 univalence axiom, a new flag ``-indices-matter'' has been implemented, 
 taking into account the universe levels of indices when computing the
-levels of inductive types. This supports using Coq as a tool to explore
+levels of inductive types. This supports using {\Coq} as a tool to explore
 the relations between homotopy theory and type theory.
 
 Maxime Dénès and Benjamin Grégoire developed an implementation of
@@ -1025,17 +1025,23 @@ conversion test and normal form computation using the OCaml native
 compiler. It complements the virtual machine conversion offering much
 faster computation for expensive functions.
 
-{\Coq} 8.5 also comes with a bunch of many various smaller-scale changes
-and improvements regarding the different components of the system.
+{\Coq} 8.5 also comes with a bunch of many various smaller-scale
+changes and improvements regarding the different components of the
+system. We shall only list a few of them.
+
+Pierre Boutillier developed an improved tactic for simplification of
+expressions called {\tt cbn}.
 
-Maxime Dénès maintained the bytecode-based reduction machine.
+Maxime Dénès maintained the bytecode-based reduction machine. Pierre
+Letouzey maintained the extraction mechanism.
 
 Pierre-Marie Pédrot has extended the syntax of terms to,
 experimentally, allow holes in terms to be solved by a locally
 specified tactic.
 
 Existential variables are referred to by identifiers rather than mere
-numbers, thanks to Hugo Herbelin.
+numbers, thanks to Hugo Herbelin who also improved the tactic language
+here and there.
 
 Error messages for universe inconsistencies have been improved by
 Matthieu Sozeau. Error messages for unification and type inference
@@ -1043,14 +1049,42 @@ failures have been improved by Hugo Herbelin, Pierre-Marie Pédrot and
 Arnaud Spiwack.
 
 Pierre Courtieu contributed new features for using {\Coq} through Proof
-General and for better interactive experience (bullets, Search etc).
-
-A distribution channel for Coq packages using the Opam tool has been
-developed by Thomas Braibant and Guillaume Claret.
+General and for better interactive experience (bullets, Search, etc).
+
+The efficiency of the whole system has been significantly improved
+thanks to contributions from Pierre-Marie Pédrot.
+
+A distribution channel for {\Coq} packages using the OPAM tool has
+been initiated by Thomas Braibant and developed by Guillaume Claret,
+with contributions by Enrico Tassi and feedback from Hugo Herbelin.
+
+Packaging tools were provided by Pierre Letouzey and Enrico Tassi
+(Windows), Pierre Boutillier, Matthieu Sozeau and Maxime Dénès (MacOS
+X). Maxime Dénès improved significantly the testing and benchmarking
+support.
+
+Many power users helped to improve the design of the new features via
+the bug tracker, the coq development mailing list or the coq-club
+mailing list. Special thanks are going to the users who contributed
+patches and intensive brain-storming, starting with Jason Gross,
+Jonathan Leivent, Greg Malecha, Clément Pit-Claudel, Marc Lasson,
+Lionel Rieg. It would however be impossible to mention with precision
+all names of people who to some extent influenced the development.
+
+Version 8.5 is one of the most important release of {\Coq}. Its
+development spanned over about 3 years and a half with about one year
+of beta-testing. General maintenance during part or whole of this
+period has been done by Pierre Boutillier, Pierre Courtieu, Maxime
+Dénès, Hugo Herbelin, Pierre Letouzey, Guillaume Melquiond,
+Pierre-Marie Pédrot, Matthieu Sozeau, Arnaud Spiwack, Enrico Tassi as
+well as Bruno Barras, Yves Bertot, Frédéric Besson, Xavier Clerc,
+Pierre Corbineau, Jean-Christophe Filliâtre, Julien Forest, Sébastien
+Hinderer, Assia Mahboubi, Jean-Marc Notin, Yann Régis-Gianas, François
+Ripault, Carst Tankink. Maxime Dénès coordinated the release process.
 
 \begin{flushright}
-Paris, January 2015\\
-Hugo Herbelin \& Matthieu Sozeau\\
+Paris, January 2015, revised December 2015,\\
+Hugo Herbelin, Matthieu Sozeau and the {\Coq} development team\\
 \end{flushright}
 
 
diff --git a/doc/refman/RefMan-pro.tex b/doc/refman/RefMan-pro.tex
index 7af87a399a..c37367de5b 100644
--- a/doc/refman/RefMan-pro.tex
+++ b/doc/refman/RefMan-pro.tex
@@ -157,21 +157,36 @@ in Section~\ref{ProofWith}.
   
   Use only section variables occurring in the statement.
 
-\variant {\tt Proof using -(} {\ident$_1$} {\ldots} {\ident$_n$} {\tt ).}
+\variant {\tt Proof using Type*.} 
+  
+  The {\tt *} operator computes the forward transitive closure.
+  E.g. if the variable {\tt H} has type {\tt p < 5} then {\tt H} is
+  in {\tt p*} since {\tt p} occurs in the type of {\tt H}.
+  {\tt Type* } is the forward transitive closure of the entire set of
+  section variables occurring in the statement.
+
+\variant {\tt Proof using -( \ident$_1$} {\ldots} {\tt \ident$_n$  ).}
   
   Use all section variables except {\ident$_1$} {\ldots} {\ident$_n$}.
 
-\variant {\tt Proof using }  {\emph collection$_1$} {\tt + } {\emph collection$_2$} {\tt .}
-\variant {\tt Proof using }  {\emph collection$_1$} {\tt - } {\emph collection$_2$} {\tt .}
-\variant {\tt Proof using }  {\emph collection$_1$} {\tt - (} {\ident$_1$} {\ldots} {\ident$_n$} {\tt ).}
+\variant {\tt Proof using \nterm{collection}$_1$ + \nterm{collection}$_2$ .}
+
+\variant {\tt Proof using \nterm{collection}$_1$ - \nterm{collection}$_2$ .}
+
+\variant {\tt Proof using \nterm{collection} - ( \ident$_1$} {\ldots} {\tt \ident$_n$ ).}
 
-  Use section variables being in the set union or set difference of the two
-  colelctions.  See Section~\ref{Collection} to know how to form a named
+\variant {\tt Proof using \nterm{collection} * .}
+
+  Use section variables being, respectively, in the set union, set difference,
+  set complement, set forward transitive closure.
+  See Section~\ref{Collection} to know how to form a named
   collection.
+  The {\tt *} operator binds stronger than {\tt +} and {\tt -}.
 
 \subsubsection{{\tt Proof using} options}
-\comindex{Default Proof Using}
-\comindex{Suggest Proof Using}
+\optindex{Default Proof Using}
+\optindex{Suggest Proof Using}
+% \optindex{Proof Using Clear Unused}
 
 The following options modify the behavior of {\tt Proof using}.
 
@@ -186,11 +201,17 @@ The following options modify the behavior of {\tt Proof using}.
   When {\tt Qed} is performed, suggest a {\tt using} annotation if
   the user did not provide one.
 
+% \variant{\tt Unset Proof Using Clear Unused.}
+% 
+%   When {\tt Proof using a} all section variables but for {\tt a} and
+%   the variables used in the type of {\tt a} are cleared.
+%   This option can be used to turn off this behavior.
+% 
 \subsubsection[\tt Collection]{Name a set of section hypotheses for {\tt Proof using}}
 \comindex{Collection}\label{Collection}
 
 The command {\tt Collection} can be used to name a set of section hypotheses,
-with the purpose of making {\tt Proof using} annotations more compat.
+with the purpose of making {\tt Proof using} annotations more compact.
 
 \variant {\tt Collection Some := x y z.}
 
@@ -209,7 +230,7 @@ with the purpose of making {\tt Proof using} annotations more compat.
 \variant {\tt Collection Many := Fewer - (x y).}
 
   Define the collection named "Many" containing the set difference
-  of "Fewer" and the unamed collection {\tt x y}.
+  of "Fewer" and the unnamed collection {\tt x y}.
 
 \subsection[\tt Abort.]{\tt Abort.\comindex{Abort}}
 
@@ -386,6 +407,19 @@ Proof.
 
 \end{ErrMsgs}
 
+The bullet behavior can be controlled by the following commands.
+
+\begin{quote}
+Set Bullet Behavior "None".
+\end{quote}
+
+This makes bullets inactive.
+
+\begin{quote}
+Set Bullet Behavior "Strict Subproofs".
+\end{quote}
+
+This makes bullets active (this is the default behavior).
 
 \section{Requesting information}
 
diff --git a/doc/refman/RefMan-sch.tex b/doc/refman/RefMan-sch.tex
index 571e16d578..53aa6b86ab 100644
--- a/doc/refman/RefMan-sch.tex
+++ b/doc/refman/RefMan-sch.tex
@@ -126,6 +126,8 @@ conclusion is {\tt (n:nat)(even n)->(Q n)}.
 \optindex{Boolean Equality Schemes}
 \optindex{Elimination Schemes}
 \optindex{Nonrecursive Elimination Schemes}
+\optindex{Case Analysis Schemes}
+\optindex{Decidable Equality Schemes}
 \label{set-nonrecursive-elimination-schemes}
 }
 
@@ -139,6 +141,10 @@ and {\tt Record} (see~\ref{Record}) do not have an automatic
 declaration of the induction principles. It can be activated with the
 command {\tt Set Nonrecursive Elimination Schemes}. It can be
 deactivated again with {\tt Unset Nonrecursive Elimination Schemes}.
+
+In addition, the {\tt Case Analysis Schemes} flag governs the generation of
+case analysis lemmas for inductive types, i.e. corresponding to the
+pattern-matching term alone and without fixpoint.
 \\
 
 You can also activate the automatic declaration of those Boolean equalities
diff --git a/doc/refman/RefMan-syn.tex b/doc/refman/RefMan-syn.tex
index aabc8a8995..3af72db78e 100644
--- a/doc/refman/RefMan-syn.tex
+++ b/doc/refman/RefMan-syn.tex
@@ -860,11 +860,11 @@ statically. For instance, if {\tt f} is a polymorphic function of type
 {\scope}, then {\tt a} of type {\tt t} in {\tt f~t~a} is not
 recognized as an argument to be interpreted in scope {\scope}.
 
-\comindex{Bind Scope} 
-Any global reference can be bound by default to an
-interpretation scope. The command to do it is
+\comindex{Bind Scope}
+More generally, any {\class} (see Chapter~\ref{Coercions-full}) can be
+bound to an interpretation scope. The command to do it is
 \begin{quote}
-{\tt Bind Scope} {\scope} \texttt{with} {\qualid}
+{\tt Bind Scope} {\scope} \texttt{with} {\class}
 \end{quote}
 
 \Example
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 315acc0811..f5a1bf3b22 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -219,8 +219,10 @@ difference: the user can leave some holes (denoted by \texttt{\_} or
 {\tt (\_:\type)}) in the term. {\tt refine} will generate as
 many subgoals as there are holes in the term. The type of holes must be
 either synthesized by the system or declared by an
-explicit cast like \verb|(_:nat->Prop)|. This low-level
-tactic can be useful to advanced users.
+explicit cast like \verb|(_:nat->Prop)|. Any subgoal that occurs in other
+subgoals is automatically shelved, as if calling {\tt shelve\_unifiable}
+(see Section~\ref{shelve}).
+This low-level tactic can be useful to advanced users.
 
 \Example
 
@@ -256,6 +258,13 @@ Defined.
   which type cannot be inferred. Put a cast around it.
 \end{ErrMsgs}
 
+\begin{Variants}
+\item {\tt simple refine \term}\tacindex{simple refine}
+
+  This tactic behaves like {\tt refine}, but it does not shelve any
+  subgoal. It does not perform any beta-reduction either.
+\end{Variants}
+
 \subsection{\tt apply \term}
 \tacindex{apply}
 \label{apply}
@@ -793,7 +802,7 @@ the tactic {\tt intro} applies the tactic {\tt hnf} until the tactic
 
 \end{Variants}
 
-\subsection{\tt intros {\intropattern} \mbox{\dots} \intropattern}
+\subsection{\tt intros {\intropatternlist}}
 \label{intros-pattern}
 \tacindex{intros \intropattern}
 \index{Introduction patterns}
@@ -802,9 +811,11 @@ the tactic {\tt intro} applies the tactic {\tt hnf} until the tactic
 \index{Disjunctive/conjunctive introduction patterns}
 \index{Equality introduction patterns}
 
-
-This extension of the tactic {\tt intros} combines introduction of
-variables or hypotheses and case analysis. An {\em introduction pattern} is
+This extension of the tactic {\tt intros} allows to apply tactics on
+the fly on the variables or hypotheses which have been introduced. An
+{\em introduction pattern list} {\intropatternlist} is a list of
+introduction patterns possibly containing the filling introduction
+patterns {\tt *} and {\tt **}. An {\em introduction pattern} is
 either:
 \begin{itemize}
 \item a {\em naming introduction pattern}, i.e. either one of:
@@ -813,12 +824,12 @@ either:
   \item the pattern \texttt{?\ident}
   \item an identifier
   \end{itemize}
-\item a {\em destructing introduction pattern} which itself classifies into:
+\item an {\em action introduction pattern} which itself classifies into:
   \begin{itemize}
   \item a {\em disjunctive/conjunctive introduction pattern}, i.e. either one of:
     \begin{itemize}
     \item a disjunction of lists of patterns:
-      {\tt [$p_{11}$ \dots\ $p_{1m_1}$ | \dots\ | $p_{11}$ \dots\ $p_{nm_n}$]}
+      {\tt [$\intropatternlist_1$ | \dots\ | $\intropatternlist_n$]}
     \item a conjunction of patterns: {\tt ($p_1$ , \dots\ , $p_n$)}
     \item a list of patterns {\tt ($p_1$ \&\ \dots\ \&\ $p_n$)}
       for sequence of right-associative binary constructs
@@ -828,15 +839,13 @@ either:
     \item a pattern for decomposing an equality: {\tt [= $p_1$ \dots\ $p_n$]}
     \item the rewriting orientations: {\tt ->} or {\tt <-}
     \end{itemize}
-  \item the on-the-fly application of a lemma: $p${\tt /{\term}}
+  \item the on-the-fly application of lemmas: $p${\tt \%{\term$_1$}}
+    \ldots {\tt \%{\term$_n$}} where $p$ itself is not a pattern for
+    on-the-fly application of lemmas (note: syntax is in experimental stage)
   \end{itemize}
 \item the wildcard: {\tt \_}
 \end{itemize}
 
-Introduction patterns can be combined into lists. An {\em introduction
-  pattern list} is a list of introduction patterns possibly containing
-the filling introduction patterns {\tt *} and {\tt **}.
-
 Assuming a goal of type $Q \to P$ (non-dependent product), or
 of type $\forall x:T,~P$ (dependent product), the behavior of
 {\tt intros $p$} is defined inductively over the structure of the
@@ -849,20 +858,22 @@ introduction pattern~$p$:
 \item introduction on \texttt{\ident} behaves as described in
   Section~\ref{intro};
 \item introduction over a disjunction of list of patterns {\tt
-  [$p_{11}$ \dots\ $p_{1m_1}$ | \dots\ | $p_{11}$ \dots\ $p_{nm_n}$]}
-  expects the product to be over an inductive type
-  whose number of constructors is $n$ (or more generally over a type
-  of conclusion an inductive type built from $n$ constructors,
-  e.g. {\tt C -> A\textbackslash/B if $n=2$}): it destructs the introduced
-  hypothesis as {\tt destruct} (see Section~\ref{destruct}) would and
-  applies on each generated subgoal the corresponding tactic;
-  \texttt{intros}~$p_{i1}$ {\ldots} $p_{im_i}$; if the disjunctive
-  pattern is part of a sequence of patterns and is not the last
-  pattern of the sequence, then {\Coq} completes the pattern so that all
-  the argument of the constructors of the inductive type are
-  introduced (for instance, the list of patterns {\tt [$\;$|$\;$] H}
-  applied on goal {\tt forall x:nat, x=0 -> 0=x} behaves the same as
-  the list of patterns {\tt [$\,$|$\,$?$\,$] H});
+  [$\intropatternlist_{1}$ | \dots\ | $\intropatternlist_n$]} expects
+  the product to be over an inductive type whose number of
+  constructors is $n$ (or more generally over a type of conclusion an
+  inductive type built from $n$ constructors, e.g. {\tt C ->
+    A\textbackslash/B} with $n=2$ since {\tt A\textbackslash/B} has 2
+  constructors): it destructs the introduced hypothesis as {\tt
+    destruct} (see Section~\ref{destruct}) would and applies on each
+  generated subgoal the corresponding tactic;
+  \texttt{intros}~$\intropatternlist_i$. The introduction patterns in
+  $\intropatternlist_i$ are expected to consume no more than the
+  number of arguments of the $i^{\mbox{\scriptsize th}}$
+  constructor. If it consumes less, then {\Coq} completes the pattern
+  so that all the arguments of the constructors of the inductive type
+  are introduced (for instance, the list of patterns {\tt [$\;$|$\;$]
+    H} applied on goal {\tt forall x:nat, x=0 -> 0=x} behaves the same
+  as the list of patterns {\tt [$\,$|$\,$?$\,$] H});
 \item introduction over a conjunction of patterns {\tt ($p_1$, \ldots,
   $p_n$)} expects the goal to be a product over an inductive type $I$ with a
   single constructor that itself has at least $n$ arguments: it
@@ -876,10 +887,10 @@ introduction pattern~$p$:
   {\tt ($p_1$,(\ldots,(\dots,$p_n$)\ldots))}; it expects the
   hypothesis to be a sequence of right-associative binary inductive
   constructors such as {\tt conj} or {\tt ex\_intro}; for instance, an
-  hypothesis with type {\tt A\verb|/\|exists x, B\verb|/\|C\verb|/\|D} can be
+  hypothesis with type {\tt A\verb|/\|(exists x, B\verb|/\|C\verb|/\|D)} can be
   introduced via pattern {\tt (a \& x \& b \& c \& d)};
 \item if the product is over an equality type, then a pattern of the
-  form {\tt [=$p_{1}$ \dots\ $p_n$]} applies either {\tt injection}
+  form {\tt [= $p_{1}$ \dots\ $p_n$]} applies either {\tt injection}
   (see Section~\ref{injection}) or {\tt discriminate} (see
   Section~\ref{discriminate}) instead of {\tt destruct}; if {\tt
     injection} is applicable, the patterns $p_1$, \ldots, $p_n$ are
@@ -896,9 +907,10 @@ introduction pattern~$p$:
   itself is erased; if the term to substitute is a variable, it is
   substituted also in the context of goal and the variable is removed
   too;
-\item introduction over a pattern $p${\tt /{\term}} first applies
-  {\term} on the hypothesis to be introduced (as in {\tt apply
-  }{\term} {\tt in}), prior to the application of the introduction
+\item introduction over a pattern $p${\tt \%{\term$_1$}} \ldots {\tt
+  \%{\term$_n$}} first applies {\term$_1$},\ldots, {\term$_n$} on the
+  hypothesis to be introduced (as in {\tt apply }{\term}$_1$, \ldots,
+  {\term}$_n$ {\tt in}) prior to the application of the introduction
   pattern $p$;
 \item introduction on the wildcard depends on whether the product is
   dependent or not: in the non-dependent case, it erases the
@@ -913,19 +925,6 @@ introduction pattern~$p$:
   not any more a quantification or an implication.
 \end{itemize}
 
-Then, if $p_1$ ... $p_n$ is a list of introduction patterns possibly
-containing {\tt *} or {\tt **}, {\tt intros $p_1$ ... $p_n$}
-\begin{itemize}
-\item introduction over {\tt *} introduces all forthcoming quantified
-  variables appearing in a row;
-\item introduction over {\tt **} introduces all forthcoming quantified
-  variables or hypotheses until the goal is not any more a
-  quantification or an implication;
-\item introduction over an introduction pattern $p$ introduces the
-  forthcoming quantified variables or premise of the goal and applies
-  the introduction pattern $p$ to it.
-\end{itemize}
-
 \Example
 
 \begin{coq_example}
@@ -936,28 +935,38 @@ intros * [a | (_,c)] f.
 Abort.
 \end{coq_eval}
 
-\Rem {\tt intros $p_1~\ldots~p_n$} is not fully equivalent to
-\texttt{intros $p_1$;\ldots; intros $p_n$} for the following reasons:
-\begin{itemize}
-\item A wildcard pattern never succeeds when applied isolated on a
-  dependent product, while it succeeds as part of a list of
-  introduction patterns if the hypotheses that depends on it are
-  erased too.
-\item A disjunctive or conjunctive pattern followed by an introduction
-  pattern forces the introduction in the context of all arguments of
-  the constructors before applying the next pattern while a terminal
-  disjunctive or conjunctive pattern does not. Here is an example
+\Rem {\tt intros $p_1~\ldots~p_n$} is not equivalent to \texttt{intros
+  $p_1$;\ldots; intros $p_n$} for the following reason: If one of the
+$p_i$ is a wildcard pattern, he might succeed in the first case
+because the further hypotheses it depends in are eventually erased too
+while it might fail in the second case because of dependencies in
+hypotheses which are not yet introduced (and a fortiori not yet
+erased).
+
+\Rem In {\tt intros $\intropatternlist$}, if the last introduction
+pattern is a disjunctive or conjunctive pattern {\tt
+  [$\intropatternlist_1$ | \dots\ | $\intropatternlist_n$]}, the
+completion of $\intropatternlist_i$ so that all the arguments of the
+$i^{\mbox{\scriptsize th}}$ constructors of the corresponding
+inductive type are introduced can be controlled with the
+following option:
+\optindex{Bracketing Last Introduction Pattern}
+
+\begin{quote}
+{\tt Set Bracketing Last Introduction Pattern}
+\end{quote}
+
+Force completion, if needed, when the last introduction pattern is a
+disjunctive or conjunctive pattern (this is the default).
+
+\begin{quote}
+{\tt Unset Bracketing Last Introduction Pattern}
+\end{quote}
+
+Deactivate completion when the last introduction pattern is a disjunctive
+or conjunctive pattern.
 
-\begin{coq_example}
-Goal forall n:nat, n = 0 -> n = 0.
-intros [ | ] H.
-Show 2.
-Undo.
-intros [ | ]; intros H.
-Show 2.
-\end{coq_example}
 
-\end{itemize}
 
 \subsection{\tt clear \ident}
 \tacindex{clear}
@@ -1246,18 +1255,9 @@ in the list of subgoals remaining to prove.
   introduction pattern (in particular, if {\intropattern} is {\ident},
   the tactic behaves like \texttt{assert ({\ident} :\ {\form})}).
 
-  If {\intropattern} is a disjunctive/conjunctive 
-  introduction pattern, the tactic behaves like \texttt{assert
-    {\form}} followed by a {\tt destruct} using this introduction pattern.
-
-  If {\intropattern} is a rewriting intropattern pattern, the tactic
-  behaves like \texttt{assert {\form}} followed by a call to {\tt
-    subst} on the resulting hypothesis, if applicable, or to {\tt
-    rewrite} otherwise.
-
-  If {\intropattern} is an injection intropattern pattern, the tactic
-  behaves like \texttt{assert {\form}} followed by {\tt injection}
-  using this introduction pattern.
+  If {\intropattern} is an action introduction pattern, the tactic
+  behaves like \texttt{assert {\form}} followed by the action done by
+  this introduction pattern.
 
 \item \texttt{assert {\form} as {\intropattern} by {\tac}}
 
@@ -1456,6 +1456,24 @@ a hypothesis or in the body or the type of a local definition.
 
 \end{Variants}
 
+\subsection{\tt admit}
+\tacindex{admit}
+\tacindex{give\_up}
+\label{admit}
+
+The {\tt admit} tactic allows temporarily skipping a subgoal so as to
+progress further in the rest of the proof.  A proof containing
+admitted goals cannot be closed with {\tt Qed} but only with
+{\tt Admitted}.
+
+\begin{Variants}
+
+  \item {\tt give\_up}
+
+    Synonym of {\tt admit}.
+
+\end{Variants}
+
 \subsection{\tt absurd \term}
 \tacindex{absurd}
 \label{absurd}
@@ -1528,25 +1546,27 @@ for each possible form of {\term}, i.e. one for each constructor of
 the inductive or co-inductive type. Unlike {\tt induction}, no
 induction hypothesis is generated by {\tt destruct}.
 
-If the argument is dependent in either the conclusion or some
-hypotheses of the goal, the argument is replaced by the appropriate
-constructor form in each of the resulting subgoals, thus performing
-case analysis. If non-dependent, the tactic simply exposes the
-inductive or co-inductive structure of the argument.
-
 There are special cases:
 
 \begin{itemize}
 
 \item If {\term} is an identifier {\ident} denoting a quantified
-variable of the conclusion of the goal, then {\tt destruct {\ident}}
-behaves as {\tt intros until {\ident}; destruct {\ident}}.
+  variable of the conclusion of the goal, then {\tt destruct {\ident}}
+  behaves as {\tt intros until {\ident}; destruct {\ident}}. If
+  {\ident} is not anymore dependent in the goal after application of
+  {\tt destruct}, it is erased (to avoid erasure, use
+  parentheses, as in {\tt destruct ({\ident})}).
 
 \item If {\term} is a {\num}, then {\tt destruct {\num}} behaves as
 {\tt intros until {\num}} followed by {\tt destruct} applied to the
 last introduced hypothesis. Remark: For destruction of a numeral, use
 syntax {\tt destruct ({\num})} (not very interesting anyway).
 
+\item In case {\term} is an hypothesis {\ident} of the context,
+  and {\ident} is not anymore dependent in the goal after
+  application of {\tt destruct}, it is erased (to avoid erasure, use
+  parentheses, as in {\tt destruct ({\ident})}).
+
 \item The argument {\term} can also be a pattern of which holes are
   denoted by ``\_''. In this case, the tactic checks that all subterms
   matching the pattern in the conclusion and the hypotheses are
@@ -1623,14 +1643,6 @@ syntax {\tt destruct ({\num})} (not very interesting anyway).
   They combine the effects of the {\tt with}, {\tt as}, {\tt eqn:}, {\tt using},
   and {\tt in} clauses.
 
-\item{\tt destruct !{\ident}}
-
-  This is a case when the destructed term is an hypothesis of the
-  context. The ``!'' modifier tells to keep the hypothesis in the
-  context after destruction.
-
-  This applies also to the other form of {\tt destruct} and {\tt edestruct}.
-
 \item{\tt case \term}\label{case}\tacindex{case}
 
   The tactic {\tt case} is a more basic tactic to perform case
@@ -1696,14 +1708,22 @@ There are particular cases:
 \begin{itemize}
 
 \item If {\term} is an identifier {\ident} denoting a quantified
-variable of the conclusion of the goal, then {\tt induction {\ident}}
-behaves as {\tt intros until {\ident}; induction {\ident}}.
+  variable of the conclusion of the goal, then {\tt induction
+    {\ident}} behaves as {\tt intros until {\ident}; induction
+    {\ident}}.  If {\ident} is not anymore dependent in the goal
+  after application of {\tt induction}, it is erased (to avoid
+  erasure, use parentheses, as in {\tt induction ({\ident})}).
 
 \item If {\term} is a {\num}, then {\tt induction {\num}} behaves as
 {\tt intros until {\num}} followed by {\tt induction} applied to the
 last introduced hypothesis. Remark: For simple induction on a numeral,
 use syntax {\tt induction ({\num})} (not very interesting anyway).
 
+\item In case {\term} is an hypothesis {\ident} of the context,
+  and {\ident} is not anymore dependent in the goal after
+  application of {\tt induction}, it is erased (to avoid erasure, use
+  parentheses, as in {\tt induction ({\ident})}).
+
 \item The argument {\term} can also be a pattern of which holes are
   denoted by ``\_''. In this case, the tactic checks that all subterms
   matching the pattern in the conclusion and the hypotheses are
@@ -1818,15 +1838,6 @@ Show 2.
   einduction}.  It combines the effects of the {\tt with}, {\tt as}, %%{\tt eqn:},
   {\tt using}, and {\tt in} clauses.
 
-\item{\tt induction !{\ident}}
-
-  This is a case when the term on which to apply induction is an
-  hypothesis of the context. The ``!'' modifier tells to keep the
-  hypothesis in the context after induction.
-
-  This applies also to the other form of {\tt induction} and {\tt
-    einduction}.
-
 \item {\tt elim \term}\label{elim}
 
   This is a more basic induction tactic.  Again, the type of the
@@ -3015,23 +3026,33 @@ variables bound by a let-in construction inside the term itself (use
 here the {\tt zeta} flag). In any cases, opaque constants are not
 unfolded (see Section~\ref{Opaque}).
 
-The goal may be normalized with two strategies: {\em lazy} ({\tt lazy}
-tactic), or {\em call-by-value} ({\tt cbv} tactic). The lazy strategy
-is a call-by-need strategy, with sharing of reductions: the arguments of a
-function call are partially evaluated only when necessary, and if an
-argument is used several times then it is computed only once. This
-reduction is efficient for reducing expressions with dead code. For
-instance, the proofs of a proposition {\tt exists~$x$. $P(x)$} reduce to a
-pair of a witness $t$, and a proof that $t$ satisfies the predicate
-$P$. Most of the time, $t$ may be computed without computing the proof
-of $P(t)$, thanks to the lazy strategy.
+Normalization according to the flags is done by first evaluating the
+head of the expression into a {\em weak-head} normal form, i.e. until
+the evaluation is bloked by a variable (or an opaque constant, or an
+axiom), as e.g. in {\tt x\;u$_1$\;...\;u$_n$}, or {\tt match x with
+  ... end}, or {\tt (fix f x \{struct x\} := ...) x}, or is a
+constructed form (a $\lambda$-expression, a constructor, a cofixpoint,
+an inductive type, a product type, a sort), or is a redex that the
+flags prevent to reduce. Once a weak-head normal form is obtained,
+subterms are recursively reduced using the same strategy.
+
+Reduction to weak-head normal form can be done using two strategies:
+{\em lazy} ({\tt lazy} tactic), or {\em call-by-value} ({\tt cbv}
+tactic). The lazy strategy is a call-by-need strategy, with sharing of
+reductions: the arguments of a function call are weakly evaluated only
+when necessary, and if an argument is used several times then it is
+weakly computed only once. This reduction is efficient for reducing
+expressions with dead code. For instance, the proofs of a proposition
+{\tt exists~$x$. $P(x)$} reduce to a pair of a witness $t$, and a
+proof that $t$ satisfies the predicate $P$. Most of the time, $t$ may
+be computed without computing the proof of $P(t)$, thanks to the lazy
+strategy.
 
 The call-by-value strategy is the one used in ML languages: the
-arguments of a function call are evaluated first, using a weak
-reduction (no reduction under the $\lambda$-abstractions). Despite the
-lazy strategy always performs fewer reductions than the call-by-value
-strategy, the latter is generally more efficient for evaluating purely
-computational expressions (i.e. with few dead code).
+arguments of a function call are systematically weakly evaluated
+first. Despite the lazy strategy always performs fewer reductions than
+the call-by-value strategy, the latter is generally more efficient for
+evaluating purely computational expressions (i.e. with few dead code).
 
 \begin{Variants}
 \item {\tt compute} \tacindex{compute}\\
@@ -3394,7 +3415,7 @@ local definition. Example: {\tt unfold not in (Type of H1) (Type of H3).}
 This tactic implements a Prolog-like resolution procedure to solve the
 current goal. It first tries to solve the goal using the {\tt
   assumption} tactic, then it reduces the goal to an atomic one using
-{\tt intros} and introducing the newly generated hypotheses as hints.
+{\tt intros} and introduces the newly generated hypotheses as hints.
 Then it looks at the list of tactics associated to the head symbol of
 the goal and tries to apply one of them (starting from the tactics
 with lower cost). This process is recursively applied to the generated
@@ -3454,11 +3475,10 @@ intact. \texttt{auto} and \texttt{trivial} never fail.
 \tacindex{eauto}
 \label{eauto}
 
-This tactic generalizes {\tt auto}. In contrast with
-the latter, {\tt eauto} uses unification of the goal
-against the hints rather than pattern-matching
-(in other words, it uses {\tt eapply} instead of
-{\tt apply}).
+This tactic generalizes {\tt auto}. While {\tt auto} does not try
+resolution hints which would leave existential variables in the goal,
+{\tt eauto} does try them (informally speaking, it uses {\tt eapply}
+where {\tt auto} uses {\tt apply}).
 As a consequence, {\tt eauto} can solve such a goal:
 
 \begin{coq_eval}
@@ -3560,7 +3580,7 @@ The hints for \texttt{auto} and \texttt{eauto} are stored in
 databases.  Each database maps head symbols to a list of hints. One can
 use the command \texttt{Print Hint \ident} to display the hints
 associated to the head symbol \ident{} (see \ref{PrintHint}). Each
-hint has a cost that is an nonnegative integer, and an optional pattern.
+hint has a cost that is a nonnegative integer, and an optional pattern.
 The hints with lower cost are tried first. A hint is tried by
 \texttt{auto} when the conclusion of the current goal
 matches its pattern or when it has no pattern.
@@ -3623,33 +3643,36 @@ The {\hintdef} is one of the following expressions:
 \item {\tt Resolve \term}
   \comindex{Hint Resolve}
 
-  This command adds {\tt apply {\term}} to the hint list
+  This command adds {\tt simple apply {\term}} to the hint list
   with the head symbol of the type of \term. The cost of that hint is
-  the number of subgoals generated by {\tt apply {\term}}.
-
-  In case the inferred type of \term\ does not start with a product the
-  tactic added in the hint list is {\tt exact {\term}}. In case this
-  type can be reduced to a type starting with a product, the tactic {\tt
-    apply {\term}} is also stored in the hints list.
-
-  If the inferred type of \term\ contains a dependent
-  quantification on a predicate, it is added to the hint list of {\tt
-    eapply} instead of the hint list of {\tt apply}. In this case, a
-  warning is printed since the hint is only used by the tactic {\tt
-    eauto} (see \ref{eauto}). A typical example of a hint that is used
-  only by \texttt{eauto} is a transitivity lemma.
+  the number of subgoals generated by {\tt simple apply {\term}}.
+%{\tt auto} actually uses a slightly modified variant of {\tt simple apply} with use_metas_eagerly_in_conv_on_closed_terms set to false
+
+  % Is it really needed?
+  %% In case the inferred type of \term\ does not start with a product
+  %% the tactic added in the hint list is {\tt exact {\term}}. In case
+  %% this type can however be reduced to a type starting with a product,
+  %% the tactic {\tt apply {\term}} is also stored in the hints list.
+
+  If the inferred type of \term\ contains a dependent quantification
+  on a variable which occurs only in the premisses of the type and not
+  in its conclusion, no instance could be inferred for the variable by
+  unification with the goal. In this case, the hint is added to the
+  hint list of {\tt eauto} (see \ref{eauto}) instead of the hint list
+  of {\tt auto} and a warning is printed. A typical example of a hint
+  that is used only by \texttt{eauto} is a transitivity lemma.
 
   \begin{ErrMsgs}
-  \item \errindex{Bound head variable}
+%%  \item \errindex{Bound head variable}
+
+  \item \term\ \errindex{cannot be used as a hint}
 
     The head symbol of the type of {\term} is a bound variable such
     that this tactic cannot be associated to a constant.
 
-  \item \term\ \errindex{cannot be used as a hint}
-
-    The type of {\term} contains products over variables that do not
-    appear in the conclusion. A typical example is a transitivity axiom.
-    In that case the {\tt apply} tactic fails, and thus is useless.
+    %% The type of {\term} contains products over variables that do not
+    %% appear in the conclusion. A typical example is a transitivity axiom.
+    %% In that case the {\tt simple apply} tactic fails, and thus is useless.
 
   \end{ErrMsgs}
 
@@ -3664,10 +3687,10 @@ The {\hintdef} is one of the following expressions:
 \item \texttt{Immediate {\term}}
 \comindex{Hint Immediate}
 
-  This command adds {\tt apply {\term}; trivial} to the hint list
+  This command adds {\tt simple apply {\term}; trivial} to the hint list
   associated with the head symbol of the type of {\ident} in the given
   database. This tactic will fail if all the subgoals generated by
-  {\tt apply {\term}} are not solved immediately by the {\tt trivial}
+  {\tt simple apply {\term}} are not solved immediately by the {\tt trivial}
   tactic (which only tries tactics with cost $0$).
 
   This command is useful for theorems such as the symmetry of equality
@@ -3679,7 +3702,7 @@ The {\hintdef} is one of the following expressions:
 
   \begin{ErrMsgs}
 
-  \item \errindex{Bound head variable}
+%%  \item \errindex{Bound head variable}
 
   \item \term\ \errindex{cannot be used as a hint}
 
@@ -3705,7 +3728,9 @@ The {\hintdef} is one of the following expressions:
 
     \item {\ident} \errindex{is not an inductive type}
 
-    \item {\ident} \errindex{not declared}
+% No need to have this message here, is is generic to all commands
+% referring to globals
+%%    \item {\ident} \errindex{not declared}
 
   \end{ErrMsgs}
 
@@ -3769,7 +3794,7 @@ Hint Extern 4 (~(_ = _)) => discriminate.
   with hints with a cost less than 4.
 
   One can even use some sub-patterns of the pattern in the tactic
-  script. A sub-pattern is a question mark followed by an ident, like
+  script. A sub-pattern is a question mark followed by an identifier, like
   \texttt{?X1} or \texttt{?X2}. Here is an example:
 
 % Require EqDecide.
@@ -3781,37 +3806,71 @@ Hint Extern 5   ({?X1 = ?X2} + {?X1 <> ?X2}) =>
  generalize X1, X2; decide equality : eqdec.
 Goal
 forall a b:list (nat * nat), {a = b} + {a <> b}.
-info_auto with eqdec.
+Info 1 auto with eqdec.
 \end{coq_example}
 \begin{coq_eval}
 Abort.
 \end{coq_eval}
 
+\item \texttt{Cut} {\textit{regexp}}
+\label{HintCut}
+\comindex{Hint Cut}
+
+  \textit{Warning:} these hints currently only apply to typeclass proof search and
+  the \texttt{typeclasses eauto} tactic.
+
+  This command can be used to cut the proof-search tree according to a
+  regular expression matching paths to be cut. The grammar for regular
+  expressions is the following:
+\[\begin{array}{lcll}
+  e & ::= & \ident & \text{ hint or instance identifier } \\
+  & & \texttt{*} & \text{ any hint } \\
+  & & e | e' & \text{ disjunction } \\
+  & & e ; e' & \text{ sequence } \\
+  & & ! e & \text{ Kleene star } \\
+  & & \texttt{emp} & \text{ empty } \\
+  & & \texttt{eps} & \text{ epsilon } \\
+  & & \texttt{(} e \texttt{)} & 
+\end{array}\]
+
+The \texttt{emp} regexp does not match any search path while
+\texttt{eps} matches the empty path. During proof search, the path of
+successive successful hints on a search branch is recorded, as a list of
+identifiers for the hints (note \texttt{Hint Extern}'s do not have an
+associated identifier). Before applying any hint $\ident$ the current
+path $p$ extended with $\ident$ is matched against the current cut
+expression $c$ associated to the hint database. If matching succeeds,
+the hint is \emph{not} applied. The semantics of \texttt{Hint Cut} $e$
+is to set the cut expression to $c | e$, the initial cut expression
+being \texttt{emp}.
+
+
+\item \texttt{Mode} {\tt (+ | -)}$^*$ {\qualid}
+\label{HintMode}
+\comindex{Hint Mode}
+
+This sets an optional mode of use of the identifier {\qualid}.  When
+proof-search faces a goal that ends in an application of {\qualid} to
+arguments {\tt \term$_1$ \mbox{\dots} \term$_n$}, the mode tells if the
+hints associated to qualid can be applied or not. A mode specification 
+is a list of $n$ {\tt +} or {\tt -} items that specify if an argument is
+to be treated as an input {\tt +} or an output {\tt -} of the
+identifier. For a mode to match a list of arguments, input terms \emph{must
+not} contain existential variables, while outputs can be any term.
+Multiple modes can be declared for a single identifier, in that case 
+only one mode needs to match the arguments for the hints to be applied.
+
+{\tt Hint Mode} is especially useful for typeclasses, when one does not
+want to support default instances and avoid ambiguity in
+general. Setting a parameter of a class as an input forces proof-search
+to be driven by that index of the class.
+
 \end{itemize}
 
 \Rem One can use an \texttt{Extern} hint with no pattern to do
 pattern-matching on hypotheses using \texttt{match goal with} inside
 the tactic.
 
-\begin{Variants}
-\item {\tt Hint \hintdef}
-
-  No database name is given: the hint is registered in the {\tt core}
-    database.
-
-\item {\tt Hint Local {\hintdef} : \ident$_1$ \mbox{\dots} \ident$_n$}
-
-  This is used to declare hints that must not be exported to the other
-  modules that require and import the current module. Inside a
-  section, the option {\tt Local} is useless since hints do not
-  survive anyway to the closure of sections.
-
-\item {\tt Hint Local \hintdef}
-
-  Idem for the {\tt core} database.
-
-\end{Variants}
-
 % There are shortcuts that allow to define several goal at once:
 
 % \begin{itemize}
@@ -4075,6 +4134,7 @@ The tactic {\tt exists (n // m)} did not fail. The hole was solved by
 
 \subsection{\tt tauto}
 \tacindex{tauto}
+\tacindex{dtauto}
 \label{tauto}
 
 This tactic implements a decision procedure for intuitionistic propositional
@@ -4123,8 +4183,21 @@ Abort.
 because \verb=(forall x:nat, ~ A -> P x)= cannot be treated as atomic and an
 instantiation of \verb=x= is necessary.
 
+\begin{Variants}
+
+\item {\tt dtauto}
+
+  While {\tt tauto} recognizes inductively defined connectives
+  isomorphic to the standard connective {\tt and}, {\tt prod}, {\tt
+    or}, {\tt sum}, {\tt False}, {\tt Empty\_set}, {\tt unit}, {\tt
+    True}, {\tt dtauto} recognizes also all inductive types with
+  one constructors and no indices, i.e. record-style connectives.
+
+\end{Variants}
+
 \subsection{\tt intuition \tac}
 \tacindex{intuition}
+\tacindex{dintuition}
 \label{intuition}
 
 The tactic \texttt{intuition} takes advantage of the search-tree built
@@ -4157,8 +4230,49 @@ incompatibilities.
 \item {\tt intuition}
 
   Is equivalent to {\tt intuition auto with *}.
+
+\item {\tt dintuition}
+
+  While {\tt intuition} recognizes inductively defined connectives
+  isomorphic to the standard connective {\tt and}, {\tt prod}, {\tt
+    or}, {\tt sum}, {\tt False}, {\tt Empty\_set}, {\tt unit}, {\tt
+    True}, {\tt dintuition} recognizes also all inductive types with
+  one constructors and no indices, i.e. record-style connectives.
+
 \end{Variants}
 
+\optindex{Intuition Negation Unfolding}
+\optindex{Intuition Iff Unfolding}
+
+Some aspects of the tactic {\tt intuition} can be
+controlled using options. To avoid that inner negations which do not
+need to be unfolded are unfolded, use:
+
+\begin{quote}
+{\tt Unset Intuition Negation Unfolding}
+\end{quote}
+
+To do that all negations of the goal are unfolded even inner ones
+(this is the default), use:
+
+\begin{quote}
+{\tt Set Intuition Negation Unfolding}
+\end{quote}
+
+To avoid that inner occurrence of {\tt iff} which do not need to be
+unfolded are unfolded (this is the default), use:
+
+\begin{quote}
+{\tt Unset Intuition Iff Unfolding}
+\end{quote}
+
+To do that all negations of the goal are unfolded even inner ones
+(this is the default), use:
+
+\begin{quote}
+{\tt Set Intuition Iff Unfolding}
+\end{quote}
+
 % En attente d'un moyen de valoriser les fichiers de demos
 %\SeeAlso file \texttt{contrib/Rocq/DEMOS/Demo\_tauto.v}
 
@@ -4634,7 +4748,7 @@ Use \texttt{classical\_right} to prove the right part of the disjunction with th
 %% procedure for first-order intuitionistic logic implemented in {\em
 %%   NuPRL}\cite{Kre02}.
 
-%% Search may optionnaly be bounded by a multiplicity parameter
+%% Search may optionally be bounded by a multiplicity parameter
 %% indicating how many (at most) copies of a formula may be used in
 %% the proof process, its absence may lead to non-termination of the tactic.
 
@@ -4926,8 +5040,8 @@ back into focus with the command {\tt Unshelve} (Section~\ref{unshelve}).
 \begin{Variants}
   \item \texttt{shelve\_unifiable}\tacindex{shelve\_unifiable}
 
-    Shelves only these goals under focused which are mentioned in other goals.
-    Goals which appear in the type of other goals can be solve by unification.
+    Shelves only the goals under focus that are mentioned in other goals.
+    Goals that appear in the type of other goals can be solved by unification.
 
 \Example
 \begin{coq_example}
diff --git a/doc/refman/RefMan-uti.tex b/doc/refman/RefMan-uti.tex
index 0729391062..c282083b5c 100644
--- a/doc/refman/RefMan-uti.tex
+++ b/doc/refman/RefMan-uti.tex
@@ -102,7 +102,7 @@ generator using for instance the command:
 
 This command generates a file \texttt{Makefile} that can be used to
 compile all the sources of the current project. It follows the
-syntax described by the output of \texttt{\% coq\_makefile --help}.
+syntax described by the output of \texttt{\% coq\_makefile ----help}.
 Once the \texttt{Makefile} file has been generated a first time, it
 can be used by the \texttt{make} command to compile part or all of
 the project. Note that once it has been generated once, as soon as
diff --git a/doc/refman/Reference-Manual.tex b/doc/refman/Reference-Manual.tex
index ac28e0ba03..dcb98d96b3 100644
--- a/doc/refman/Reference-Manual.tex
+++ b/doc/refman/Reference-Manual.tex
@@ -20,6 +20,11 @@
 \usepackage{headers} % in this directory
 \usepackage{multicol}
 \usepackage{xspace}
+\usepackage{pmboxdraw}
+\usepackage{float}
+
+\floatstyle{boxed} 
+\restylefloat{figure}
 
 % for coqide
 \ifpdf   % si on est pas en pdflatex
diff --git a/doc/refman/Universes.tex b/doc/refman/Universes.tex
index 018d73908b..a08cd1475a 100644
--- a/doc/refman/Universes.tex
+++ b/doc/refman/Universes.tex
@@ -7,14 +7,12 @@
 \asection{General Presentation}
 
 \begin{flushleft}
-  \em The status of Universe Polymorphism is experimental. Some features
-  are not compatible with it (yet): bytecode compilation does not handle
-  polymorphic definitions, it treats them as opaque constants.
+  \em The status of Universe Polymorphism is experimental.
 \end{flushleft}
 
 This section describes the universe polymorphic extension of Coq.
-Universe polymorphism allows writing generic definitions making use of
-universes and reuse them at different and sometimes incompatible levels.
+Universe polymorphism makes it possible to write generic definitions making use of
+universes and reuse them at different and sometimes incompatible universe levels.
 
 A standard example of the difference between universe \emph{polymorphic} and
 \emph{monomorphic} definitions is given by the identity function:
@@ -65,11 +63,11 @@ Now \texttt{pidentity} is used at two different levels: at the head of
 the application it is instantiated at \texttt{Top.3} while in the
 argument position it is instantiated at \texttt{Top.4}. This definition
 is only valid as long as \texttt{Top.4} is strictly smaller than
-\texttt{Top.3}, as show by the constraints. Not that this definition is
-monomorphic (not universe polymorphic), so in turn the two universes are
-actually global levels.
+\texttt{Top.3}, as show by the constraints. Note that this definition is
+monomorphic (not universe polymorphic), so the two universes
+(in this case \texttt{Top.3} and \texttt{Top.4}) are actually global levels.
 
-Inductive types can also be declared universes polymorphic, on universes
+Inductive types can also be declared universes polymorphic on universes
 appearing in their parameters or fields. A typical example is given by
 monoids:
 
@@ -81,7 +79,7 @@ Print Monoid.
 
 The \texttt{Monoid}'s carrier universe is polymorphic, hence it is
 possible to instantiate it for example with \texttt{Monoid} itself.
-First we build the trivial unit monoid, in \texttt{Set}:
+First we build the trivial unit monoid in \texttt{Set}:
 \begin{coq_example}
 Definition unit_monoid : Monoid := 
   {| mon_car := unit; mon_unit := tt; mon_op x y := tt |}.
@@ -119,18 +117,28 @@ producing global universe constraints, one can use the
 \begin{itemize}
 \item \texttt{Lemma}, \texttt{Axiom}, and all the other ``definition''
   keywords support polymorphism.
-\item \texttt{Variables}, \texttt{Context} in a section support polymorphism.
-  This means that the
-  variables are discharged polymorphically over definitions that use
-  them. In other words, two definitions in the section sharing a common
-  variable will both get parameterized by the universes produced by the 
-  variable declaration. This is in contrast to a ``mononorphic'' variable
-  which introduces global universes, making the two definitions depend on
-  the \emph{same} global universes associated to the variable.
+\item \texttt{Variables}, \texttt{Context}, \texttt{Universe} and
+  \texttt{Constraint} in a section support polymorphism.  This means
+  that the universe variables (and associated constraints) are
+  discharged polymorphically over definitions that use them. In other
+  words, two definitions in the section sharing a common variable will
+  both get parameterized by the universes produced by the variable
+  declaration. This is in contrast to a ``mononorphic'' variable which
+  introduces global universes and constraints, making the two
+  definitions depend on the \emph{same} global universes associated to
+  the variable.
 \item \texttt{Hint \{Resolve, Rewrite\}} will use the auto/rewrite hint
   polymorphically, not at a single instance.
 \end{itemize}
 
+\asection{Global and local universes}
+
+Each universe is declared in a global or local environment before it can
+be used. To ensure compatibility, every \emph{global} universe is set to
+be strictly greater than \Set~when it is introduced, while every
+\emph{local} (i.e. polymorphically quantified) universe is introduced as
+greater or equal to \Set.
+
 \asection{Conversion and unification}
 
 The semantics of conversion and unification have to be modified a little
@@ -151,6 +159,7 @@ unification can have different unfolding behaviors on the same
 development with universe polymorphism switched on or off.
 
 \asection{Minimization}
+\optindex{Universe Minimization ToSet}
 
 Universe polymorphism with cumulativity tends to generate many useless
 inclusion constraints in general. Typically at each application of a
@@ -173,23 +182,48 @@ This definition is elaborated by minimizing the universe of id to level
 generated at the application of id and a constraint that $\Set \le i$.
 This minimization process is applied only to fresh universe
 variables. It simply adds an equation between the variable and its lower
-bound if it is an atomic universe (i.e. not an algebraic max()).
+bound if it is an atomic universe (i.e. not an algebraic \texttt{max()}
+universe).
+
+The option \texttt{Unset Universe Minimization ToSet} disallows
+minimization to the sort $\Set$ and only collapses floating universes
+between themselves.
 
 \asection{Explicit Universes}
 
-\begin{flushleft}
-  \em The design and implementation of explicit universes is very
-  experimental and is likely to change in future versions.
-\end{flushleft}
+The syntax has been extended to allow users to explicitly bind names to
+universes and explicitly instantiate polymorphic definitions.
+
+\subsection{\tt Universe {\ident}.
+  \comindex{Universe}
+  \label{UniverseCmd}}
 
-The syntax has been extended to allow users to explicitely bind names to
-universes and explicitely instantantiate polymorphic
-definitions. Currently, binding is implicit at the first occurrence of a 
-universe name. For example, i and j below are introduced by the
-annotations attached to Types. 
+In the monorphic case, this command declares a new global universe named
+{\ident}. It supports the polymorphic flag only in sections, meaning the
+universe quantification will be discharged on each section definition
+independently.
+
+\subsection{\tt Constraint {\ident} {\textit{ord}} {\ident}.
+  \comindex{Constraint}
+  \label{ConstraintCmd}}
+
+This command declares a new constraint between named universes.
+The order relation can be one of $<$, $\le$ or $=$. If consistent, 
+the constraint is then enforced in the global environment. Like
+\texttt{Universe}, it can be used with the \texttt{Polymorphic} prefix
+in sections only to declare constraints discharged at section closing time.
+
+\begin{ErrMsgs}
+\item \errindex{Undeclared universe {\ident}}.
+\item \errindex{Universe inconsistency}
+\end{ErrMsgs}
+
+\subsection{Polymorphic definitions}
+For polymorphic definitions, the declaration of (all) universe levels
+introduced by a definition uses the following syntax:
 
 \begin{coq_example*}
-Polymorphic Definition le (A : Type@{i}) : Type@{j} := A.
+Polymorphic Definition le@{i j} (A : Type@{i}) : Type@{j} := A.
 \end{coq_example*}
 \begin{coq_example}
 Print le.
@@ -197,40 +231,32 @@ Print le.
 
 During refinement we find that $j$ must be larger or equal than $i$, as
 we are using $A : Type@{i} <= Type@{j}$, hence the generated
-constraint. Note that the names here are not bound in the final
-definition, they just allow to specify locally what relations should
-hold. In the term and in general in proof mode, universe names
-introduced in the types can be refered to in terms.
-
-Definitions can also be instantiated explicitely, giving their full instance:
+constraint. At the end of a definition or proof, we check that the only
+remaining universes are the ones declared. In the term and in general in
+proof mode, introduced universe names can be referred to in
+terms. Note that local universe names shadow global universe names.
+During a proof, one can use \texttt{Show Universes} to display
+the current context of universes.
+
+Definitions can also be instantiated explicitly, giving their full instance:
 \begin{coq_example}
 Check (pidentity@{Set}).
-Check (le@{i j}).
+Universes k l.
+Check (le@{k l}).
 \end{coq_example}
 
 User-named universes are considered rigid for unification and are never
-miminimized.
+minimized.
 
-Finally, two commands allow to name \emph{global} universes and constraints.
+\subsection{\tt Unset Strict Universe Declaration.
+  \optindex{Strict Universe Declaration}
+  \label{StrictUniverseDeclaration}}
 
-\subsection{\tt Universe {\ident}.
-  \comindex{Universe}
-  \label{UniverseCmd}}
-
-This command declare a new global universe named {\ident}.
-
-\subsection{\tt Constraint {\ident} {\textit{ord}} {\ident}.
-  \comindex{Constraint}
-  \label{ConstraintCmd}}
-
-This command declare a new constraint between named universes. 
-The order relation can be one of $<$, $<=$ or $=$. If consistent, 
-the constraint is then enforced in the global environment.
-
-\begin{ErrMsgs}
-\item \errindex{Undeclared universe {\ident}}.
-\item \errindex{Universe inconsistency}
-\end{ErrMsgs}
+The command \texttt{Unset Strict Universe Declaration} allows one to
+freely use identifiers for universes without declaring them first, with
+the semantics that the first use declares it. In this mode, the universe
+names are not associated with the definition or proof once it has been
+defined. This is meant mainly for debugging purposes.
 
 %%% Local Variables: 
 %%% mode: latex
diff --git a/doc/refman/biblio.bib b/doc/refman/biblio.bib
index d78ce4f2c6..70ee1f41f0 100644
--- a/doc/refman/biblio.bib
+++ b/doc/refman/biblio.bib
@@ -288,9 +288,14 @@ s},
 
 @InProceedings{Coquand93,
   author      = {Th. Coquand},
-  title       = {{Infinite Objects in Type Theory}},
+  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},
-  crossref    = {Nijmegen93}
+  pages       = {62-78}
 }
 
 @inproceedings{Corbineau08types,
@@ -323,6 +328,15 @@ s},
   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
@@ -540,6 +554,13 @@ s},
   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},
@@ -660,6 +681,13 @@ s},
   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},
@@ -1366,4 +1394,4 @@ Languages},
   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}
-}
\ No newline at end of file
+}
diff --git a/doc/refman/coqdoc.tex b/doc/refman/coqdoc.tex
index ee2b042f4e..26dbd59e76 100644
--- a/doc/refman/coqdoc.tex
+++ b/doc/refman/coqdoc.tex
@@ -285,7 +285,7 @@ suffix \verb!.tex!.
   
   Select a \texmacs\ output.
 
-\item[\texttt{--stdout}] ~\par
+\item[\texttt{\mm{}stdout}] ~\par
 
   Write output to stdout.
 
@@ -496,14 +496,25 @@ Default behavior is to assume ASCII 7 bits input files.
 \item[\texttt{-latin1}, \texttt{\mm{}latin1}] ~\par
 
   Select ISO-8859-1 input files. It is equivalent to
-  \texttt{--inputenc latin1 --charset iso-8859-1}.
+  \texttt{\mm{}inputenc latin1 \mm{}charset iso-8859-1}.
 
 \item[\texttt{-utf8}, \texttt{\mm{}utf8}] ~\par
 
-  Select UTF-8 (Unicode) input files. It is equivalent to
-  \texttt{--inputenc utf8 --charset utf-8}.
-  \LaTeX\ UTF-8 support can be found at
- \url{http://www.ctan.org/pkg/unicode}.
+  Set \texttt{\mm{}inputenc utf8x} for \LaTeX\ output and
+  \texttt{\mm{}charset utf-8} for HTML output. Also use Unicode
+  replacements for a couple of standard plain ASCII notations such
+  as $\rightarrow$ for \texttt{->} and $\forall$ for
+  \texttt{forall}. \LaTeX\ UTF-8 support can be found at
+  \url{http://www.ctan.org/pkg/unicode}.
+
+  For the interpretation of Unicode characters by \LaTeX, extra
+  packages which {\coqdoc} does not provide by default might be
+  required, such as \texttt{textgreek} for some Greek letters or
+  \texttt{stmaryrd} for some mathematical symbols. If a Unicode
+  character is missing an interpretation in the \texttt{utf8x} input
+  encoding, add
+  \verb=\DeclareUnicodeCharacter{=\textit{code}\verb=}{=\textit{latex-interpretation}\verb=}=. Packages
+  and declarations can be added with option \texttt{-p}.
 
 \item[\texttt{\mm{}inputenc} \textit{string}] ~\par
 
diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template
index 024e13413a..a12983ab84 100644
--- a/doc/stdlib/index-list.html.template
+++ b/doc/stdlib/index-list.html.template
@@ -59,6 +59,7 @@ through the <tt>Require Import</tt> command.</p>
     theories/Logic/WeakFan.v
     theories/Logic/WKL.v
     theories/Logic/FinFun.v
+    theories/Logic/PropFacts.v
   </dd>
 
   <dt> <b>Structures</b>:
@@ -476,13 +477,6 @@ through the <tt>Require Import</tt> command.</p>
     theories/MSets/MSetPositive.v
     theories/MSets/MSetToFiniteSet.v
     (theories/MSets/MSets.v)
-    theories/MMaps/MMapAVL.v
-    theories/MMaps/MMapFacts.v
-    theories/MMaps/MMapInterface.v
-    theories/MMaps/MMapList.v
-    theories/MMaps/MMapPositive.v
-    theories/MMaps/MMapWeakList.v
-    (theories/MMaps/MMaps.v)
   </dd>
 
   <dt> <b>FSets</b>:
@@ -591,7 +585,7 @@ through the <tt>Require Import</tt> command.</p>
   </dd>
 
   <dt> <b>Program</b>:
-    Support for dependently-typed programming.
+    Support for dependently-typed programming
   </dt>
   <dd>
     theories/Program/Basics.v
@@ -612,4 +606,13 @@ through the <tt>Require Import</tt> command.</p>
     theories/Unicode/Utf8_core.v
     theories/Unicode/Utf8.v
   </dd>
+
+  <dt> <b>Compat</b>:
+    Compatibility wrappers for previous versions of Coq
+  </dt>
+  <dd>
+    theories/Compat/AdmitAxiom.v
+    theories/Compat/Coq84.v
+    theories/Compat/Coq85.v
+  </dd>
 </dl>
diff --git a/doc/tools/Translator.tex b/doc/tools/Translator.tex
index 5f7b6dc951..ed1d336d9e 100644
--- a/doc/tools/Translator.tex
+++ b/doc/tools/Translator.tex
@@ -419,7 +419,7 @@ the hypotheses), or a comma-separated list of either hypothesis name,
 or {\tt (value of $H$)} or {\tt (type of $H$)}. Moreover, occurrences
 can be specified after every hypothesis after the {\TERM{at}}
 keyword. {\em concl} is either empty or \TERM{*}, and can be followed
-by occurences.
+by occurrences.
 
 \begin{transbox}
 \TRANS{in Goal}{in |- *}
diff --git a/doc/tutorial/Tutorial.tex b/doc/tutorial/Tutorial.tex
index 836944ab1c..e09feeb8eb 100644
--- a/doc/tutorial/Tutorial.tex
+++ b/doc/tutorial/Tutorial.tex
@@ -208,7 +208,7 @@ Definition two : nat := S one.
 
 Actually \Coq~ allows several possible syntaxes:
 \begin{coq_example}
-Definition three : nat := S two.
+Definition three := S two : nat.
 \end{coq_example}
 
 Here is a way to define the doubling function, which expects an