Merge branch 'v8.5'

7 files changed, 47 insertions, 10 deletions

diff --git a/doc/refman/Extraction.tex b/doc/refman/Extraction.tex
index 74c8374de..a963662f6 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/RefMan-cic.tex b/doc/refman/RefMan-cic.tex
index e3e49e115..1554ee04d 100644
--- a/doc/refman/RefMan-cic.tex
+++ b/doc/refman/RefMan-cic.tex
@@ -24,7 +24,7 @@ written {\it ``x:T''}. Informally, {\it ``x:T''} can be thought as
 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~\label{cic:terms} but, first, we describe sorts.
+Section~\ref{cic:terms} but, first, we describe sorts.
 
 \subsection[Sorts]{Sorts\label{Sorts}
 \index{Sorts}}
diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex
index a718a26ea..f2ab79dce 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}
@@ -284,6 +285,9 @@ 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}
 
@@ -314,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}
diff --git a/doc/refman/RefMan-gal.tex b/doc/refman/RefMan-gal.tex
index 0e758bcab..fcccd9cb4 100644
--- a/doc/refman/RefMan-gal.tex
+++ b/doc/refman/RefMan-gal.tex
@@ -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}
diff --git a/doc/refman/RefMan-sch.tex b/doc/refman/RefMan-sch.tex
index 571e16d57..53aa6b86a 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/Universes.tex b/doc/refman/Universes.tex
index ea3cca77e..a08cd1475 100644
--- a/doc/refman/Universes.tex
+++ b/doc/refman/Universes.tex
@@ -159,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
@@ -248,7 +249,7 @@ User-named universes are considered rigid for unification and are never
 minimized.
 
 \subsection{\tt Unset Strict Universe Declaration.
-  \optindex{StrictUniverseDeclaration}
+  \optindex{Strict Universe Declaration}
   \label{StrictUniverseDeclaration}}
 
 The command \texttt{Unset Strict Universe Declaration} allows one to
diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template
index 33de399c0..a8bbdeb37 100644
--- a/doc/stdlib/index-list.html.template
+++ b/doc/stdlib/index-list.html.template
@@ -618,6 +618,7 @@ through the <tt>Require Import</tt> command.</p>
     Compatibility wrappers for previous versions of Coq
   </dt>
   <dd>
+    theories/Compat/AdmitAxiom.v
     theories/Compat/Coq84.v
     theories/Compat/Coq85.v
   </dd>