4 files changed, 75 insertions, 19 deletions
diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex
index 713f344cbe..7af4e9313a 100644
--- a/doc/refman/RefMan-ext.tex
+++ b/doc/refman/RefMan-ext.tex
@@ -279,15 +279,78 @@ of the chapter devoted to coercions.
 \label{prim-proj}
 
 The option {\tt Set Primitive Projections} turns on the use of primitive
-projections when defining subsequent records. Primitive projections
+projections when defining subsequent records (even through the {\tt
+  Inductive} and {\tt CoInductive} commands). Primitive projections
 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
 applications of the projection, considerably reducing the sizes of terms
 when manipulating parameterized records and typechecking time. On the
-user level, primitive projections are a transparent replacement
-for the usual defined ones.
+user level, primitive projections can be used as a replacement for the
+usual defined ones, although there are a few notable differences.
+
+The internally omitted parameters can be reconstructed at printing time
+even though they are absent in the actual AST manipulated by the kernel. This
+can be obtained by setting the {\tt Printing Primitive Projection Parameters}
+flag. Another compatibility printing can be activated thanks to the
+{\tt Printing Primitive Projection Compatibility} option which governs the
+printing of pattern-matching over primitive records.
+
+\subsubsection{Primitive Record Types}
+When the {\tt Set Primitive Projections} option is on, definitions of
+record types change meaning. When a type is declared with primitive
+projections, its {\tt match} construct is disabled (see
+\ref{primproj:compat} though). To eliminate the (co-)inductive type, one
+must use its defined primitive projections.
+
+There are currently two ways to introduce primitive records types:
+\begin{itemize}
+\item Through the {\tt Record} command, in which case the type has to be
+  non-recursive. The defined type enjoys eta-conversion definitionally,
+  that is the generalized form of surjective pairing for records:
+  {\tt $r$ = Build\_R ($r$.($p_1$) .. $r$.($p_n$))}. Eta-conversion allows to define
+  dependent elimination for these types as well.
+\item Through the {\tt Inductive} and {\tt CoInductive} commands, when
+  the body of the definition is a record declaration of the form {\tt
+    Build\_R \{ $p_1$ : $t_1$; .. ; $p_n$ : $t_n$ \}}. In this case the types can be
+  recursive and eta-conversion is disallowed. These kind of record types
+  differ from their traditional versions in the sense that dependent
+  elimination is not available for them and only non-dependent case analysis
+  can be defined.
+\end{itemize}
+
+\subsubsection{Reduction}
+
+The basic reduction rule of a primitive projection is {\tt $p_i$
+  (Build\_R $t_1$ .. $t_n$) $\rightarrow_{\iota}$ $t_i$}. However, to take the $\delta$ flag into
+account, projections can be in two states: folded or unfolded. An
+unfolded primitive projection application obeys the rule above, while
+the folded version delta-reduces to the unfolded version. This allows to
+precisely mimic the usual unfolding rules of constants. Projections
+obey the usual {\tt simpl} flags of the {\tt Arguments} command in particular.
+
+There is currently no way to input unfolded primitive projections at the
+user-level, and one must use the {\tt Printing Primitive Projection
+  Compatibility} to display unfolded primitive projections as matches
+and distinguish them from folded ones.
+
+\subsubsection{Compatibility Projections and {\tt match}}
+\label{primproj:compat}
+To ease compatibility with ordinary record types, each primitive
+projection is also defined as a ordinary constant taking parameters and
+an object of the record type as arguments, and whose body is an
+application of the unfolded primitive projection of the same name. These
+constants are used when elaborating partial applications of the
+projection. One can distinguish them from applications of the primitive
+projection if the {\tt Printing Primitive Projection Parameters} option
+is off: for a primitive projection application, parameters are printed
+as underscores while for the compatibility projections they are printed
+as usual.
+
+Additionally, user-written {\tt match} constructs on primitive records
+are desugared into substitution of the projections, they cannot be
+printed back as {\tt match} constructs.
 
   % - r.(p) and (p r) elaborate to native projection application, and
   %   the parameters cannot be mentioned. The following arguments are
@@ -305,13 +368,6 @@ 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.
 
-The internally omitted parameters can be reconstructed at printing time
-even though they are absent in the actual AST manipulated by the kernel. This
-can be obtained by setting the {\tt Printing Primitive Projection Parameters}
-flag. Another compatibility printing can be activated 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}
 \index{match@{\tt match\ldots with\ldots end}}}
@@ -1664,7 +1720,7 @@ to be given as if none arguments were implicit. By symmetry, this also
 affects printing. To restore parsing and normal printing of implicit
 arguments, use:
 \begin{quote}
-{\tt Set Parsing Explicit.}
+{\tt Unset Parsing Explicit.}
 \end{quote}
 
 \subsection{Canonical structures
diff --git a/doc/refman/RefMan-ssr.tex b/doc/refman/RefMan-ssr.tex
index 61f7421c44..db794e5a63 100644
--- a/doc/refman/RefMan-ssr.tex
+++ b/doc/refman/RefMan-ssr.tex
@@ -42,7 +42,7 @@ Proofs written in \ssr{} typically look quite different from the
 ones written using only tactics as per Chapter~\ref{Tactics}.
 We try to summarise here the most ``visible'' ones in order to
 help the reader already accustomed to the tactics described in
-Chapter~\ref{Tactics}to read this chapter.
+Chapter~\ref{Tactics} to read this chapter.
 
 The first difference between the tactics described in this
 chapter and the tactics described in Chapter~\ref{Tactics} is the way
@@ -79,19 +79,19 @@ expansion and partial evaluation participate all to a same concept of
 rewriting a goal in a larger sense. As such, all these functionalities are
 provided by the \ssrC{rewrite} tactic.
 
-\ssrC{} includes a little language of patterns to select subterms in tactics
+\ssr{} includes a little language of patterns to select subterms in tactics
 or tacticals where it matters.  Its most notable application
 is in the \ssrC{rewrite} tactic, where patterns are used to specify
 where the rewriting step has to take place.
 
-Finally, \ssr{} supports the so-called reflection steps, typically
+Finally, \ssr{} supports so-called reflection steps, typically
 allowing to switch back and forth between the computational view and
 logical view of a concept.
 
 To conclude it is worth mentioning that \ssr{} tactics
 can be mixed with non \ssr{} tactics in the same proof,
-or in the same LTac expression.  The few exceptions
-to this statement are described in section~\label{sec:compat}.
+or in the same Ltac expression.  The few exceptions
+to this statement are described in section~\ref{sec:compat}.
 
 \iffalse
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -130,7 +130,7 @@ ProofGeneral provided in the distribution:
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \subsection*{Acknowledgments}
-The authors would like to thank Fr\'ed\'eric Blanqui, Fran\,cois Pottier
+The authors would like to thank Frédéric Blanqui, François Pottier
 and Laurence Rideau for their comments and suggestions.
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 6e27357008..8fbcfdf308 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -3309,7 +3309,7 @@ evaluating purely computational expressions (i.e. with little dead code).
   fine-tuned. It is specially interesting for full evaluation of algebraic
   objects. This includes the case of reflection-based tactics.
 
-\item {\tt native\_compute} \tacindex{native\_compute}
+\item {\tt native\_compute} \tacindex{native\_compute} \optindex{NativeCompute Profiling}
 
   This tactic evaluates the goal by compilation to \ocaml{} as described in
   \cite{FullReduction}. If \Coq{} is running in native code, it can be typically
diff --git a/doc/refman/Setoid.tex b/doc/refman/Setoid.tex
index 6c79284389..0c8cd408f2 100644
--- a/doc/refman/Setoid.tex
+++ b/doc/refman/Setoid.tex
@@ -223,7 +223,7 @@ the following command.
 
 \comindex{Add Parametric Morphism}
 \begin{quote}
-  \texttt{Add Parametric Morphism} ($x_1 : \T_!$) \ldots ($x_k : \T_k$)\\
+  \texttt{Add Parametric Morphism} ($x_1 : \T_1$) \ldots ($x_k : \T_k$) :
   (\textit{f $t_1$ \ldots $t_n$})\\
   \texttt{~with signature} \textit{sig}\\
   \texttt{~as id}.\\