Indexing and documenting some options.

3 files changed, 18 insertions, 1 deletions

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-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