8 files changed, 125 insertions, 32 deletions
diff --git a/doc/refman/Extraction.tex b/doc/refman/Extraction.tex
index 01dbcfb1c..fa3d61b1c 100644
--- a/doc/refman/Extraction.tex
+++ b/doc/refman/Extraction.tex
@@ -19,6 +19,12 @@ be used (abusively) to refer to any of the three.
 %% the one in previous versions of \Coq: there is no more
 %% an explicit toplevel for the language (formerly called \textsc{Fml}). 
 
+Before using any of the commands or options described in this chapter,
+the extraction framework should first be loaded explicitly
+via {\tt Require Extraction}. Note that in earlier versions of Coq, these
+commands and options were directly available without any preliminary
+{\tt Require}.
+
 \asection{Generating ML code}
 \comindex{Extraction}
 \comindex{Recursive Extraction}
@@ -501,6 +507,7 @@ We can now extract this program to \ocaml:
 Reset Initial.
 \end{coq_eval}
 \begin{coq_example}
+Require Extraction.
 Require Import Euclid Wf_nat.
 Extraction Inline gt_wf_rec lt_wf_rec induction_ltof2.
 Recursive Extraction eucl_dev.
diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex
index fdd272581..96fb1eb75 100644
--- a/doc/refman/RefMan-cic.tex
+++ b/doc/refman/RefMan-cic.tex
@@ -461,6 +461,13 @@ recursively convertible to $u'_1$, or, symmetrically, $u_2$ is $\lb
 x:T\mto u'_2$ and $u_1\,x$ is recursively convertible to $u'_2$.  We
 then write $\WTEGCONV{t_1}{t_2}$.
 
+Apart from this we consider two instances of polymorphic and cumulative (see Chapter~\ref{Universes-full}) inductive types (see below)
+convertible $\WTEGCONV{t\ w_1 \dots w_m}{t\ w_1' \dots w_m'}$ if we have subtypings (see below) in both directions, i.e.,
+$\WTEGLECONV{t\ w_1 \dots w_m}{t\ w_1' \dots w_m'}$ and $\WTEGLECONV{t\ w_1' \dots w_m'}{t\ w_1 \dots w_m}$.
+Furthermore, we consider $\WTEGCONV{c\ v_1 \dots v_m}{c'\ v_1' \dots v_m'}$ convertible if $\WTEGCONV{v_i}{v_i'}$
+and we have that $c$ and $c'$ are the same constructors of different instances the same inductive types (differing only in universe levels)
+such that $\WTEG{c\ v_1 \dots v_m}{t\ w_1 \dots w_m}$ and $\WTEG{c'\ v_1' \dots v_m'}{t'\ w_1' \dots w_m'}$ and we have $\WTEGCONV{t\ w_1 \dots w_m}{t\ w_1' \dots w_m'}$.
+
 The convertibility relation allows introducing a new typing rule
 which says that two convertible well-formed types have the same
 inhabitants.
@@ -480,6 +487,17 @@ convertibility into a {\em subtyping} relation inductively defined by:
 \item $\WTEGLECONV{\Prop}{\Set}$, hence, by transitivity,
   $\WTEGLECONV{\Prop}{\Type(i)}$, for any $i$
 \item if $\WTEGCONV{T}{U}$ and $\WTELECONV{\Gamma::(x:T)}{T'}{U'}$ then $\WTEGLECONV{\forall~x:T, T'}{\forall~x:U, U'}$.
+\item if $\Ind{}{p}{\Gamma_I}{\Gamma_C}$ is a universe polymorphic and cumulative (see Chapter~\ref{Universes-full})
+  inductive type (see below) and $(t : \forall\Gamma_P,\forall\Gamma_{\mathit{Arr}(t)}, \Sort)\in\Gamma_I$
+  and $(t' : \forall\Gamma_P',\forall\Gamma_{\mathit{Arr}(t)}', \Sort')\in\Gamma_I$
+  are two different instances of \emph{the same} inductive type (differing only in universe levels) with constructors
+  \[[c_1: \forall\Gamma_P,\forall T_{1,1} \dots T_{1,n_1},t\ v_{1,1} \dots v_{1,m}; \dots; c_k: \forall\Gamma_P,\forall T_{k, 1} \dots T_{k,n_k},t\ v_{n,1}\dots v_{n,m}]\]
+  and
+  \[[c_1: \forall\Gamma_P',\forall T_{1,1}' \dots T_{1,n_1}',t'\ v_{1,1}' \dots v_{1,m}'; \dots; c_k: \forall\Gamma_P',\forall T_{k, 1}' \dots T_{k,n_k}',t\ v_{n,1}'\dots v_{n,m}']\]
+  respectively then $\WTEGLECONV{t\ w_1 \dots w_m}{t\ w_1' \dots w_m'}$ (notice that $t$ and $t'$ are both fully applied, i.e., they have a sort as a type)
+  if $\WTEGCONV{w_i}{w_i'}$ for $1 \le i \le m$ and we have
+  \[ \WTEGLECONV{T_{i,j}}{T_{i,j}'} \text{ and } \WTEGLECONV{A_i}{A_i'}\]
+  where $\Gamma_{\mathit{Arr}(t)} = [a_1 : A_1; a_1 : A_l]$ and $\Gamma_{\mathit{Arr}(t)} = [a_1 : A_1'; a_1 : A_l']$.
 \end{enumerate}
 
 The conversion rule up to subtyping is now exactly:
@@ -530,8 +548,12 @@ Formally, we can represent any {\em inductive definition\index{definition!induct
 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:
+such that each $T$ in $(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}}.
+Furthermore, we must have that each $T$ in $(t:T)\in\Gamma_I$ can be written as:
+$\forall\Gamma_P,\forall\Gamma_{\mathit{Arr}(t)}, \Sort$ where $\Gamma_{\mathit{Arr}(t)}$ is called the
+{\em Arity} of the inductive type\index{arity of inductive type} $t$ and
+$\Sort$ is called the sort of the inductive type $t$.
 
 \paragraph{Examples}
 
diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex
index 6dd0ddf81..939fc87a6 100644
--- a/doc/refman/RefMan-ext.tex
+++ b/doc/refman/RefMan-ext.tex
@@ -721,18 +721,20 @@ a given type. See Section~\ref{Show}.
 
 \section{Advanced recursive functions}
 
-The \emph{experimental} command 
+The following \emph{experimental} command is available
+when the {\tt FunInd} library has been loaded via {\tt Require Import FunInd}:
 \begin{center}
    \texttt{Function {\ident} {\binder$_1$}\ldots{\binder$_n$}
      \{decrease\_annot\} : type$_0$ := \term$_0$}
    \comindex{Function}
    \label{Function}
 \end{center}
-can be seen as a generalization of {\tt Fixpoint}.  It is actually a
-wrapper for several ways of defining a function \emph{and other useful
+This command can be seen as a generalization of {\tt Fixpoint}.  It is actually
+a wrapper for several ways of defining a function \emph{and other useful
   related objects}, namely: an induction principle that reflects the
 recursive structure of the function (see \ref{FunInduction}), and its
-fixpoint equality.  The meaning of this
+fixpoint equality.
+ The meaning of this
 declaration is to define a function {\it ident}, similarly to {\tt
   Fixpoint}. Like in {\tt Fixpoint}, the decreasing argument must be
 given (unless the function is not recursive), but it must not
diff --git a/doc/refman/RefMan-pro.tex b/doc/refman/RefMan-pro.tex
index 0760d716e..b66659dc8 100644
--- a/doc/refman/RefMan-pro.tex
+++ b/doc/refman/RefMan-pro.tex
@@ -427,22 +427,6 @@ This command displays the current goals.
   This tactics script may contain some holes (subgoals not yet proved).
   They are printed under the form \verb!<Your Tactic Text here>!.
 
-%% \item {\tt Show Tree.}\comindex{Show Tree}\\
-%% This command can be seen as a more structured way of
-%% displaying the state of the proof than that 
-%% provided by {\tt Show Script}. Instead of just giving
-%% the list of tactics that have been applied, it 
-%% shows the derivation tree constructed by then. 
-%% Each node of the tree contains the conclusion
-%% of the corresponding sub-derivation (i.e. a
-%% goal with its corresponding local context) and 
-%% the tactic that has generated all the 
-%% sub-derivations. The leaves of this tree are
-%% the goals which still remain to be proved.
-
-%\item {\tt Show Node}\comindex{Show Node}\\
-%        Not yet documented
-
 \item {\tt Show Proof.}\comindex{Show Proof}\\
 It displays the proof term generated by the 
 tactics that have been applied. 
diff --git a/doc/refman/RefMan-sch.tex b/doc/refman/RefMan-sch.tex
index 53aa6b86a..d3719bed4 100644
--- a/doc/refman/RefMan-sch.tex
+++ b/doc/refman/RefMan-sch.tex
@@ -196,8 +196,10 @@ Check tree_forest_mutind.
 
 The {\tt Functional Scheme} command is a high-level experimental
 tool for generating automatically induction principles
-corresponding to (possibly mutually recursive) functions.  Its
-syntax follows the schema:
+corresponding to (possibly mutually recursive) functions.
+First, it must be made available via {\tt Require Import FunInd}.
+ Its
+syntax then follows the schema:
 \begin{quote}
 {\tt Functional Scheme {\ident$_1$} := Induction for \ident'$_1$ Sort {\sort$_1$} \\
   with\\
@@ -319,6 +321,7 @@ of a tree or a forest. Note that we use \texttt{Function} which
 generally produces better principles.
 
 \begin{coq_example*}
+Require Import FunInd.
 Function tree_size (t:tree) : nat :=
   match t with
   | node A f => S (forest_size f)
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 253eb7f01..be75dc9d5 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -1053,21 +1053,31 @@ dependencies. This tactic is the inverse of {\tt intro}.
 \label{move}
 
 This moves the hypothesis named {\ident$_1$} in the local context
-after the hypothesis named {\ident$_2$}. The proof term is not changed.
+after the hypothesis named {\ident$_2$}, where ``after'' is in
+reference to the direction of the move. The proof term is not changed.
 
-If {\ident$_1$} comes before {\ident$_2$} in the order of dependencies,
-then all the hypotheses between {\ident$_1$} and {\ident$_2$} that
-(possibly indirectly) depend on {\ident$_1$} are moved too.
+If {\ident$_1$} comes before {\ident$_2$} in the order of
+dependencies, then all the hypotheses between {\ident$_1$} and
+{\ident$_2$} that (possibly indirectly) depend on {\ident$_1$} are
+moved too, and all of them are thus moved after {\ident$_2$} in the
+order of dependencies.
 
 If {\ident$_1$} comes after {\ident$_2$} in the order of dependencies,
 then all the hypotheses between {\ident$_1$} and {\ident$_2$} that
-(possibly indirectly) occur in {\ident$_1$} are moved too.
+(possibly indirectly) occur in the type of {\ident$_1$} are moved
+too, and all of them are thus moved before {\ident$_2$} in the order
+of dependencies.
 
 \begin{Variants}
 
 \item {\tt move {\ident$_1$} before {\ident$_2$}}
 
-This moves {\ident$_1$} towards and just before the hypothesis named {\ident$_2$}.
+This moves {\ident$_1$} towards and just before the hypothesis named
+{\ident$_2$}. As for {\tt move {\ident$_1$} after {\ident$_2$}},
+dependencies over {\ident$_1$} (when {\ident$_1$} comes before
+{\ident$_2$} in the order of dependencies) or in the type of
+{\ident$_1$} (when {\ident$_1$} comes after {\ident$_2$} in the order
+of dependencies) are moved too.
 
 \item {\tt move {\ident} at top}
 
@@ -1084,13 +1094,30 @@ This moves {\ident} at the bottom of the local context (at the end of the contex
 \item \errindex{No such hypothesis}
 
 \item \errindex{Cannot move {\ident$_1$} after {\ident$_2$}:
-                   it occurs in {\ident$_2$}}
+                   it occurs in the type of {\ident$_2$}}
 
 \item \errindex{Cannot move {\ident$_1$} after {\ident$_2$}:
                    it depends on {\ident$_2$}}
 
 \end{ErrMsgs}
 
+\Example
+
+\begin{coq_example}
+Goal forall x :nat, x = 0 -> forall z y:nat, y=y-> 0=x.
+intros x H z y H0.
+move x after H0.
+Undo.
+move x before H0.
+Undo.
+move H0 after H.
+Undo.
+move H0 before H.
+\end{coq_example}
+\begin{coq_eval}
+Abort.
+\end{coq_eval}
+
 \subsection{\tt rename {\ident$_1$} into {\ident$_2$}}
 \tacindex{rename}
 
@@ -2113,13 +2140,15 @@ The tactic \texttt{functional induction} performs
 case analysis and induction following the definition of a function. It
 makes use of a principle generated by \texttt{Function}
 (see Section~\ref{Function}) or \texttt{Functional Scheme}
-(see Section~\ref{FunScheme}).
+(see Section~\ref{FunScheme}). Note that this tactic is only available
+after a {\tt Require Import FunInd}.
 
 \begin{coq_eval}
 Reset Initial.
 Import Nat.
 \end{coq_eval}
 \begin{coq_example}
+Require Import FunInd.
 Functional Scheme minus_ind := Induction for minus Sort Prop.
 Check minus_ind.
 Lemma le_minus (n m:nat) : n - m <= n.
@@ -4797,6 +4826,7 @@ that performs inversion on hypothesis {\ident} of the form
 \texttt{\qualid\ \term$_1$\dots\term$_n$\ = \term} or \texttt{\term\ =
   \qualid\ \term$_1$\dots\term$_n$} where \qualid\ must have been
 defined using \texttt{Function} (see Section~\ref{Function}).
+Note that this tactic is only available after a {\tt Require Import FunInd}.
 
 \begin{ErrMsgs}
 \item \errindex{Hypothesis {\ident} must contain at least one Function}
diff --git a/doc/refman/Universes.tex b/doc/refman/Universes.tex
index 36518e6fa..2bb1301c7 100644
--- a/doc/refman/Universes.tex
+++ b/doc/refman/Universes.tex
@@ -131,6 +131,52 @@ producing global universe constraints, one can use the
   polymorphically, not at a single instance.
 \end{itemize}
 
+\asection{{\tt Cumulative, NonCumulative}}
+\comindex{Cumulative}
+\comindex{NonCumulative}
+\optindex{Inductive Cumulativity}
+
+Inductive types, coinductive types, variants and records can be
+declared cumulative using the \texttt{Cumulative}. Alternatively,
+there is an option \texttt{Set Inductive Cumulativity} which when set,
+makes all subsequent inductive definitions cumulative. Consider the examples below.
+\begin{coq_example*}
+Polymorphic Cumulative Inductive list {A : Type} :=
+| nil : list
+| cons : A -> list -> list.
+\end{coq_example*}
+\begin{coq_example}
+Print list.
+\end{coq_example}
+When printing \texttt{list}, the part of the output of the form
+\texttt{$\mathtt{\sim}$@\{i\} <= $\mathtt{\sim}$@\{j\} iff }
+indicates the universe constraints in order to have the subtyping
+$\WTEGLECONV{\mathtt{list@\{i\}} A}{\mathtt{list@\{j\}} B}$
+(for fully applied instances of \texttt{list}) whenever $\WTEGCONV{A}{B}$.
+In the case of \texttt{list} there is no constraint!
+This also means that any two instances of \texttt{list} are convertible:
+$\WTEGCONV{\mathtt{list@\{i\}} A}{\mathtt{list@\{j\}} B}$ whenever $\WTEGCONV{A}{B}$ and
+furthermore their corresponding (when fully applied to convertible arguments) constructors.
+See Chapter~\ref{Cic} for more details on convertibility and subtyping.
+Also notice the subtyping constraints for the \emph{non-cumulative} version of list:
+\begin{coq_example*}
+Polymorphic NonCumulative Inductive list' {A : Type} :=
+| nil' : list'
+| cons' : A -> list' -> list'.
+\end{coq_example*}
+\begin{coq_example}
+Print list'.
+\end{coq_example}
+The following is an example of a record with non-trivial subtyping relation:
+\begin{coq_example*}
+Polymorphic Cumulative Record packType := {pk : Type}.
+\end{coq_example*}
+\begin{coq_example}
+Print packType.
+\end{coq_example}
+Notice that as expected, \texttt{packType@\{i\}} and \texttt{packType@\{j\}} are convertible if and only if \texttt{i $=$ j}.
+
+
 \asection{Global and local universes}
 
 Each universe is declared in a global or local environment before it can
diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template
index 1b847414f..48f82f2d9 100644
--- a/doc/stdlib/index-list.html.template
+++ b/doc/stdlib/index-list.html.template
@@ -589,7 +589,6 @@ through the <tt>Require Import</tt> command.</p>
   </dt>
   <dd>
     theories/Compat/AdmitAxiom.v
-    theories/Compat/Coq84.v
     theories/Compat/Coq85.v
     theories/Compat/Coq86.v
   </dd>