Merge PR #6982: Sphinx doc chapter 2

6 files changed, 2360 insertions, 2583 deletions

diff --git a/Makefile.doc b/Makefile.doc
index e6ab89efc..0f424af09 100644
--- a/Makefile.doc
+++ b/Makefile.doc
@@ -57,8 +57,8 @@ ALLSPHINXOPTS= -d $(SPHINXBUILDDIR)/doctrees $(SPHINXOPTS)
 DOCCOMMON:=doc/common/version.tex doc/common/title.tex doc/common/macros.tex
 
 REFMANCOQTEXFILES:=$(addprefix doc/refman/, \
-  RefMan-gal.v.tex RefMan-ext.v.tex \
-  RefMan-mod.v.tex RefMan-tac.v.tex \
+  RefMan-gal.v.tex \
+  RefMan-tac.v.tex \
   RefMan-cic.v.tex RefMan-lib.v.tex \
   RefMan-tacex.v.tex RefMan-syn.v.tex \
   RefMan-oth.v.tex RefMan-ltac.v.tex \
diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex
deleted file mode 100644
index a1950d136..000000000
--- a/doc/refman/RefMan-ext.tex
+++ /dev/null
@@ -1,2152 +0,0 @@
-\chapter[Extensions of \Gallina{}]{Extensions of \Gallina{}\label{Gallina-extension}\index{Gallina}}
-%HEVEA\cutname{gallina-ext.html}
-
-{\gallina} is the kernel language of {\Coq}. We describe here extensions of
-the Gallina's syntax.
-
-\section{Record types
-\comindex{Record}
-\comindex{Inductive}
-\comindex{CoInductive}
-\label{Record}}
-
-The \verb+Record+ construction is a macro allowing the definition of
-records as is done in many programming languages.  Its syntax is
-described on Figure~\ref{record-syntax}.  In fact, the \verb+Record+
-macro is more general than the usual record types, since it allows
-also for ``manifest'' expressions. In this sense, the \verb+Record+
-construction allows defining ``signatures''.
-
-\begin{figure}[h]
-\begin{centerframe}
-\begin{tabular}{lcl}
-{\sentence} & ++= & {\record}\\
-  & & \\
-{\record} & ::= &
-   {\recordkw} {\ident} \zeroone{\binders} \zeroone{{\tt :} {\sort}} \verb.:=. \\
-&& ~~~~\zeroone{\ident}
-       \verb!{! \zeroone{\nelist{\field}{;}} \verb!}! \verb:.:\\
-  & & \\
-{\recordkw} & ::= &
-   {\tt Record} $|$ {\tt Inductive} $|$ {\tt CoInductive}\\
-  & & \\
-{\field} & ::= & {\name} \zeroone{\binders} : {\type} \zeroone{{\tt where} {\it notation}} \\
- & $|$ & {\name} \zeroone{\binders} {\typecstrtype} := {\term}\\
-\end{tabular}
-\end{centerframe}
-\caption{Syntax for the definition of {\tt Record}}
-\label{record-syntax}
-\end{figure}
-
-\noindent In the expression
-\begin{quote}
-{\tt Record {\ident} {\params} : {\sort} := {\ident$_0$} \{ \\
-  {\ident$_1$} \binders$_1$ : {\term$_1$} ; ... ; \\
-  {\ident$_n$} \binders$_n$ : {\term$_n$} \}.}
-\end{quote}
-\noindent the identifier {\ident} is the name of the defined record
-and {\sort} is its type. The identifier {\ident$_0$} is the name of
-its constructor. If {\ident$_0$} is omitted, the default name {\tt
-Build\_{\ident}} is used.
-If {\sort} is omitted, the default sort is {\Type}.
-The identifiers {\ident$_1$}, \dots, {\ident$_n$} are the names of
-fields and {\tt forall {\binders$_1$}, {\term$_1$}}, \dots,
-{\tt forall {\binders$_n$}, {\term$_n$}}
-their respective types. Remark that the type of {\ident$_i$} may
-depend on the previous {\ident$_j$} (for $j<i$). Thus the order of the
-fields is important. Finally, {\params} are the parameters of the
-record.
-
-More generally, a record may have explicitly defined (a.k.a.
-manifest) fields. For instance, {\tt Record} {\ident} {\tt [}
-{\params} {\tt ]} \texttt{:} {\sort} := \verb+{+ {\ident$_1$}
-\texttt{:} {\type$_1$} \verb+;+ {\ident$_2$} \texttt{:=} {\term$_2$}
-\verb+;+ {\ident$_3$} \texttt{:} {\type$_3$} \verb+}+ in which case
-the correctness of {\type$_3$} may rely on the instance {\term$_2$} of
-{\ident$_2$} and {\term$_2$} in turn may depend on {\ident$_1$}.
-
-
-\Example
-The set of rational numbers may be defined as:
-\begin{coq_eval}
-Reset Initial.
-\end{coq_eval}
-\begin{coq_example}
-Record Rat : Set := mkRat
-  {sign : bool;
-   top : nat;
-   bottom : nat;
-   Rat_bottom_cond : 0 <> bottom;
-   Rat_irred_cond :
-    forall x y z:nat, (x * y) = top /\ (x * z) = bottom -> x = 1}.
-\end{coq_example}
-
-Remark here that the field \verb+Rat_bottom_cond+ depends
-on the field \verb+bottom+ and \verb+Rat_irred_cond+ depends
-on both \verb+top+ and \verb+bottom+.
-
-Let us now see the work done by the {\tt Record} macro.  First the
-macro generates a variant type definition with just one constructor:
-\begin{quote}
-{\tt Variant {\ident} {\params} : {\sort} := \\
-  {\ident$_0$} ({\ident$_1$} : {\term$_1$}) ... ({\ident$_n$} : {\term$_n$}).}
-\end{quote}
-To build an object of type {\ident}, one should provide the
-constructor {\ident$_0$} with $n$ terms filling the fields of
-the record.
-
-As an example, let us define the rational $1/2$:
-\begin{coq_example*}
-Theorem one_two_irred :
- forall x y z:nat, x * y = 1 /\ x * z = 2 -> x = 1.
-Admitted.
-\end{coq_example*}
-\begin{coq_example}
-Definition half := mkRat true 1 2 (O_S 1) one_two_irred.
-\end{coq_example}
-\begin{coq_example}
-Check half.
-\end{coq_example}
-
-\begin{figure}[t]
-\begin{centerframe}
-\begin{tabular}{lcl}
-{\term} & ++= &
-         \verb!{|! \zeroone{\nelist{\fielddef}{;}} \verb!|}! \\
-  & & \\
-{\fielddef} & ::= & {\name} \zeroone{\binders} := {\term} \\
-\end{tabular}
-\end{centerframe}
-\caption{Syntax for constructing elements of a \texttt{Record} using named fields}
-\label{fig:fieldsyntax}
-\end{figure}
-
-Alternatively, the following syntax allows creating objects by using named fields, as
-shown on Figure~\ref{fig:fieldsyntax}. The
-fields do not have to be in any particular order, nor do they have to be all
-present if the missing ones can be inferred or prompted for (see
-Section~\ref{Program}).
-
-\begin{coq_example}
-Definition half' :=
-  {| sign := true;
-     Rat_bottom_cond := O_S 1;
-     Rat_irred_cond := one_two_irred |}.
-\end{coq_example}
-
-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}
-{\tt Add Printing Record {\ident}.}
-\end{quote}
-to get record syntax or
-\begin{quote}
-{\tt Add Printing Constructor {\ident}.}
-\end{quote}
-to get constructor syntax.
-
-This syntax can also be used for pattern matching.
-
-\begin{coq_example}
-Eval compute in (
-  match half with
-  | {| sign := true; top := n |} => n
-  | _ => 0
-  end).
-\end{coq_example}
-
-The macro generates also, when it is possible, the projection
-functions for destructuring an object of type {\ident}.  These
-projection functions are given the names of the corresponding
-fields. If a field is named ``\verb=_='' then no projection is built
-for it. In our example:
-
-\begin{coq_example}
-Eval compute in top half.
-Eval compute in bottom half.
-Eval compute in Rat_bottom_cond half.
-\end{coq_example}
-
-An alternative syntax for projections based on a dot notation is
-available:
-
-\begin{coq_example}
-Eval compute in half.(top).
-\end{coq_example}
-
-It can be activated for printing with the command
-\optindex{Printing Projections}
-\begin{quote}
-{\tt Set Printing Projections.}
-\end{quote}
-
-\begin{coq_example}
-Set Printing Projections.
-Check top half.
-\end{coq_example}
-
-The corresponding grammar rules are given in Figure~\ref{fig:projsyntax}.
-When {\qualid} denotes a projection, the syntax {\tt
-  {\term}.({\qualid})} is equivalent to {\qualid~\term}, the syntax
-{\term}{\tt .(}{\qualid}~{\termarg}$_1$ {\ldots} {\termarg}$_n${\tt )} to
-{\qualid~{\termarg}$_1$ {\ldots} {\termarg}$_n$~\term}, and the syntax
-{\term}{\tt .(@}{\qualid}~{\term}$_1$~\ldots~{\term}$_n${\tt )} to
-{@\qualid~{\term}$_1$ {\ldots} {\term}$_n$~\term}. In each case, {\term}
-is the object projected and the other arguments are the parameters of
-the inductive type.
-
-\begin{figure}[t]
-\begin{centerframe}
-\begin{tabular}{lcl}
-{\term} & ++= & {\term} {\tt .(} {\qualid} {\tt )}\\
- & $|$ & {\term} {\tt .(} {\qualid} \nelist{\termarg}{} {\tt )}\\
- & $|$ & {\term} {\tt .(} {@}{\qualid} \nelist{\term}{} {\tt )}
-\end{tabular}
-\end{centerframe}
-\caption{Syntax for \texttt{Record} projections}
-\label{fig:projsyntax}
-\end{figure}
-
-\begin{coq_eval}
-Reset Initial.
-\end{coq_eval}
-
-\begin{Remarks}
-
-\item Records defined with the {\tt Record} keyword are not allowed to be
-recursive (references to the record's name in the type of its field
-raises an  error). To define recursive records, one can use the {\tt
-Inductive} and {\tt CoInductive} keywords, resulting in an inductive
-or co-inductive record.
-A \emph{caveat}, however, is that records
-cannot appear in mutually inductive (or co-inductive) definitions.
-
-\item Induction schemes are automatically generated for inductive records.
-Automatic generation of induction schemes for non-recursive records
-defined with the {\tt Record} keyword can be activated with the
-{\tt Nonrecursive Elimination Schemes} option
-(see~\ref{set-nonrecursive-elimination-schemes}).
-
-\item {\tt Structure} is a synonym of the keyword {\tt Record}.
-
-\end{Remarks}
-
-\begin{Warnings}
-\item {\tt {\ident$_i$} cannot be defined.}
-
-  It can happen that the definition of a projection is impossible.
-  This message is followed by an explanation of this impossibility.
-  There may be three reasons:
-   \begin{enumerate}
-   \item The name {\ident$_i$} already exists in the environment (see
-     Section~\ref{Axiom}).
-   \item The body of {\ident$_i$} uses an incorrect elimination for
-     {\ident} (see Sections~\ref{Fixpoint} and~\ref{Caseexpr}).
-   \item The type of the projections {\ident$_i$} depends on previous
-   projections which themselves could not be defined.
-   \end{enumerate}  
-\end{Warnings}     
-
-\begin{ErrMsgs}
-
-\item \errindex{Records declared with the keyword Record or Structure cannot be recursive.}
-
-  The record name {\ident} appears in the type of its fields, but uses
-  the keyword  {\tt Record}. Use  the keyword {\tt Inductive}  or {\tt
-    CoInductive} instead.
-\item \errindex{Cannot handle mutually (co)inductive records.}
-
-  Records  cannot  be  defined  as  part  of  mutually  inductive  (or
-  co-inductive) definitions,  whether with records only  or mixed with
-  standard definitions.
-\item During the definition of the one-constructor inductive
-  definition, all the errors of inductive definitions, as described in
-  Section~\ref{gal-Inductive-Definitions}, may also occur.
-
-\end{ErrMsgs}
-
-\SeeAlso Coercions and records in Section~\ref{Coercions-and-records}
-of the chapter devoted to coercions.
-
-\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 (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 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
-  %   parsed according to the remaining implicit arguments declared for the
-  %   projection (i.e. the implicit arguments after the record type
-  %   argument). In dot notation, the record type argument is considered
-  %   explicit no matter what its implicit status is.
-  % - r.(@p params) and @p args are parsed as regular applications of the
-  %   projection with explicit parameters.
-  % - [simpl p] is forbidden, but [simpl @p] will simplify both the projection
-  %   and its explicit [@p] version.
-  % - [unfold p] has no effect on projection applications unless it is applied
-  %   to a constructor. If the explicit version appears it reduces to the
-  %   projection application.
-  % - [pattern x at n], [rewrite x at n] and in general abstraction and selection
-  %   of occurrences may fail due to the disappearance of parameters.
-
-\section{Variants and extensions of {\mbox{\tt match}}
-\label{Extensions-of-match}
-\index{match@{\tt match\ldots with\ldots end}}}
-
-\subsection{Multiple and nested pattern-matching
-\index{ML-like patterns}
-\label{Mult-match}}
-
-The basic version of \verb+match+ allows pattern-matching on simple
-patterns. As an extension, multiple nested patterns or disjunction of
-patterns are allowed, as in ML-like languages.
-
-The extension just acts as a macro that is expanded during parsing
-into a sequence of {\tt match} on simple patterns. Especially, a
-construction defined using the extended {\tt match} is generally
-printed under its expanded form (see~\texttt{Set Printing Matching} in
-section~\ref{SetPrintingMatching}).
-
-\SeeAlso Chapter~\ref{Mult-match-full}.
-
-\subsection{Pattern-matching on boolean values: the {\tt if} expression
-\label{if-then-else}
-\index{if@{\tt if ... then ... else}}}
-
-For inductive types with exactly two constructors and for
-pattern-matchings expressions which do not depend on the arguments of
-the constructors, it is possible to use a {\tt if ... then ... else}
-notation. For instance, the definition
-
-\begin{coq_example}
-Definition not (b:bool) :=
-  match b with
-  | true => false
-  | false => true
-  end.
-\end{coq_example}
-
-\noindent can be alternatively written
-
-\begin{coq_eval}
-Reset not.
-\end{coq_eval}
-\begin{coq_example}
-Definition not (b:bool) := if b then false else true.
-\end{coq_example}
-
-More generally, for an inductive type with constructors {\tt C$_1$}
-and {\tt C$_2$}, we have the following equivalence
-
-\smallskip
-
-{\tt if {\term} \zeroone{\ifitem} then {\term}$_1$ else {\term}$_2$} $\equiv$
-\begin{tabular}[c]{l}
-{\tt match {\term} \zeroone{\ifitem} with}\\
-{\tt \verb!|! C$_1$ \_ {\ldots} \_ \verb!=>! {\term}$_1$} \\
-{\tt \verb!|! C$_2$ \_ {\ldots} \_ \verb!=>! {\term}$_2$} \\
-{\tt end}
-\end{tabular}
-
-Here is an example.
-
-\begin{coq_example}
-Check (fun x (H:{x=0}+{x<>0}) =>
-  match H with
-  | left _ => true
-  | right _ => false
-  end).
-\end{coq_example}
-
-Notice that the printing uses the {\tt if} syntax because {\tt sumbool} is
-declared as such (see Section~\ref{printing-options}).
-
-\subsection{Irrefutable patterns: the destructuring {\tt let} variants 
-\index{let in@{\tt let ... in}}
-\label{Letin}}
-
-Pattern-matching on terms inhabiting inductive type having only one
-constructor can be alternatively written using {\tt let ... in ...}
-constructions. There are two variants of them.
-
-\subsubsection{First destructuring {\tt let} syntax}
-The expression {\tt let
-(}~{\ident$_1$},\ldots,{\ident$_n$}~{\tt ) :=}~{\term$_0$}~{\tt
-in}~{\term$_1$} performs case analysis on a {\term$_0$} which must be in
-an inductive type with one constructor having itself $n$ arguments. Variables
-{\ident$_1$}\ldots{\ident$_n$} are bound to the $n$ arguments of the
-constructor in expression {\term$_1$}. For instance, the definition
-
-\begin{coq_example}
-Definition fst (A B:Set) (H:A * B) := match H with
-                                      | pair x y => x
-                                      end.
-\end{coq_example}
-
-can be alternatively written 
-
-\begin{coq_eval}
-Reset fst.
-\end{coq_eval}
-\begin{coq_example}
-Definition fst (A B:Set) (p:A * B) := let (x, _) := p in x.
-\end{coq_example}
-Notice that reduction is different from regular {\tt let ... in ...}
-construction since it happens only if {\term$_0$} is in constructor
-form. Otherwise, the reduction is blocked.
-
-The pretty-printing of a definition by matching on a
-irrefutable pattern can either be done using {\tt match} or the {\tt
-let} construction (see Section~\ref{printing-options}).
-
-If {\term} inhabits an inductive type with one constructor {\tt C},
-we have an equivalence between
-
-{\tt let ({\ident}$_1$,\ldots,{\ident}$_n$) \zeroone{\ifitem} := {\term} in {\term}'}
-
-\noindent and
-
-{\tt match {\term} \zeroone{\ifitem} with C {\ident}$_1$ {\ldots} {\ident}$_n$ \verb!=>! {\term}' end}
-
-
-\subsubsection{Second destructuring {\tt let} syntax\index{let '... in@\texttt{let '... in}}}
-
-Another destructuring {\tt let} syntax is available for inductive types with
-one constructor by giving an arbitrary pattern instead of just a tuple
-for all the arguments. For example, the preceding example can be written:
-\begin{coq_eval}
-Reset fst.
-\end{coq_eval}
-\begin{coq_example}
-Definition fst (A B:Set) (p:A*B) := let 'pair x _ := p in x.
-\end{coq_example}
-
-This is useful to match deeper inside tuples and also to use notations
-for the pattern, as the syntax {\tt let 'p := t in b} allows arbitrary
-patterns to do the deconstruction. For example:
-
-\begin{coq_example}
-Definition deep_tuple (A:Set) (x:(A*A)*(A*A)) : A*A*A*A :=
-  let '((a,b), (c, d)) := x in (a,b,c,d).
-Notation " x 'With' p " := (exist _ x p) (at level 20).
-Definition proj1_sig' (A:Set) (P:A->Prop) (t:{ x:A | P x }) : A :=
-  let 'x With p := t in x.
-\end{coq_example}
-
-When printing definitions which are written using this construct it
-takes precedence over {\tt let} printing directives for the datatype
-under consideration (see Section~\ref{printing-options}).
-
-\subsection{Controlling pretty-printing of {\tt match} expressions
-\label{printing-options}}
-
-The following commands give some control over the pretty-printing of
-{\tt match} expressions.
-
-\subsubsection{Printing nested patterns
-\label{SetPrintingMatching}
-\optindex{Printing Matching}}
-
-The Calculus of Inductive Constructions knows pattern-matching only
-over simple patterns. It is however convenient to re-factorize nested
-pattern-matching into a single pattern-matching over a nested pattern.
-{\Coq}'s printer try to do such limited re-factorization.
-
-\begin{quote}
-{\tt Set Printing Matching.}
-\end{quote}
-This tells {\Coq} to try to use nested patterns. This is the default
-behavior.
-
-\begin{quote}
-{\tt Unset Printing Matching.}
-\end{quote}
-This tells {\Coq} to print only simple pattern-matching problems in
-the same way as the {\Coq} kernel handles them.
-
-\begin{quote}
-{\tt Test Printing Matching.}
-\end{quote}
-This tells if the printing matching mode is on or off. The default is
-on.
-
-\subsubsection{Factorization of clauses with same right-hand side}
-\label{SetPrintingFactorizableMatchPatterns}
-\optindex{Printing Factorizable Match Patterns}
-
-When several patterns share the same right-hand side, it is
-additionally possible to share the clauses using disjunctive patterns.
-Assuming that the printing matching mode is on, whether {\Coq}'s
-printer shall try to do this kind of factorization is governed by the
-following commands:
-
-\begin{quote}
-{\tt Set Printing Factorizable Match Patterns.}
-\end{quote}
-This tells {\Coq}'s printer to try to use disjunctive patterns. This is the default
-behavior.
-
-\begin{quote}
-{\tt Unset Printing Factorizable Match Patterns.}
-\end{quote}
-This tells {\Coq}'s printer not to try to use disjunctive patterns.
-
-\begin{quote}
-{\tt Test Printing Factorizable Match Patterns.}
-\end{quote}
-This tells if the factorization of clauses with same right-hand side is
-on or off.
-
-\subsubsection{Use of a default clause}
-\label{SetPrintingAllowDefaultClause}
-\optindex{Printing Allow Default Clause}
-
-When several patterns share the same right-hand side which do not
-depend on the arguments of the patterns, yet an extra factorization is
-possible: the disjunction of patterns can be replaced with a ``{\tt
-  \_}'' default clause. Assuming that the printing matching mode and
-the factorization mode are on, whether {\Coq}'s printer shall try to
-use a default clause is governed by the following commands:
-
-\begin{quote}
-{\tt Set Printing Allow Default Clause.}
-\end{quote}
-This tells {\Coq}'s printer to use a default clause when relevant. This is the default
-behavior.
-
-\begin{quote}
-{\tt Unset Printing Allow Default Clause.}
-\end{quote}
-This tells {\Coq}'s printer not to use a default clause.
-
-\begin{quote}
-{\tt Test Printing Allow Default Clause.}
-\end{quote}
-This tells if the use of a default clause is allowed.
-
-\subsubsection{Printing of wildcard pattern
-\optindex{Printing Wildcard}}
-
-Some variables in a pattern may not occur in the right-hand side of
-the pattern-matching clause.  There are options to control the
-display of these variables.
-
-\begin{quote}
-{\tt Set Printing Wildcard.}
-\end{quote}
-The variables having no occurrences in the right-hand side of the
-pattern-matching clause are just printed using the wildcard symbol
-``{\tt \_}''.
-
-\begin{quote}
-{\tt Unset Printing Wildcard.}
-\end{quote}
-The variables, even useless, are printed using their usual name. But some
-non dependent variables have no name. These ones are still printed
-using a ``{\tt \_}''.
-
-\begin{quote}
-{\tt Test Printing Wildcard.}
-\end{quote}
-This tells if the wildcard printing mode is on or off. The default is
-to print wildcard for useless variables.
-
-\subsubsection{Printing of the elimination predicate
-\optindex{Printing Synth}}
-
-In most of the cases, the type of the result of a matched term is
-mechanically synthesizable. Especially, if the result type does not
-depend of the matched term.
-
-\begin{quote}
-{\tt Set Printing Synth.}
-\end{quote}
-The result type is not printed when {\Coq} knows that it can
-re-synthesize it.
-
-\begin{quote}
-{\tt Unset Printing Synth.}
-\end{quote}
-This forces the result type to be always printed.
-
-\begin{quote}
-{\tt Test Printing Synth.}
-\end{quote}
-This tells if the non-printing of synthesizable types is on or off.
-The default is to not print synthesizable types.
-
-\subsubsection{Printing matching on irrefutable pattern
-\label{AddPrintingLet}
-\comindex{Add Printing Let {\ident}}
-\comindex{Remove Printing Let {\ident}}
-\comindex{Test Printing Let for {\ident}}
-\comindex{Print Table Printing Let}}
-
-If an inductive type has just one constructor,
-pattern-matching can be written using the first destructuring let syntax.
-
-\begin{quote}
-{\tt Add Printing Let {\ident}.}
-\end{quote}
-This adds {\ident} to the list of inductive types for which
-pattern-matching is written using a {\tt let} expression.
-
-\begin{quote}
-{\tt Remove Printing Let {\ident}.}
-\end{quote}
-This removes {\ident} from this list. Note that removing an inductive
-type from this list has an impact only for pattern-matching written using
-\texttt{match}. Pattern-matching explicitly written using a destructuring
-let are not impacted.
-
-\begin{quote}
-{\tt Test Printing Let for {\ident}.}
-\end{quote}
-This tells if {\ident} belongs to the list.
-
-\begin{quote}
-{\tt Print Table Printing Let.}
-\end{quote}
-This prints the list of inductive types for which pattern-matching is
-written using a {\tt let} expression.
-
-The list of inductive types for which pattern-matching is written
-using a {\tt let} expression is managed synchronously. This means that
-it is sensible to the command {\tt Reset}.
-
-\subsubsection{Printing matching on booleans
-\comindex{Add Printing If {\ident}}
-\comindex{Remove Printing If {\ident}}
-\comindex{Test Printing If for {\ident}}
-\comindex{Print Table Printing If}}
-
-If an inductive type is isomorphic to the boolean type,
-pattern-matching can be written using {\tt if} ... {\tt then} ... {\tt
-  else} ...
-
-\begin{quote}
-{\tt Add Printing If {\ident}.}
-\end{quote}
-This adds {\ident} to the list of inductive types for which
-pattern-matching is written using an {\tt if} expression.
-
-\begin{quote}
-{\tt Remove Printing If {\ident}.}
-\end{quote}
-This removes {\ident} from this list.
-
-\begin{quote}
-{\tt Test Printing If for {\ident}.}
-\end{quote}
-This tells if {\ident} belongs to the list.
-
-\begin{quote}
-{\tt Print Table Printing If.}
-\end{quote}
-This prints the list of inductive types for which pattern-matching is
-written using an {\tt if} expression.
-
-The list of inductive types for which pattern-matching is written
-using an {\tt if} expression is managed synchronously. This means that
-it is sensible to the command {\tt Reset}.
-
-\subsubsection{Example}
-
-This example emphasizes what the printing options offer.
-
-\begin{coq_example}
-Definition snd (A B:Set) (H:A * B) := match H with
-                                      | pair x y => y
-                                      end.
-Test Printing Let for prod.
-Print snd.
-Remove Printing Let prod.
-Unset Printing Synth.
-Unset Printing Wildcard.
-Print snd.
-\end{coq_example}
-\begin{coq_eval}
-Reset Initial.
-\end{coq_eval}
-
-\subsection{Printing \mbox{\tt match} templates}
-
-The {\tt Show Match} vernacular command prints a {\tt match} template for
-a given type. See Section~\ref{Show}.
-
-% \subsection{Still not dead old notations}
-
-% The following variant of {\tt match} is inherited from older version
-% of {\Coq}. 
-
-% \medskip
-% \begin{tabular}{lcl}
-% {\term} & ::= & {\annotation} {\tt Match} {\term} {\tt with} {\terms} {\tt end}\\
-% \end{tabular}
-% \medskip
-
-% This syntax is a macro generating a combination of {\tt match} with {\tt
-% Fix} implementing a combinator for primitive recursion equivalent to
-% the {\tt Match} construction of \Coq\ V5.8. It is provided only for
-% sake of compatibility with \Coq\ V5.8. It is recommended to avoid it.
-% (see Section~\ref{Matchexpr}).
-
-% There is also a notation \texttt{Case} that is the
-% ancestor of \texttt{match}. Again, it is still in the code for
-% compatibility with old versions but the user should not use it.
-
-% Explained in RefMan-gal.tex
-%% \section{Forced type}
-
-%% In some cases, one may wish to assign a particular type to a term. The
-%% syntax to force the type of a term is the following:
-
-%% \medskip
-%% \begin{tabular}{lcl}
-%% {\term} & ++= & {\term} {\tt :} {\term}\\
-%% \end{tabular}
-%% \medskip
-
-%% It forces the first term to be of type the second term. The
-%% type must be compatible with
-%% the term. More precisely it must be either a type convertible to
-%% the automatically inferred type (see Chapter~\ref{Cic}) or a type
-%% coercible to it, (see \ref{Coercions}). When the type of a
-%% whole expression is forced, it is usually not necessary to give the types of
-%% the variables involved in the term.
-
-%% Example:
-
-%% \begin{coq_example}
-%% Definition ID := forall X:Set, X -> X.
-%% Definition id := (fun X x => x):ID.
-%% Check id.
-%% \end{coq_example}
-
-\section{Advanced recursive functions}
-
-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}
-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
-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 might not
-necessarily be \emph{structurally} decreasing. The point of the {\tt
-  \{\}} annotation is to name the decreasing argument \emph{and} to
-describe which kind of decreasing criteria must be used to ensure
-termination of recursive calls.
-
-The {\tt Function} construction also enjoys the {\tt with} extension
-to define mutually recursive definitions. However, this feature does
-not work for non structurally recursive functions. % VRAI??
-
-See the documentation of {\tt functional induction}
-(see Section~\ref{FunInduction}) and {\tt Functional Scheme}
-(see Section~\ref{FunScheme} and \ref{FunScheme-examples}) for how to use the
-induction principle to easily reason about the function.
-
-\noindent {\bf Remark: } To obtain the right principle, it is better
-to put rigid parameters of the function as first arguments. For
-example it is better to define plus like this:
-
-\begin{coq_example*}
-Function plus (m n : nat) {struct n} : nat :=
-  match n with
-  | 0 => m
-  | S p => S (plus m p)
-  end.
-\end{coq_example*}
-\noindent than like this:
-\begin{coq_eval}
-Reset plus.
-\end{coq_eval}
-\begin{coq_example*}
-Function plus (n m : nat) {struct n} : nat :=
-  match n with
-  | 0 => m
-  | S p => S (plus p m)
-  end.
-\end{coq_example*}
-
-\paragraph[Limitations]{Limitations\label{sec:Function-limitations}}
-\term$_0$ must be built as a \emph{pure pattern-matching tree}
-(\texttt{match...with}) with applications only \emph{at the end} of
-each branch.  
-
-Function does not support partial application of the function being defined. Thus, the following example cannot be accepted due to the presence of partial application of \ident{wrong} into the body of \ident{wrong}~:
-\begin{coq_eval}
-Require List.
-\end{coq_eval}
-\begin{coq_example*}
-Fail Function wrong (C:nat) : nat :=
-  List.hd 0 (List.map wrong (C::nil)).
-\end{coq_example*}
-
-For now dependent cases are not treated for non structurally terminating functions.
-
-
-
-\begin{ErrMsgs}
-\item \errindex{The recursive argument must be specified}
-\item \errindex{No argument name \ident}
-\item \errindex{Cannot use mutual definition with well-founded
-    recursion or measure}
-
-\item \errindex{Cannot define graph for \ident\dots} (warning)
-
-  The generation of the graph relation \texttt{(R\_\ident)} used to
-  compute the induction scheme of \ident\ raised a typing error. Only
-  the ident is defined; the induction scheme will not be generated.
-
-  This error happens generally when:
-
-  \begin{itemize}
-  \item the definition uses pattern matching on dependent types, which
-    \texttt{Function} cannot deal with yet.
-  \item the definition is not a \emph{pattern-matching tree} as
-    explained above.
-  \end{itemize}
-
-\item \errindex{Cannot define principle(s) for \ident\dots} (warning)
-
-  The generation of the graph relation \texttt{(R\_\ident)} succeeded
-  but the induction principle could not be built. Only the ident is
-  defined. Please report.
-
-\item \errindex{Cannot build functional inversion principle} (warning)
-
-  \texttt{functional inversion} will not be available for the
-  function.
-\end{ErrMsgs}
-
-
-\SeeAlso{\ref{FunScheme}, \ref{FunScheme-examples}, \ref{FunInduction}}
-
-Depending on the {\tt \{$\ldots$\}} annotation, different definition
-mechanisms are used by {\tt Function}. More precise description
-given below.
-
-\begin{Variants}
-\item \texttt{ Function {\ident} {\binder$_1$}\ldots{\binder$_n$}
-    : type$_0$ := \term$_0$}
-
-  Defines the not recursive function \ident\ as if declared with
-  \texttt{Definition}.  Moreover the following are defined:
-
-  \begin{itemize}
-  \item {\tt\ident\_rect}, {\tt\ident\_rec} and {\tt\ident\_ind},
-    which reflect the pattern matching structure of \term$_0$ (see the
-    documentation of {\tt Inductive} \ref{Inductive});
-  \item The inductive \texttt{R\_\ident} corresponding to the graph of
-    \ident\ (silently);
-  \item \texttt{\ident\_complete} and \texttt{\ident\_correct} which are
-    inversion information linking the function and its graph.
-  \end{itemize}
-\item \texttt{Function {\ident} {\binder$_1$}\ldots{\binder$_n$}
-    {\tt \{}{\tt struct} \ident$_0${\tt\}} : type$_0$ := \term$_0$}
-  
-  Defines the structural recursive function \ident\ as if declared
-  with \texttt{Fixpoint}.  Moreover the following are defined:
-
-  \begin{itemize}
-  \item The same objects as above;
-  \item The fixpoint equation of \ident: \texttt{\ident\_equation}.
-  \end{itemize}
-  
-\item \texttt{Function {\ident} {\binder$_1$}\ldots{\binder$_n$} {\tt
-      \{}{\tt measure \term$_1$} \ident$_0${\tt\}} : type$_0$ :=
-    \term$_0$}
-\item \texttt{Function {\ident} {\binder$_1$}\ldots{\binder$_n$}
- {\tt \{}{\tt wf \term$_1$} \ident$_0${\tt\}} : type$_0$ := \term$_0$}
-
-Defines a recursive function by well founded recursion. \textbf{The
-module \texttt{Recdef} of the standard library must be loaded for this
-feature}. The {\tt \{\}} annotation is mandatory and must be one of
-the following:
-\begin{itemize}
-\item {\tt \{measure} \term$_1$ \ident$_0${\tt\}} with \ident$_0$
-      being the decreasing argument and \term$_1$ being a function
-      from type of \ident$_0$ to \texttt{nat} for which value on the
-      decreasing argument decreases (for the {\tt lt} order on {\tt
-      nat}) at each recursive call of \term$_0$. Parameters of the
-      function are bound in  \term$_0$;
-\item {\tt \{wf} \term$_1$ \ident$_0${\tt\}} with \ident$_0$ being
-      the decreasing argument and \term$_1$ an ordering relation on
-      the type of \ident$_0$ (i.e. of type T$_{\ident_0}$
-      $\to$ T$_{\ident_0}$ $\to$ {\tt Prop}) for which
-      the decreasing argument decreases at each recursive call of
-      \term$_0$. The order must be well founded. Parameters of the
-      function are bound in  \term$_0$.
-\end{itemize} 
-
-Depending on the annotation, the user is left with some proof
-obligations that will be used to define the function. These proofs
-are: proofs that each recursive call is actually decreasing with
-respect to the given criteria, and (if the criteria is \texttt{wf}) a
-proof that the ordering relation is well founded.
-
-%Completer sur measure et wf
-
-Once proof obligations are discharged, the following objects are
-defined:
-
-\begin{itemize}
-\item The same objects as with the \texttt{struct};
-\item The lemma \texttt{\ident\_tcc} which collects all proof
-  obligations in one property;
-\item The lemmas \texttt{\ident\_terminate} and \texttt{\ident\_F}
-  which is needed to be inlined during extraction of \ident.
-\end{itemize}
-
-
-
-%Complete!!
-The way this recursive function is defined is the subject of several
-papers by Yves Bertot and Antonia Balaa on the one hand, and Gilles Barthe,
-Julien Forest, David Pichardie, and Vlad Rusu on the other hand.
-
-%Exemples ok ici
-
-\bigskip
-
-\noindent {\bf Remark: } Proof obligations are presented as several
-subgoals belonging to a Lemma {\ident}{\tt\_tcc}. % These subgoals are independent which means that in order to
-% abort them you will have to abort each separately.
-
-
-
-%The decreasing argument cannot be dependent of another??
-
-%Exemples faux ici
-\end{Variants}
-
-
-\section{Section mechanism
-\index{Sections}
-\label{Section}}
-
-The sectioning mechanism can be used to to organize a proof in
-structured sections. Then local declarations become available (see
-Section~\ref{Basic-definitions}).
-
-\subsection{\tt Section {\ident}\comindex{Section}}
-
-This command is used to open a section named {\ident}.
-
-%% Discontinued ?
-%% \begin{Variants}
-%% \comindex{Chapter}
-%% \item{\tt Chapter {\ident}}\\
-%%         Same as {\tt Section {\ident}}
-%% \end{Variants}
-
-\subsection{\tt End {\ident}
-\comindex{End}}
-
-This command closes the section named {\ident}. After closing of the
-section, the local declarations (variables and local definitions) get
-{\em discharged}, meaning that they stop being visible and that all
-global objects defined in the section are generalized with respect to
-the variables and local definitions they each depended on in the
-section.
-
-
-Here is an example :
-\begin{coq_example}
-Section s1.
-Variables x y : nat.
-Let y' := y.
-Definition x' := S x.
-Definition x'' := x' + y'.
-Print x'.
-End s1.
-Print x'.
-Print x''.
-\end{coq_example}
-Notice the difference between the value of {\tt x'} and {\tt x''}
-inside section {\tt s1} and outside.
-
-\begin{ErrMsgs}
-\item \errindex{This is not the last opened section}
-\end{ErrMsgs}
-
-\begin{Remarks}
-\item Most commands, like {\tt Hint}, {\tt Notation}, option management, ...
-which appear inside a section are canceled when the
-section is closed.
-% see Section~\ref{LongNames}
-%\item Usually all identifiers must be distinct. 
-%However, a name already used in a closed section (see \ref{Section})
-%can be reused. In this case, the old name is no longer accessible.
-
-% Obsolète
-%\item A module implicitly open a section. Be careful not to name a
-%module with an identifier already used in the module (see \ref{compiled}).
-\end{Remarks}
-
-\input{RefMan-mod.v}
-
-\section{Libraries and qualified names}
-
-\subsection{Names of libraries
-\label{Libraries}
-\index{Libraries}}
-
-The theories developed in {\Coq} are stored in {\em library files}
-which are hierarchically classified into {\em libraries} and {\em
-  sublibraries}. To express this hierarchy, library names are
-represented by qualified identifiers {\qualid}, i.e. as list of
-identifiers separated by dots (see Section~\ref{qualid}). For
-instance, the library file {\tt Mult} of the standard {\Coq} library
-{\tt Arith} is named {\tt Coq.Arith.Mult}. The identifier that starts
-the name of a library is called a {\em library root}.  All library
-files of the standard library of {\Coq} have the reserved root {\tt Coq}
-but library file names based on other roots can be obtained by using
-{\Coq} commands ({\tt coqc}, {\tt coqtop}, {\tt coqdep}, \dots) options
-{\tt -Q} or {\tt -R} (see Section~\ref{coqoptions}). Also, when an
-interactive {\Coq} session starts, a library of root {\tt Top} is
-started, unless option {\tt -top} is set (see
-Section~\ref{coqoptions}).
-
-\subsection{Qualified names
-\label{LongNames}
-\index{Qualified identifiers}
-\index{Absolute names}}
-
-Library files are modules which possibly contain submodules which
-eventually contain constructions (axioms, parameters, definitions,
-lemmas, theorems, remarks or facts). The {\em absolute name}, or {\em
-full name}, of a construction in some library file is a qualified
-identifier starting with the logical name of the library file,
-followed by the sequence of submodules names encapsulating the
-construction and ended by the proper name of the construction.
-Typically, the absolute name {\tt Coq.Init.Logic.eq} denotes Leibniz'
-equality defined in the module {\tt Logic} in the sublibrary {\tt
-Init} of the standard library of \Coq.
-
-The proper name that ends the name of a construction is the {\it short
-name} (or sometimes {\it base name}) of the construction (for
-instance, the short name of {\tt Coq.Init.Logic.eq} is {\tt eq}). Any
-partial suffix of the absolute name is a {\em partially qualified name}
-(e.g. {\tt Logic.eq} is a partially qualified name for {\tt
-Coq.Init.Logic.eq}).  Especially, the short name of a construction is
-its shortest partially qualified name.
-
-{\Coq} does not accept two constructions (definition, theorem, ...)
-with the same absolute name but different constructions can have the
-same short name (or even same partially qualified names as soon as the
-full names are different).
-
-Notice that the notion of absolute, partially qualified and
-short names also applies to library file names.
-
-\paragraph{Visibility}
-
-{\Coq} maintains a table called {\it name table} which maps partially
-qualified names of constructions to absolute names. This table is
-updated by the commands {\tt Require} (see \ref{Require}), {\tt
-Import} and {\tt Export} (see \ref{Import}) and also each time a new
-declaration is added to the context. An absolute name is called {\it
-visible} from a given short or partially qualified name when this
-latter name is enough to denote it. This means that the short or
-partially qualified name is mapped to the absolute name in {\Coq} name
-table. Definitions flagged as {\tt Local} are only accessible with their
-fully qualified name (see \ref{Definition}).
-
-It may happen that a visible name is hidden by the short name or a
-qualified name of another construction. In this case, the name that
-has been hidden must be referred to using one more level of
-qualification. To ensure that a construction always remains
-accessible, absolute names can never be hidden.
-
-Examples:
-\begin{coq_eval}
-Reset Initial.
-\end{coq_eval}
-\begin{coq_example}
-Check 0.
-Definition nat := bool.
-Check 0.
-Check Datatypes.nat.
-Locate nat.
-\end{coq_example}
-
-\SeeAlso Command {\tt Locate} in Section~\ref{Locate} and {\tt Locate
-Library} in Section~\ref{Locate Library}.
-
-\subsection{Libraries and filesystem\label{loadpath}\index{Loadpath}
-\index{Physical paths} \index{Logical paths}}
-
-Please note that the questions described here have been subject to
-redesign in Coq v8.5. Former versions of Coq use the same terminology
-to describe slightly different things.
-
-Compiled files (\texttt{.vo} and \texttt{.vio}) store sub-libraries. In
-order to refer to them inside {\Coq}, a translation from file-system
-names to {\Coq} names is needed. In this translation, names in the
-file system are called {\em physical} paths while {\Coq} names are
-contrastingly called {\em logical} names.
-
-A logical prefix {\tt Lib} can be associated to a physical path
-\textrm{\textsl{path}} using the command line option {\tt -Q}
-\textrm{\textsl{path}} {\tt Lib}. All subfolders of {\textsl{path}} are
-recursively associated to the logical path {\tt Lib} extended with the
-corresponding suffix coming from the physical path. For instance, the
-folder {\tt path/fOO/Bar} maps to {\tt Lib.fOO.Bar}. Subdirectories
-corresponding to invalid {\Coq} identifiers are skipped, and, by
-convention, subdirectories named {\tt CVS} or {\tt \_darcs} are
-skipped too.
-
-Thanks to this mechanism, {\texttt{.vo}} files are made available through the
-logical name of the folder they are in, extended with their own basename. For
-example, the name associated to the file {\tt path/fOO/Bar/File.vo} is
-{\tt Lib.fOO.Bar.File}. The same caveat applies for invalid identifiers.
-When compiling a source file, the {\texttt{.vo}} file stores its logical name,
-so that an error is issued if it is loaded with the wrong loadpath afterwards.
-
-Some folders have a special status and are automatically put in the path.
-{\Coq} commands associate automatically a logical path to files
-in the repository trees rooted at the directory from where the command
-is launched, \textit{coqlib}\texttt{/user-contrib/}, the directories
-listed in the \verb:$COQPATH:, \verb:${XDG_DATA_HOME}/coq/: and
-\verb:${XDG_DATA_DIRS}/coq/: environment variables (see
-\url{http://standards.freedesktop.org/basedir-spec/basedir-spec-latest.html})
-with the same physical-to-logical translation and with an empty logical prefix.
-
-The command line option \texttt{-R} is a variant of \texttt{-Q} which has the
-strictly same behavior regarding loadpaths, but which also makes the
-corresponding \texttt{.vo} files available through their short names in a
-way not unlike the {\tt Import} command (see~{\ref{Import}}). For instance,
-\texttt{-R} \textrm{\textsl{path}} \texttt{Lib} associates to the file
-\texttt{path/fOO/Bar/File.vo} the logical name \texttt{Lib.fOO.Bar.File}, but
-allows this file to be accessed through the short names \texttt{fOO.Bar.File},
-\texttt{Bar.File} and \texttt{File}. If several files with identical base name
-are present in different subdirectories of a recursive loadpath, which of
-these files is found first may be system-dependent and explicit
-qualification is recommended. The {\tt From} argument of the {\tt Require}
-command can be used to bypass the implicit shortening by providing an absolute
-root to the required file (see~\ref{Require}).
-
-There also exists another independent loadpath mechanism attached to {\ocaml}
-object files (\texttt{.cmo} or \texttt{.cmxs}) rather than {\Coq} object files
-as described above. The {\ocaml} loadpath is managed using the option
-\texttt{-I path} (in the {\ocaml} world, there is neither a notion of logical
-name prefix nor a way to access files in subdirectories of \texttt{path}).
-See the command \texttt{Declare ML Module} in Section~\ref{compiled} to
-understand the need of the {\ocaml} loadpath.
-
-See Section~\ref{coqoptions} for a more general view over the {\Coq}
-command line options.
-
-%% \paragraph{The special case of remarks and facts}
-%% 
-%% In contrast with definitions, lemmas, theorems, axioms and parameters,
-%% the absolute name of remarks includes the segment of sections in which
-%% it is defined. Concretely, if a remark {\tt R} is defined in
-%% subsection {\tt S2} of section {\tt S1} in module {\tt M}, then its
-%% absolute name is {\tt M.S1.S2.R}. The same for facts, except that the
-%% name of the innermost section is dropped from the full name. Then, if
-%% a fact {\tt F} is defined in subsection {\tt S2} of section {\tt S1}
-%% in module {\tt M}, then its absolute name is {\tt M.S1.F}.
-
-\section{Implicit arguments
-\index{Implicit arguments}
-\label{Implicit Arguments}}
-
-An implicit argument of a function is an argument which can be
-inferred from contextual knowledge. There are different kinds of
-implicit arguments that can be considered implicit in different
-ways. There are also various commands to control the setting or the
-inference of implicit arguments.
-
-\subsection{The different kinds of implicit arguments}
-
-\subsubsection{Implicit arguments inferable from the knowledge of other 
-arguments of a function}
-
-The first kind of implicit arguments covers the arguments that are
-inferable from the knowledge of the type of other arguments of the
-function, or of the type of the surrounding context of the
-application.  Especially, such implicit arguments correspond to 
-parameters dependent in the type of the function. Typical implicit
-arguments are the type arguments in polymorphic functions.  
-There are several kinds of such implicit arguments.
-
-\paragraph{Strict Implicit Arguments.} 
-An implicit argument can be either strict or non strict. An implicit
-argument is said {\em strict} if, whatever the other arguments of the
-function are, it is still inferable from the type of some other
-argument. Technically, an implicit argument is strict if it
-corresponds to a parameter which is not applied to a variable which
-itself is another parameter of the function (since this parameter
-may erase its arguments), not in the body of a {\tt match}, and not
-itself applied or matched against patterns (since the original
-form of the argument can be lost by reduction).
-
-For instance, the first argument of
-\begin{quote}
-\verb|cons: forall A:Set, A -> list A -> list A|
-\end{quote}
-in module {\tt List.v} is strict because {\tt list} is an inductive
-type and {\tt A} will always be inferable from the type {\tt
-list A} of the third argument of {\tt cons}.
-On the contrary, the second argument of a term of type 
-\begin{quote}
-\verb|forall P:nat->Prop, forall n:nat, P n -> ex nat P|
-\end{quote}
-is implicit but not strict, since it can only be inferred from the
-type {\tt P n} of the third argument and if {\tt P} is, e.g., {\tt
-fun \_ => True}, it reduces to an expression where {\tt n} does not
-occur any longer. The first argument {\tt P} is implicit but not
-strict either because it can only be inferred from {\tt P n} and {\tt
-P} is not canonically inferable from an arbitrary {\tt n} and the
-normal form of {\tt P n} (consider e.g. that {\tt n} is {\tt 0} and
-the third argument has type {\tt True}, then any {\tt P} of the form
-{\tt fun n => match n with 0 => True | \_ => \mbox{\em anything} end} would
-be a solution of the inference problem).
-
-\paragraph{Contextual Implicit Arguments.} 
-An implicit argument can be {\em contextual} or not. An implicit
-argument is said {\em contextual} if it can be inferred only from the
-knowledge of the type of the context of the current expression. For
-instance, the only argument of
-\begin{quote}
-\verb|nil : forall A:Set, list A|
-\end{quote}
-is contextual. Similarly, both arguments of a term of type
-\begin{quote}
-\verb|forall P:nat->Prop, forall n:nat, P n \/ n = 0|
-\end{quote}
-are contextual (moreover, {\tt n} is strict and {\tt P} is not).
-
-\paragraph{Reversible-Pattern Implicit Arguments.}
-There is another class of implicit arguments that can be reinferred
-unambiguously if all the types of the remaining arguments are
-known. This is the class of implicit arguments occurring in the type
-of another argument in position of reversible pattern, which means it
-is at the head of an application but applied only to uninstantiated
-distinct variables. Such an implicit argument is called {\em
-reversible-pattern implicit argument}. A typical example is the
-argument {\tt P} of {\tt nat\_rec} in
-\begin{quote}
-{\tt nat\_rec : forall P : nat -> Set,
-       P 0 -> (forall n : nat, P n -> P (S n)) -> forall x : nat, P x}.
-\end{quote}
-({\tt P} is reinferable by abstracting over {\tt n} in the type {\tt P n}).
-
-See Section~\ref{SetReversiblePatternImplicit} for the automatic declaration
-of reversible-pattern implicit arguments.
-
-\subsubsection{Implicit arguments inferable by resolution}
-
-This corresponds to a class of non dependent implicit arguments that
-are solved based on the structure of their type only.
-
-\subsection{Maximal or non maximal insertion of implicit arguments}
-
-In case a function is partially applied, and the next argument to be
-applied is an implicit argument, two disciplines are applicable. In the
-first case, the function is considered to have no arguments furtherly:
-one says that the implicit argument is not maximally inserted. In
-the second case, the function is considered to be implicitly applied
-to the implicit arguments it is waiting for: one says that the
-implicit argument is maximally inserted.
-
-Each implicit argument can be declared to have to be inserted
-maximally or non maximally. This can be governed argument per argument
-by the command {\tt Implicit Arguments} (see~\ref{ImplicitArguments})
-or globally by the command {\tt Set Maximal Implicit Insertion}
-(see~\ref{SetMaximalImplicitInsertion}). See also
-Section~\ref{PrintImplicit}.
-
-\subsection{Casual use of implicit arguments}
-
-In a given expression, if it is clear that some argument of a function
-can be inferred from the type of the other arguments, the user can
-force the given argument to be guessed by replacing it by ``{\tt \_}''. If
-possible, the correct argument will be automatically generated.
-
-\begin{ErrMsgs}
-
-\item \errindex{Cannot infer a term for this placeholder}
-
-  {\Coq} was not able to deduce an instantiation of a ``{\tt \_}''.
-
-\end{ErrMsgs}
-
-\subsection{Declaration of implicit arguments
-\comindex{Arguments}}
-\label{ImplicitArguments}
-
-In case one wants that some arguments of a given object (constant,
-inductive types, constructors, assumptions, local or not) are always
-inferred by Coq, one may declare once and for all which are the expected
-implicit arguments of this object. There are two ways to do this,
-a priori and a posteriori.
-
-\subsubsection{Implicit Argument Binders}
-
-In the first setting, one wants to explicitly give the implicit
-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.
-\end{coq_eval}
-\begin{coq_example}
-Definition id {A : Type} (x : A) : A := x.
-\end{coq_example}
-
-This automatically declares the argument {\tt A} of {\tt id} as a
-maximally inserted implicit argument. One can then do as-if the argument
-was absent in every situation but still be able to specify it if needed:
-\begin{coq_example}
-Definition compose {A B C} (g : B -> C) (f : A -> B) := 
-  fun x => g (f x).
-Goal forall A, compose id id = id (A:=A).
-\end{coq_example}
-
-The syntax is supported in all top-level definitions: {\tt Definition},
-{\tt Fixpoint}, {\tt Lemma} and so on. For (co-)inductive datatype
-declarations, the semantics are the following: an inductive parameter
-declared as an implicit argument need not be repeated in the inductive
-definition but will become implicit for the constructors of the
-inductive only, not the inductive type itself. For example:
-
-\begin{coq_example}
-Inductive list {A : Type} : Type :=
-| nil : list
-| cons : A -> list -> list.
-Print list.
-\end{coq_example}
-
-One can always specify the parameter if it is not uniform using the
-usual implicit arguments disambiguation syntax.
-
-\subsubsection{Declaring Implicit Arguments}
-
-To set implicit arguments a posteriori, one can use the
-command:
-\begin{quote}
-\tt Arguments {\qualid} \nelist{\possiblybracketedident}{}
-\end{quote}
-where the list of {\possiblybracketedident} is a prefix of the list of arguments
-of {\qualid} where the ones to be declared implicit are surrounded by square
-brackets and the ones to be declared as maximally inserted implicits are
-surrounded by curly braces.
-
-After the above declaration is issued, implicit arguments can just (and
-have to) be skipped in any expression involving an application of
-{\qualid}.
-
-Implicit arguments can be cleared with the following syntax:
-
-\begin{quote}
-{\tt Arguments {\qualid} : clear implicits
-\comindex{Arguments}}
-\end{quote}
-
-\begin{Variants}
-\item {\tt Global Arguments {\qualid} \nelist{\possiblybracketedident}{}
-\comindex{Global Arguments}}
-
-Tell to recompute the implicit arguments of {\qualid} after ending of
-the current section if any, enforcing the implicit arguments known
-from inside the section to be the ones declared by the command.
-
-\item {\tt Local Arguments {\qualid} \nelist{\possiblybracketedident}{}
-\comindex{Local Arguments}}
-
-When in a module, tell not to activate the implicit arguments of
-{\qualid} declared by this command to contexts that require the
-module.
-
-\item {\tt \zeroone{Global {\sl |} Local} Arguments {\qualid} \sequence{\nelist{\possiblybracketedident}{}}{,}}
-
-For names of constants, inductive types, constructors, lemmas which
-can only be applied to a fixed number of arguments (this excludes for
-instance constants whose type is polymorphic), multiple 
-implicit arguments decflarations can be given. 
-Depending on the number of arguments {\qualid} is applied
-to in practice, the longest applicable list of implicit arguments is
-used to select which implicit arguments are inserted.
-
-For printing, the omitted arguments are the ones of the longest list
-of implicit arguments of the sequence.
-
-\end{Variants}
-
-\Example
-\begin{coq_eval}
-Reset Initial.
-\end{coq_eval}
-\begin{coq_example*}
-Inductive list (A:Type) : Type :=
- | nil : list A 
- | cons : A -> list A -> list A.
-\end{coq_example*}
-\begin{coq_example}
-Check (cons nat 3 (nil nat)).
-Arguments cons [A] _ _.
-Arguments nil [A].
-Check (cons 3 nil).
-Fixpoint map (A B:Type) (f:A->B) (l:list A) : list B :=
-  match l with nil => nil | cons a t => cons (f a) (map A B f t) end.
-Fixpoint length (A:Type) (l:list A) : nat :=
-  match l with nil => 0 | cons _ m => S (length A m) end.
-Arguments map [A B] f l.
-Arguments length {A} l. (* A has to be maximally inserted *)
-Check (fun l:list (list nat) => map length l).
-Arguments map [A B] f l, [A] B f l, A B f l.
-Check (fun l => map length l = map (list nat) nat length l).
-\end{coq_example}
-
-\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}
-
-{\Coq} can also automatically detect what are the implicit arguments
-of a defined object. The command is just
-\begin{quote}
-{\tt Arguments {\qualid} : default implicits
-\comindex{Arguments}}
-\end{quote}
-The auto-detection is governed by options telling if strict,
-contextual, or reversible-pattern implicit arguments must be
-considered or not (see
-Sections~\ref{SetStrictImplicit},~\ref{SetContextualImplicit},~\ref{SetReversiblePatternImplicit}
-and also~\ref{SetMaximalImplicitInsertion}).
-
-\begin{Variants}
-\item {\tt Global Arguments {\qualid} : default implicits
-\comindex{Global Arguments}}
-
-Tell to recompute the implicit arguments of {\qualid} after ending of
-the current section if any.
-
-\item {\tt Local Arguments {\qualid} : default implicits
-\comindex{Local Arguments}}
-
-When in a module, tell not to activate the implicit arguments of
-{\qualid} computed by this declaration to contexts that requires the
-module.
-
-\end{Variants}
-
-\Example
-\begin{coq_eval}
-Reset Initial.
-\end{coq_eval}
-\begin{coq_example*}
-Inductive list (A:Set) : Set := 
-  | nil : list A 
-  | cons : A -> list A -> list A.
-\end{coq_example*}
-\begin{coq_example}
-Arguments cons : default implicits.
-Print Implicit cons.
-Arguments nil : default implicits.
-Print Implicit nil.
-Set Contextual Implicit.
-Arguments nil : default implicits.
-Print Implicit nil.
-\end{coq_example}
-
-The computation of implicit arguments takes account of the
-unfolding of constants.  For instance, the variable {\tt p} below has
-type {\tt (Transitivity R)} which is reducible to {\tt forall x,y:U, R x
-y -> forall z:U, R y z -> R x z}. As the variables {\tt x}, {\tt y} and
-{\tt z} appear strictly in body of the type, they are implicit.
-
-\begin{coq_example*}
-Variable X : Type.
-Definition Relation := X -> X -> Prop.
-Definition Transitivity (R:Relation) :=
-  forall x y:X, R x y -> forall z:X, R y z -> R x z.
-Variables (R : Relation) (p : Transitivity R).
-Arguments p : default implicits.
-\end{coq_example*}
-\begin{coq_example}
-Print p.
-Print Implicit p.
-\end{coq_example}
-\begin{coq_example*}
-Variables (a b c : X) (r1 : R a b) (r2 : R b c).
-\end{coq_example*}
-\begin{coq_example}
-Check (p r1 r2).
-\end{coq_example}
-
-\subsection{Mode for automatic declaration of implicit arguments
-\label{Auto-implicit}
-\optindex{Implicit Arguments}}
-
-In case one wants to systematically declare implicit the arguments
-detectable as such, one may switch to the automatic declaration of
-implicit arguments mode by using the command
-\begin{quote}
-\tt Set Implicit Arguments.
-\end{quote}
-Conversely, one may unset the mode by using {\tt Unset Implicit
-Arguments}.  The mode is off by default. Auto-detection of implicit
-arguments is governed by options controlling whether strict and
-contextual implicit arguments have to be considered or not.
-
-\subsection{Controlling strict implicit arguments
-\optindex{Strict Implicit}
-\label{SetStrictImplicit}}
-
-When the mode for automatic declaration of implicit arguments is on,
-the default is to automatically set implicit only the strict implicit
-arguments plus, for historical reasons, a small subset of the non
-strict implicit arguments. To relax this constraint and to
-set implicit all non strict implicit arguments by default, use the command
-\begin{quote}
-\tt Unset Strict Implicit.
-\end{quote}
-Conversely, use the command {\tt Set Strict Implicit} to
-restore the original mode that declares implicit only the strict implicit arguments plus a small subset of the non strict implicit arguments.
-
-In the other way round, to capture exactly the strict implicit arguments and no more than the strict implicit arguments, use the command:
-\optindex{Strongly Strict Implicit}
-\begin{quote}
-\tt Set Strongly Strict Implicit.
-\end{quote}
-Conversely, use the command {\tt Unset Strongly Strict Implicit} to
-let the option ``{\tt Strict Implicit}'' decide what to do.
-
-\Rem In versions of {\Coq} prior to version 8.0, the default was to
-declare the strict implicit arguments as implicit.
-
-\subsection{Controlling contextual implicit arguments
-\optindex{Contextual Implicit}
-\label{SetContextualImplicit}}
-
-By default, {\Coq} does not automatically set implicit the contextual
-implicit arguments. To tell {\Coq} to infer also contextual implicit
-argument, use command  
-\begin{quote}
-\tt Set Contextual Implicit. 
-\end{quote}
-Conversely, use command {\tt Unset Contextual Implicit} to
-unset the contextual implicit mode.
-
-\subsection{Controlling reversible-pattern implicit arguments
-\optindex{Reversible Pattern Implicit}
-\label{SetReversiblePatternImplicit}}
-
-By default, {\Coq} does not automatically set implicit the reversible-pattern
-implicit arguments. To tell {\Coq} to infer also reversible-pattern implicit
-argument, use command  
-\begin{quote}
-\tt Set Reversible Pattern Implicit. 
-\end{quote}
-Conversely, use command {\tt Unset Reversible Pattern Implicit} to
-unset the reversible-pattern implicit mode.
-
-\subsection{Controlling the insertion of implicit arguments not followed by explicit arguments
-\optindex{Maximal Implicit Insertion}
-\label{SetMaximalImplicitInsertion}}
-
-Implicit arguments can be declared to be automatically inserted when a
-function is partially applied and the next argument of the function is
-an implicit one. In case the implicit arguments are automatically
-declared (with the command {\tt Set Implicit Arguments}), the command
-\begin{quote}
-\tt Set Maximal Implicit Insertion. 
-\end{quote}
-is used to tell to declare the implicit arguments with a maximal
-insertion status. By default, automatically declared implicit
-arguments are not declared to be insertable maximally.  To restore the
-default mode for maximal insertion, use command {\tt Unset Maximal
-Implicit Insertion}.
-
-\subsection{Explicit applications
-\index{Explicitly given implicit arguments}
-\label{Implicits-explicitation}
-\index{qualid@{\qualid}} \index{\symbol{64}}}
-
-In presence of non strict or contextual argument, or in presence of
-partial applications, the synthesis of implicit arguments may fail, so
-one may have to give explicitly certain implicit arguments of an
-application. The syntax for this is {\tt (\ident:=\term)} where {\ident}
-is the name of the implicit argument and {\term} is its corresponding
-explicit term. Alternatively, one can locally deactivate the hiding of
-implicit arguments of a function by using the notation
-{\tt @{\qualid}~{\term}$_1$..{\term}$_n$}. This syntax extension is
-given Figure~\ref{fig:explicitations}.
-\begin{figure}
-\begin{centerframe}
-\begin{tabular}{lcl}
-{\term} & ++= & @ {\qualid} \nelist{\term}{}\\
-& $|$ & @ {\qualid}\\
-& $|$ & {\qualid} \nelist{\textrm{\textsl{argument}}}{}\\
-\\
-{\textrm{\textsl{argument}}} & ::= & {\term} \\
-& $|$ & {\tt ({\ident}:={\term})}\\
-\end{tabular}
-\end{centerframe}
-\caption{Syntax for explicitly giving implicit arguments}
-\label{fig:explicitations}
-\end{figure}
-
-\noindent {\bf Example (continued): }
-\begin{coq_example}
-Check (p r1 (z:=c)).
-Check (p (x:=a) (y:=b) r1 (z:=c) r2).
-\end{coq_example}
-
-\subsection{Renaming implicit arguments
-\comindex{Arguments}
-}
-
-Implicit arguments names can be redefined using the following syntax:
-\begin{quote}
-{\tt Arguments {\qualid} \nelist{\name}{}  : rename}
-\end{quote}
-
-With the {\tt assert} flag, {\tt Arguments} can be used to assert
-that a given object has the expected number of arguments and that
-these arguments are named as expected.
-
-\noindent {\bf Example (continued): }
-\begin{coq_example}
-Arguments p [s t] _ [u] _: rename.
-Check (p r1 (u:=c)).
-Check (p (s:=a) (t:=b) r1 (u:=c) r2).
-Fail Arguments p [s t] _ [w] _ : assert.
-\end{coq_example}
-
-
-\subsection{Displaying what the implicit arguments are
-\comindex{Print Implicit}
-\label{PrintImplicit}}
-
-To display the implicit arguments associated to an object, and to know
-if each of them is to be used maximally or not, use the command
-\begin{quote}
-\tt Print Implicit {\qualid}.
-\end{quote}
-
-\subsection{Explicit displaying of implicit arguments for pretty-printing
-\optindex{Printing Implicit}
-\optindex{Printing Implicit Defensive}}
-
-By default the basic pretty-printing rules hide the inferable implicit
-arguments of an application. To force printing all implicit arguments,
-use command
-\begin{quote}
-{\tt Set Printing Implicit.}
-\end{quote}
-Conversely, to restore the hiding of implicit arguments, use command
-\begin{quote}
-{\tt Unset Printing Implicit.}
-\end{quote}
-
-By default the basic pretty-printing rules display the implicit arguments that are not detected as strict implicit arguments. This ``defensive'' mode can quickly make the display cumbersome so this can be deactivated by using the command
-\begin{quote}
-{\tt Unset Printing Implicit Defensive.}
-\end{quote}
-Conversely, to force the display of non strict arguments, use command
-\begin{quote}
-{\tt Set Printing Implicit Defensive.}
-\end{quote}
-
-\SeeAlso {\tt Set Printing All} in Section~\ref{SetPrintingAll}.
-
-\subsection{Interaction with subtyping}
-
-When an implicit argument can be inferred from the type of more than
-one of the other arguments, then only the type of the first of these
-arguments is taken into account, and not an upper type of all of
-them.  As a consequence, the inference of the implicit argument of
-``='' fails in
-\begin{coq_example*}
-Fail Check nat = Prop.
-\end{coq_example*}
-
-but succeeds in
-\begin{coq_example*}
-Check Prop = nat.
-\end{coq_example*}
-
-\subsection{Deactivation of implicit arguments for parsing}
-\optindex{Parsing Explicit}
-
-Use of implicit arguments can be deactivated by issuing the command:
-\begin{quote}
-{\tt Set Parsing Explicit.}
-\end{quote}
-
-In this case, all arguments of constants, inductive types,
-constructors, etc, including the arguments declared as implicit, have
-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 Unset Parsing Explicit.}
-\end{quote}
-
-\subsection{Canonical structures
-\comindex{Canonical Structure}}
-
-A canonical structure is an instance of a record/structure type that
-can be used to solve unification problems involving a projection
-applied to an unknown structure instance (an implicit argument) and
-a value.  The complete documentation of canonical structures can be found
-in Chapter~\ref{CS-full}, here only a simple example is given.
-
-Assume that {\qualid} denotes an object $(Build\_struc~ c_1~ \ldots~ c_n)$ in
-the
-structure {\em struct} of which the fields are $x_1$, ...,
-$x_n$. Assume that {\qualid} is declared as a canonical structure
-using the command
-\begin{quote}
-{\tt Canonical Structure {\qualid}.}
-\end{quote}
-Then, each time an equation of the form $(x_i~
-\_)=_{\beta\delta\iota\zeta}c_i$ has to be solved during the
-type-checking process, {\qualid} is used as a solution. Otherwise
-said, {\qualid} is canonically used to extend the field $c_i$ into a
-complete structure built on $c_i$.
-
-Canonical structures are particularly useful when mixed with
-coercions and strict implicit arguments. Here is an example.
-\begin{coq_example*}
-Require Import Relations.
-Require Import EqNat.
-Set Implicit Arguments.
-Unset Strict Implicit.
-Structure Setoid : Type := 
-  {Carrier :> Set;
-   Equal : relation Carrier;
-   Prf_equiv : equivalence Carrier Equal}.
-Definition is_law (A B:Setoid) (f:A -> B) :=
-  forall x y:A, Equal x y -> Equal (f x) (f y).
-Axiom eq_nat_equiv : equivalence nat eq_nat.
-Definition nat_setoid : Setoid := Build_Setoid eq_nat_equiv.
-Canonical Structure nat_setoid.
-\end{coq_example*}
-
-Thanks to \texttt{nat\_setoid} declared as canonical, the implicit
-arguments {\tt A} and {\tt B} can be synthesized in the next statement.
-\begin{coq_example}
-Lemma is_law_S : is_law S.
-\end{coq_example}
-
-\Rem If a same field occurs in several canonical structure, then
-only the structure declared first as canonical is considered.
-
-\begin{Variants}
-\item {\tt Canonical Structure {\ident} := {\term} : {\type}.}\\
- {\tt Canonical Structure {\ident} := {\term}.}\\
- {\tt Canonical Structure {\ident} : {\type} := {\term}.}
-
-These are equivalent to a regular definition of {\ident} followed by
-the declaration 
-
-{\tt Canonical Structure {\ident}}.
-\end{Variants}
-
-\SeeAlso more examples in user contribution \texttt{category}
-(\texttt{Rocq/ALGEBRA}).
-
-\subsubsection{Print Canonical Projections.
-\comindex{Print Canonical Projections}}
-
-This displays the list of global names that are components of some
-canonical structure. For each of them, the canonical structure of
-which it is a projection is indicated. For instance, the above example 
-gives the following output:
-
-\begin{coq_example}
-Print Canonical Projections.
-\end{coq_example}
-
-\subsection{Implicit types of variables}
-\comindex{Implicit Types}
-
-It is possible to bind variable names to a given type (e.g. in a
-development using arithmetic, it may be convenient to bind the names
-{\tt n} or {\tt m} to the type {\tt nat} of natural numbers). The
-command for that is
-\begin{quote}
-\tt Implicit Types \nelist{\ident}{} : {\type}
-\end{quote}
-The effect of the command is to automatically set the type of bound
-variables starting with {\ident} (either {\ident} itself or
-{\ident} followed by one or more single quotes, underscore or digits)
-to be {\type} (unless the bound variable is already declared with an
-explicit type in which case, this latter type is considered).
-
-\Example
-\begin{coq_example}
-Require Import List.
-Implicit Types m n : nat.
-Lemma cons_inj_nat : forall m n l, n :: l = m :: l -> n = m.
-intros m n.
-Lemma cons_inj_bool : forall (m n:bool) l, n :: l = m :: l -> n = m.
-\end{coq_example}
-
-\begin{Variants}
-\item {\tt Implicit Type {\ident} : {\type}}\\
-This is useful for declaring the implicit type of a single variable.
-\item
- {\tt Implicit Types\,%
-(\,{\ident$_{1,1}$}\ldots{\ident$_{1,k_1}$}\,{\tt :}\,{\term$_1$} {\tt )}\,%
-\ldots\,{\tt (}\,{\ident$_{n,1}$}\ldots{\ident$_{n,k_n}$}\,{\tt :}\,%
-{\term$_n$} {\tt )}.}\\ 
-  Adds $n$ blocks of implicit types with different specifications.
-\end{Variants}
-
-
-\subsection{Implicit generalization
-\label{implicit-generalization}
-\comindex{Generalizable Variables}}
-% \textquoteleft since \` doesn't do what we want
-\index{0genimpl@{\textquoteleft\{\ldots\}}}
-\index{0genexpl@{\textquoteleft(\ldots)}}
-
-Implicit generalization is an automatic elaboration of a statement with
-free variables into a closed statement where these variables are
-quantified explicitly. Implicit generalization is done inside binders
-starting with a \texttt{\`{}} and terms delimited by \texttt{\`{}\{ \}} and
-\texttt{\`{}( )}, always introducing maximally inserted implicit arguments for
-the generalized variables. Inside implicit generalization
-delimiters, free variables in the current context are automatically
-quantified using a product or a lambda abstraction to generate a closed
-term. In the following statement for example, the variables \texttt{n}
-and \texttt{m} are automatically generalized and become explicit
-arguments of the lemma as we are using \texttt{\`{}( )}:
-
-\begin{coq_example}
-Generalizable All Variables.
-Lemma nat_comm : `(n = n + 0).
-\end{coq_example}
-\begin{coq_eval}
-Abort.
-\end{coq_eval}
-One can control the set of generalizable identifiers with the
-\texttt{Generalizable} vernacular command to avoid unexpected
-generalizations when mistyping identifiers. There are three variants of
-the command:
-
-\begin{quote}
-{\tt Generalizable (All|No) Variable(s)? ({\ident$_1$ \ident$_n$})?.}
-\end{quote}
-
-\begin{Variants}
-\item {\tt Generalizable All Variables.} All variables are candidate for 
-  generalization if they appear free in the context under a
-  generalization delimiter. This may result in confusing errors in
-  case of typos. In such cases, the context will probably contain some
-  unexpected generalized variable.
-
-\item {\tt Generalizable No Variables.} Disable implicit generalization 
-  entirely. This is the default behavior.
-
-\item {\tt Generalizable Variable(s)? {\ident$_1$ \ident$_n$}.} 
-  Allow generalization of the given identifiers only. Calling this
-  command multiple times adds to the allowed identifiers.
-
-\item {\tt Global Generalizable} Allows to export the choice of
-  generalizable variables.
-\end{Variants}
-
-One can also use implicit generalization for binders, in which case the
-generalized variables are added as binders and set maximally implicit.
-\begin{coq_example*}
-Definition id `(x : A) : A := x.
-\end{coq_example*}
-\begin{coq_example}
-Print id.
-\end{coq_example}
-
-The generalizing binders \texttt{\`{}\{ \}} and \texttt{\`{}( )} work similarly to
-their explicit counterparts, only binding the generalized variables
-implicitly, as maximally-inserted arguments. In these binders, the
-binding name for the bound object is optional, whereas the type is
-mandatory, dually to regular binders.
-
-\section{Coercions
-\label{Coercions}
-\index{Coercions}}
-
-Coercions can be used to implicitly inject terms from one {\em class} in
-which they reside into another one. A {\em class} is either a sort
-(denoted by the keyword {\tt Sortclass}), a product type (denoted by the
-keyword {\tt Funclass}), or a type constructor (denoted by its name),
-e.g. an inductive type or any constant with a type of the form
-\texttt{forall} $(x_1:A_1) .. (x_n:A_n),~s$ where $s$ is a sort.
-
-Then the user is able to apply an
-object that is not a function, but can be coerced to a function, and
-more generally to consider that a term of type A is of type B provided
-that there is a declared coercion between A and B. The main command is
-\comindex{Coercion}
-\begin{quote}
-\tt Coercion {\qualid} : {\class$_1$} >-> {\class$_2$}.
-\end{quote}
-which declares the construction denoted by {\qualid} as a
-coercion between {\class$_1$} and {\class$_2$}.
-
-More details and examples, and a description of the commands related
-to coercions are provided in Chapter~\ref{Coercions-full}.
-
-\section[Printing constructions in full]{Printing constructions in full\label{SetPrintingAll}
-\optindex{Printing All}}
-
-Coercions, implicit arguments, the type of pattern-matching, but also
-notations (see Chapter~\ref{Addoc-syntax}) can obfuscate the behavior
-of some tactics (typically the tactics applying to occurrences of
-subterms are sensitive to the implicit arguments). The command
-\begin{quote}
-{\tt Set Printing All.}
-\end{quote}
-deactivates all high-level printing features such as coercions,
-implicit arguments, returned type of pattern-matching, notations and
-various syntactic sugar for pattern-matching or record projections.
-Otherwise said, {\tt Set Printing All} includes the effects
-of the commands {\tt Set Printing Implicit}, {\tt Set Printing
-Coercions}, {\tt Set Printing Synth}, {\tt Unset Printing Projections}
-and {\tt Unset Printing Notations}.  To reactivate the high-level
-printing features, use the command
-\begin{quote}
-{\tt Unset Printing All.}
-\end{quote}
-
-\section[Printing universes]{Printing universes\label{PrintingUniverses}
-\optindex{Printing Universes}}
-
-The following command:
-\begin{quote}
-{\tt Set Printing Universes}
-\end{quote}
-activates the display of the actual level of each occurrence of
-{\Type}. See Section~\ref{Sorts} for details.  This wizard option, in
-combination with \texttt{Set Printing All} (see
-section~\ref{SetPrintingAll}) can help to diagnose failures to unify
-terms apparently identical but internally different in the Calculus of
-Inductive Constructions. To reactivate the display of the actual level
-of the occurrences of {\Type}, use
-\begin{quote}
-{\tt Unset Printing Universes.}
-\end{quote}
-
-\comindex{Print Universes}
-\comindex{Print Sorted Universes}
-
-The constraints on the internal level of the occurrences of {\Type}
-(see Section~\ref{Sorts}) can be printed using the command
-\begin{quote}
-{\tt Print \zeroone{Sorted} Universes.}
-\end{quote}
-If the optional {\tt Sorted} option is given, each universe will be
-made equivalent to a numbered label reflecting its level (with a
-linear ordering) in the universe hierarchy.
-
-This command also accepts an optional output filename:
-\begin{quote}
-\tt Print \zeroone{Sorted} Universes {\str}.
-\end{quote}
-If {\str} ends in \texttt{.dot} or \texttt{.gv}, the constraints are
-printed in the DOT language, and can be processed by Graphviz
-tools. The format is unspecified if {\str} doesn't end in
-\texttt{.dot} or \texttt{.gv}.
-
-\section[Existential variables]{Existential variables\label{ExistentialVariables}}
-\label{evars}
-
-Coq terms can include existential variables which
-represents unknown subterms to eventually be replaced by actual
-subterms.
-
-Existential variables are generated in place of unsolvable implicit
-arguments or ``{\tt \_}'' placeholders when using commands such as
-\texttt{Check} (see Section~\ref{Check}) or when using tactics such as
-\texttt{refine}~(see Section~\ref{refine}), as well as in place of unsolvable
-instances when using tactics such that \texttt{eapply} (see
-Section~\ref{eapply}). An existential variable is defined in a
-context, which is the context of variables of the placeholder which
-generated the existential variable, and a type, which is the expected
-type of the placeholder. 
-
-As a consequence of typing constraints, existential variables can be
-duplicated in such a way that they possibly appear in different
-contexts than their defining context. Thus, any occurrence of a given
-existential variable comes with an instance of its original context. In the
-simple case, when an existential variable denotes the placeholder
-which generated it, or is used in the same context as the one in which
-it was generated, the context is not displayed and the existential
-variable is represented by ``?'' followed by an identifier.
-
-\begin{coq_example}
-Parameter identity : forall (X:Set), X -> X.
-Check identity _ _.
-Check identity _ (fun x => _).
-\end{coq_example}
-
-In the general case, when an existential variable ?{\ident}
-appears outside of its context of definition, its instance, written under
-the form \verb!@{id1:=term1; ...; idn:=termn}!, is appending to its
-name, indicating how the variables of its defining context are
-instantiated.  The variables of the context of the existential
-variables which are instantiated by themselves are not written, unless
-the flag {\tt Printing Existential Instances} is on (see
-Section~\ref{SetPrintingExistentialInstances}), and this is why an
-existential variable used in the same context as its context of
-definition is written with no instance.
-
-\begin{coq_example}
-Check (fun x y => _) 0 1.
-Set Printing Existential Instances.
-Check (fun x y => _) 0 1.
-\end{coq_example}
-
-\begin{coq_eval}
-Unset Printing Existential Instances.
-\end{coq_eval}
-
-Existential variables can be named by the user upon creation using
-the syntax {\tt ?[\ident]}. This is useful when the existential
-variable needs to be explicitly handled later in the script (e.g.
-with a named-goal selector, see~\ref{ltac:selector}).
-
-\subsection{Explicit displaying of existential instances for pretty-printing
-\label{SetPrintingExistentialInstances}
-\optindex{Printing Existential Instances}}
-
-The command:
-\begin{quote}
-{\tt Set Printing Existential Instances}
-\end{quote}
-activates the full display of how the context of an existential variable is
-instantiated at each of the occurrences of the existential variable.
-
-To deactivate the full display of the instances of existential
-variables, use
-\begin{quote}
-{\tt Unset Printing Existential Instances.}
-\end{quote}
-
-\subsection{Solving existential variables using tactics}
-\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 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
-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 := ltac:(exact x).
-\end{coq_example*}
-
-This construction is useful when one wants to define complicated terms using
-highly automated tactics without resorting to writing the proof-term by means of
-the interactive proof engine.
-
-This mechanism is comparable to the {\tt Declare Implicit Tactic} command
-defined at~\ref{DeclareImplicit}, except that the used tactic is local to each
-hole instead of being declared globally.
-
-%%% Local Variables: 
-%%% mode: latex
-%%% TeX-master: "Reference-Manual"
-%%% End: 
diff --git a/doc/refman/RefMan-mod.tex b/doc/refman/RefMan-mod.tex
deleted file mode 100644
index b4e270e6c..000000000
--- a/doc/refman/RefMan-mod.tex
+++ /dev/null
@@ -1,428 +0,0 @@
-\section{Module system
-\index{Modules}
-\label{section:Modules}}
-
-The module system provides a way of packaging related elements
-together, as well as a means of massive abstraction.
-
-\begin{figure}[t]
-\begin{centerframe}
-\begin{tabular}{rcl}
-{\modtype}  & ::= & {\qualid} \\
- & $|$ & {\modtype} \texttt{ with Definition }{\qualid} := {\term} \\
- & $|$ & {\modtype} \texttt{ with Module }{\qualid} := {\qualid} \\
- & $|$ & {\qualid} \nelist{\qualid}{}\\
- & $|$ & $!${\qualid} \nelist{\qualid}{}\\
- &&\\
-
-{\onemodbinding}  & ::= & {\tt ( [Import|Export] \nelist{\ident}{} : {\modtype} )}\\
- &&\\
-
-{\modbindings} & ::= & \nelist{\onemodbinding}{}\\
- &&\\
-
-{\modexpr} & ::= & \nelist{\qualid}{} \\
-           & $|$ & $!$\nelist{\qualid}{}
-\end{tabular}
-\end{centerframe}
-\caption{Syntax of modules}
-\end{figure}
-
-In the syntax of module application, the $!$ prefix indicates that
-any {\tt Inline} directive in the type of the functor arguments
-will be ignored (see \ref{Inline} below).
-
-\subsection{\tt Module {\ident}
-\comindex{Module}}
-
-This command is used to start an interactive module named {\ident}.
-
-\begin{Variants}
-
-\item{\tt Module {\ident} {\modbindings}}
-
-  Starts an interactive functor with parameters given by {\modbindings}.
-
-\item{\tt Module {\ident} \verb.:. {\modtype}}
-
-  Starts an interactive module specifying its module type. 
-
-\item{\tt Module {\ident} {\modbindings} \verb.:. {\modtype}}
-
-  Starts an interactive functor with parameters given by
-  {\modbindings}, and output module type {\modtype}.
-
-\item{\tt Module {\ident} \verb.<:. {\modtype$_1$} \verb.<:. $\ldots$ \verb.<:.{ \modtype$_n$}}
-
-  Starts an interactive module satisfying each {\modtype$_i$}. 
-
-\item{\tt Module {\ident} {\modbindings} \verb.<:. {\modtype$_1$} \verb.<:. $\ldots$ \verb.<:. {\modtype$_n$}}
-
-  Starts an interactive functor with parameters given by
-  {\modbindings}. The output module type is verified against each
-  module type {\modtype$_i$}.
-
-\item\texttt{Module [Import|Export]}
-
-  Behaves like \texttt{Module}, but automatically imports or exports
-  the module.
-
-\end{Variants}
-\subsubsection{Reserved commands inside an interactive module:
-\comindex{Include}}
-\begin{enumerate}
-\item {\tt Include {\module}}
-
-  Includes the content of {\module} in the current interactive
- module. Here {\module} can be a module expression or a module type
- expression. If {\module} is a high-order module or module type
- expression then the system tries to instantiate {\module}
- by the current interactive module.
-
-\item {\tt Include {\module$_1$} \verb.<+. $\ldots$ \verb.<+. {\module$_n$}} 
-
-is a shortcut for {\tt Include {\module$_1$}}  $\ldots$ {\tt Include {\module$_n$}}
-\end{enumerate}
-\subsection{\tt End {\ident}
-\comindex{End}}
-
-This command closes the interactive module {\ident}. If the module type
-was given the content of the module is matched against it and an error
-is signaled if the matching fails. If the module is basic (is not a
-functor) its components (constants, inductive types, submodules etc) are
-now available through the dot notation.
-
-\begin{ErrMsgs}
-\item \errindex{No such label {\ident}}
-\item \errindex{Signature components for label {\ident} do not match}
-\item \errindex{This is not the last opened module}
-\end{ErrMsgs}
-
-
-\subsection{\tt Module {\ident} := {\modexpr}
-\comindex{Module}}
-
-This command defines the module identifier {\ident} to be equal to
-{\modexpr}. 
-
-\begin{Variants}
-\item{\tt Module {\ident} {\modbindings} := {\modexpr}}
-
- Defines a functor with parameters given by {\modbindings} and body {\modexpr}.
-
-% Particular cases of the next 2 items
-%\item{\tt Module {\ident} \verb.:. {\modtype} := {\modexpr}}
-%
-%  Defines a module with body {\modexpr} and interface {\modtype}.
-%\item{\tt Module {\ident} \verb.<:. {\modtype} := {\modexpr}}
-%
-%  Defines a module with body {\modexpr}, satisfying {\modtype}.
-
-\item{\tt Module {\ident} {\modbindings} \verb.:. {\modtype} :=
-    {\modexpr}}
-
-  Defines a functor with parameters given by {\modbindings} (possibly none),
-  and output module type {\modtype}, with body {\modexpr}. 
-
-\item{\tt Module {\ident} {\modbindings} \verb.<:.  {\modtype$_1$} \verb.<:. $\ldots$ \verb.<:. {\modtype$_n$}:=
-    {\modexpr}}
-
-  Defines a functor with parameters given by {\modbindings} (possibly none) 
-  with body {\modexpr}. The body is checked against each {\modtype$_i$}.
-
-\item{\tt Module {\ident} {\modbindings} := {\modexpr$_1$} \verb.<+. $\ldots$ \verb.<+. {\modexpr$_n$}}
-
-  is equivalent to an interactive module where each {\modexpr$_i$} are included.
-
-\end{Variants}
-
-\subsection{\tt Module Type {\ident}
-\comindex{Module Type}}
-
-This command is used to start an interactive module type {\ident}.
-
-\begin{Variants}
-
-\item{\tt Module Type {\ident} {\modbindings}}
-
-  Starts an interactive functor type with parameters given by {\modbindings}.
-
-\end{Variants}
-\subsubsection{Reserved commands inside an interactive module type:
-\comindex{Include}\comindex{Inline}}
-\label{Inline}
-\begin{enumerate}
-\item {\tt Include {\module}}
-
- Same as {\tt Include} inside a module.
-
-\item {\tt Include {\module$_1$} \verb.<+. $\ldots$ \verb.<+. {\module$_n$}} 
-
-is a shortcut for {\tt Include {\module$_1$}}  $\ldots$ {\tt Include {\module$_n$}}
-
-\item {\tt {\assumptionkeyword} Inline {\assums} }
-
- The instance of this assumption will be automatically expanded at functor
- application, except when this functor application is prefixed by a $!$ annotation.
-\end{enumerate}
-\subsection{\tt End {\ident}
-\comindex{End}}
-
-This command closes the interactive module type {\ident}.
-
-\begin{ErrMsgs}
-\item \errindex{This is not the last opened module type}
-\end{ErrMsgs}
-
-\subsection{\tt Module Type {\ident} := {\modtype}}
-
-Defines a module type {\ident} equal to {\modtype}.
-
-\begin{Variants}
-\item {\tt Module Type {\ident} {\modbindings} := {\modtype}}
-
-  Defines a functor type {\ident} specifying functors taking arguments
-  {\modbindings} and returning {\modtype}.
-
-\item{\tt Module Type {\ident} {\modbindings} := {\modtype$_1$} \verb.<+. $\ldots$ \verb.<+. {\modtype$_n$}}
-
-  is equivalent to an interactive module type were each {\modtype$_i$} are included.
-
-\end{Variants}
-
-\subsection{\tt Declare Module {\ident} : {\modtype}
-\comindex{Declare Module}}
-
-Declares a module {\ident} of type {\modtype}.
-
-\begin{Variants}
-
-\item{\tt Declare Module {\ident} {\modbindings} \verb.:. {\modtype}}
-
-  Declares a functor with parameters {\modbindings} and output module
-  type {\modtype}.
-
-
-\end{Variants}
-
-
-\subsubsection{Example}
-
-Let us define a simple module.
-\begin{coq_example}
-Module M.
-  Definition T := nat.
-  Definition x := 0.
-  Definition y : bool.
-    exact true.
-  Defined.
-End M.
-\end{coq_example}
-Inside a module one can define constants, prove theorems and do any
-other things that can be done in the toplevel. Components of a closed
-module can be accessed using the dot notation:
-\begin{coq_example}
-Print M.x.
-\end{coq_example}
-A simple module type:
-\begin{coq_example}
-Module Type SIG.
-  Parameter T : Set.
-  Parameter x : T.
-End SIG.
-\end{coq_example}
-
-Now we can create a new module from \texttt{M}, giving it a less
-precise specification: the \texttt{y} component is dropped as well
-as the body of \texttt{x}.
-
-\begin{coq_eval}
-Set Printing Depth 50.
-\end{coq_eval}
-% (********** The following is not correct and should produce **********)
-% (***************** Error: N.y not a defined object *******************)
-\begin{coq_example}
-Module N  :  SIG with Definition T := nat  :=  M.
-Print N.T.
-Print N.x.
-Fail Print N.y.
-\end{coq_example}
-\begin{coq_eval}
-Reset N.
-\end{coq_eval}
-
-\noindent
-The definition of \texttt{N} using the module type expression
-\texttt{SIG with Definition T:=nat} is equivalent to the following
-one:
-
-\begin{coq_example*}
-Module Type SIG'.
-  Definition T : Set := nat.
-  Parameter x : T.
-End SIG'.
-Module N : SIG' := M.
-\end{coq_example*}
-If we just want to be sure that the our implementation satisfies a
-given module type without restricting the interface, we can use a
-transparent constraint
-\begin{coq_example}
-Module P <: SIG := M.
-Print P.y.
-\end{coq_example}
-Now let us create a functor, i.e. a parametric module
-\begin{coq_example}
-Module Two (X Y: SIG).
-\end{coq_example}
-\begin{coq_example*}
-  Definition T := (X.T * Y.T)%type.
-  Definition x := (X.x, Y.x).
-\end{coq_example*}
-\begin{coq_example}
-End Two.
-\end{coq_example}
-and apply it to our modules and do some computations
-\begin{coq_example}
-Module Q := Two M N.
-Eval compute in (fst Q.x + snd Q.x).
-\end{coq_example}
-In the end, let us define a module type with two sub-modules, sharing
-some of the fields and give one of its possible implementations:
-\begin{coq_example}
-Module Type SIG2.
-  Declare Module M1 : SIG.
-  Module M2 <: SIG.
-    Definition T := M1.T.
-    Parameter x : T.
-  End M2.
-End SIG2.
-\end{coq_example}
-\begin{coq_example*}
-Module Mod <: SIG2.
-  Module M1.
-    Definition T := nat.
-    Definition x := 1.
-  End M1.
-  Module M2 := M.
-\end{coq_example*}
-\begin{coq_example}
-End Mod.
-\end{coq_example}
-Notice that \texttt{M} is a correct body for the component \texttt{M2}
-since its \texttt{T} component is equal \texttt{nat} and hence
-\texttt{M1.T} as specified.
-\begin{coq_eval}
-Reset Initial.
-\end{coq_eval}
-
-\begin{Remarks}
-\item Modules and module types can be nested components of each other.
-\item One can have sections inside a module or a module type, but
-  not a module or a module type inside a section.
-\item Commands like \texttt{Hint} or \texttt{Notation} can
-  also appear inside modules and module types. Note that in case of a
-  module definition like:
-
-    \smallskip
-    \noindent
-    {\tt Module N : SIG := M.} 
-    \smallskip
-
-    or
-
-    \smallskip
-    {\tt Module N : SIG.\\
-      \ \ \dots\\
-      End N.}
-    \smallskip 
-    
-    hints and the like valid for \texttt{N} are not those defined in
-    \texttt{M} (or the module body) but the ones defined in
-    \texttt{SIG}.
-
-\end{Remarks}
-
-\subsection{\tt Import {\qualid}
-\comindex{Import}
-\label{Import}}
-
-If {\qualid} denotes a valid basic module (i.e. its module type is a
-signature), makes its components available by their short names.
-
-Example:
-
-\begin{coq_example}
-Module Mod.
-  Definition T:=nat.
-  Check T.
-End Mod.
-Check Mod.T.
-Fail Check T. (* Incorrect! *)
-Import Mod.
-Check T. (* Now correct *)
-\end{coq_example}
-\begin{coq_eval}
-Reset Mod.
-\end{coq_eval}
-
-Some features defined in modules are activated only when a module is
-imported. This is for instance the case of notations (see
-Section~\ref{Notation}).
-
-Declarations made with the {\tt Local} flag are never imported by the
-{\tt Import} command. Such declarations are only accessible through their
-fully qualified name.
-
-Example:
-
-\begin{coq_example}
-Module A.
-Module B.
-Local Definition T := nat.
-End B.
-End A.
-Import A.
-Fail Check B.T.
-\end{coq_example}
-
-\begin{Variants}
-\item{\tt Export {\qualid}}\comindex{Export}
-
-  When the module containing the command {\tt Export {\qualid}} is
-  imported, {\qualid} is imported as well.
-\end{Variants}
-
-\begin{ErrMsgs}
-  \item \errindexbis{{\qualid} is not a module}{is not a module}
-% this error is impossible in the import command
-%  \item \errindex{Cannot mask the absolute name {\qualid} !}
-\end{ErrMsgs}
-
-\begin{Warnings}
-  \item Trying to mask the absolute name {\qualid} !
-\end{Warnings}
-
-\subsection{\tt Print Module {\ident}
-\comindex{Print Module} \optindex{Short Module Printing}}
-
-Prints the module type and (optionally) the body of the module {\ident}.
-
-For this command and {\tt Print Module Type}, the option {\tt Short
-  Module Printing} (off by default) disables the printing of the types of fields,
-leaving only their names.
-
-\subsection{\tt Print Module Type {\ident}
-\comindex{Print Module Type}}
-
-Prints the module type corresponding to {\ident}.
-
-\subsection{\tt Locate Module {\qualid}
-\comindex{Locate Module}}
-
-Prints the full name of the module {\qualid}.
-
-
-%%% Local Variables: 
-%%% mode: latex
-%%% TeX-master: "Reference-Manual"
-%%% End: 
diff --git a/doc/refman/Reference-Manual.tex b/doc/refman/Reference-Manual.tex
index 4935b70c5..c7a98fce4 100644
--- a/doc/refman/Reference-Manual.tex
+++ b/doc/refman/Reference-Manual.tex
@@ -95,7 +95,6 @@ Options A and B of the licence are {\em not} elected.}
 \defaultheaders
 %END LATEX
 \include{RefMan-gal.v}% Gallina
-\include{RefMan-ext.v}% Gallina extensions
 \include{RefMan-lib.v}% The coq library
 \include{RefMan-cic.v}% The Calculus of Constructions
 \include{RefMan-modr}% The module system
diff --git a/doc/sphinx/index.rst b/doc/sphinx/index.rst
index f5a57b9dd..f2e444c0c 100644
--- a/doc/sphinx/index.rst
+++ b/doc/sphinx/index.rst
@@ -16,6 +16,8 @@ Table of contents
 .. toctree::
    :caption: The language
 
+   language/gallina-extensions
+
 .. toctree::
    :caption: The proof engine
 
diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst
new file mode 100644
index 000000000..d618d90ad
--- /dev/null
+++ b/doc/sphinx/language/gallina-extensions.rst
@@ -0,0 +1,2356 @@
+.. include:: ../replaces.rst
+
+.. _extensionsofgallina:
+
+Extensions of |Gallina|
+=======================
+
+|Gallina| is the kernel language of |Coq|. We describe here extensions of
+|Gallina|’s syntax.
+
+.. _record-types:
+
+Record types
+----------------
+
+The ``Record`` construction is a macro allowing the definition of
+records as is done in many programming languages. Its syntax is
+described in the grammar below. In fact, the ``Record`` macro is more general
+than the usual record types, since it allows also for “manifest”
+expressions. In this sense, the ``Record`` construction allows defining
+“signatures”.
+
+.. _record_grammar:
+
+  .. productionlist:: `sentence`
+     record         : `record_keyword` ident [binders] [: sort] := [ident] { [`field` ; … ; `field`] }.
+     record_keyword : Record | Inductive | CoInductive
+     field          : name [binders] : type [ where notation ]
+                    : | name [binders] [: term] := term
+
+In the expression:
+
+.. cmd:: Record @ident {* @param } {? : @sort} := {? @ident} { {*; @ident {* @binder } : @term } }.
+
+the first identifier `ident` is the name of the defined record and `sort` is its
+type. The optional identifier following ``:=`` is the name of its constructor. If it is omitted,
+the default name ``Build_``\ `ident`, where `ident` is the record name, is used. If `sort` is
+omitted, the default sort is `\Type`. The identifiers inside the brackets are the names of
+fields. For a given field `ident`, its type is :g:`forall binder …, term`.
+Remark that the type of a particular identifier may depend on a previously-given identifier. Thus the
+order of the fields is important. Finally, each `param` is a parameter of the record.
+
+More generally, a record may have explicitly defined (a.k.a. manifest)
+fields. For instance, we might have::
+
+  Record ident param : sort := { ident₁ : type₁ ; ident₂ := term₂ ; ident₃ : type₃ }.
+
+in which case the correctness of |type_3| may rely on the instance |term_2| of |ident_2| and |term_2| in turn
+may depend on |ident_1|.
+
+.. example::
+
+  .. coqtop:: reset all
+
+     Record Rat : Set := mkRat
+     {sign : bool;
+     top : nat;
+     bottom : nat;
+     Rat_bottom_cond : 0 <> bottom;
+     Rat_irred_cond :
+     forall x y z:nat, (x * y) = top /\ (x * z) = bottom -> x = 1}.
+
+Remark here that the fields ``Rat_bottom_cond`` depends on the field ``bottom`` and ``Rat_irred_cond``
+depends on both ``top`` and ``bottom``.
+
+Let us now see the work done by the ``Record`` macro. First the macro
+generates a variant type definition with just one constructor:
+
+.. cmd:: Variant @ident {* @params} : @sort := @ident {* (@ident : @term_1)}.
+
+To build an object of type `ident`, one should provide the constructor
+|ident_0| with the appropriate number of terms filling the fields of the record.
+
+.. example:: Let us define the rational :math:`1/2`:
+
+    .. coqtop:: in
+
+       Theorem one_two_irred : forall x y z:nat, x * y = 1 /\ x * z = 2 -> x = 1.
+       Admitted.
+
+       Definition half := mkRat true 1 2 (O_S 1) one_two_irred.
+       Check half.
+
+.. _record-named-fields-grammar:
+
+  .. productionlist::
+    term : {| [`field_def` ; … ; `field_def`] |}
+    field_def : name [binders] := `term`
+
+Alternatively, the following syntax allows creating objects by using named fields, as
+shown in this grammar. The fields do not have to be in any particular order, nor do they have
+to be all present if the missing ones can be inferred or prompted for
+(see :ref:`programs`).
+
+.. coqtop:: all
+
+  Definition half' :=
+    {| sign := true;
+       Rat_bottom_cond := O_S 1;
+       Rat_irred_cond := one_two_irred |}.
+
+This syntax can be disabled globally for printing by
+
+.. cmd:: Unset Printing Records.
+
+For a given type, one can override this using either
+
+.. cmd:: Add Printing Record @ident.
+
+to get record syntax or
+
+.. cmd:: Add Printing Constructor @ident.
+
+to get constructor syntax.
+
+This syntax can also be used for pattern matching.
+
+.. coqtop:: all
+
+   Eval compute in (
+     match half with
+     | {| sign := true; top := n |} => n
+     | _ => 0
+     end).
+
+The macro generates also, when it is possible, the projection
+functions for destructuring an object of type `\ident`.  These
+projection functions are given the names of the corresponding
+fields. If a field is named `_` then no projection is built
+for it. In our example:
+
+.. coqtop:: all
+
+  Eval compute in top half.
+  Eval compute in bottom half.
+  Eval compute in Rat_bottom_cond half.
+
+An alternative syntax for projections based on a dot notation is
+available:
+
+.. coqtop:: all
+
+   Eval compute in half.(top).
+
+It can be activated for printing with
+
+.. cmd:: Set Printing Projections.
+
+.. example::
+
+    .. coqtop:: all
+
+       Set Printing Projections.
+       Check top half.
+
+.. _record_projections_grammar:
+
+  .. productionlist:: terms
+     term : term `.` ( qualid )
+          : | term `.` ( qualid arg … arg )
+          : | term `.` ( @`qualid` `term` … `term` )
+
+  Syntax of Record projections
+
+The corresponding grammar rules are given in the preceding grammar. When `qualid`
+denotes a projection, the syntax `term.(qualid)` is equivalent to `qualid term`,
+the syntax `term.(qualid` |arg_1| |arg_n| `)` to `qualid` |arg_1| `…` |arg_n| `term`,
+and the syntax `term.(@qualid` |term_1| |term_n| `)` to `@qualid` |term_1| `…` |term_n| `term`.
+In each case, `term` is the object projected and the
+other arguments are the parameters of the inductive type.
+
+.. note::. Records defined with the ``Record`` keyword are not allowed to be
+   recursive (references to the record's name in the type of its field
+   raises an  error). To define recursive records, one can use the ``Inductive``
+   and ``CoInductive`` keywords, resulting in an inductive or co-inductive record.
+   A *caveat*, however, is that records cannot appear in mutually inductive
+   (or co-inductive) definitions.
+
+.. note:: Induction schemes are automatically generated for inductive records.
+   Automatic generation of induction schemes for non-recursive records
+   defined with the ``Record`` keyword can be activated with the
+   ``Nonrecursive Elimination Schemes`` option (see :ref:`TODO-13.1.1-nonrecursive-elimination-schemes`).
+
+.. note::``Structure`` is a synonym of the keyword ``Record``.
+
+.. warn:: @ident cannot be defined.
+
+  It can happen that the definition of a projection is impossible.
+  This message is followed by an explanation of this impossibility.
+  There may be three reasons:
+
+  #. The name `ident` already exists in the environment (see Section :ref:`TODO-1.3.1-axioms`).
+  #. The body of `ident` uses an incorrect elimination for
+     `ident` (see Sections :ref:`TODO-1.3.4-fixpoint` and :ref:`TODO-4.5.3-case-expr`).
+  #. The type of the projections `ident` depends on previous
+     projections which themselves could not be defined.
+
+.. exn:: Records declared with the keyword Record or Structure cannot be recursive.
+
+    The record name `ident` appears in the type of its fields, but uses
+    the keyword ``Record``. Use  the keyword ``Inductive`` or ``CoInductive`` instead.
+
+.. exn:: Cannot handle mutually (co)inductive records.
+
+    Records  cannot  be  defined  as  part  of  mutually  inductive  (or
+    co-inductive) definitions,  whether with records only  or mixed with
+    standard definitions.
+
+During the definition of the one-constructor inductive definition, all
+the errors of inductive definitions, as described in Section
+:ref:`TODO-1.3.3-inductive-definitions`, may also occur.
+
+**See also** Coercions and records in Section :ref:`TODO-18.9-coercions-and-records` of the chapter devoted to coercions.
+
+.. _primitive_projections:
+
+Primitive Projections
+~~~~~~~~~~~~~~~~~~~~~
+
+The option ``Set Primitive Projections`` turns on the use of primitive
+projections when defining subsequent records (even through the ``Inductive``
+and ``CoInductive`` commands). Primitive projections
+extended the Calculus of Inductive Constructions with a new binary
+term constructor `r.(p)` representing a primitive projection `p` applied
+to a record object `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 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 ``Printing Primitive Projection Parameters``
+flag. Another compatibility printing can be activated thanks to the
+``Printing Primitive Projection Compatibility`` option which governs the
+printing of pattern-matching over primitive records.
+
+Primitive Record Types
+++++++++++++++++++++++
+
+When the ``Set Primitive Projections`` option is on, definitions of
+record types change meaning. When a type is declared with primitive
+projections, its :g:`match` construct is disabled (see :ref:`primitive_projections` though).
+To eliminate the (co-)inductive type, one must use its defined primitive projections.
+
+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
+``Printing Primitive Projection Parameters`` flag. Further compatibility
+printing can be deactivated thanks to the ``Printing Primitive Projection
+Compatibility`` option which governs the printing of pattern-matching
+over primitive records.
+
+There are currently two ways to introduce primitive records types:
+
+#. Through the ``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:
+   `r` ``= Build_``\ `R` ``(``\ `r`\ ``.(``\ |p_1|\ ``) …`` `r`\ ``.(``\ |p_n|\ ``))``.
+   Eta-conversion allows to define dependent elimination for these types as well.
+#. Through the ``Inductive`` and ``CoInductive`` commands, when
+   the body of the definition is a record declaration of the form
+   ``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.
+
+Reduction
++++++++++
+
+The basic reduction rule of a primitive projection is
+|p_i| ``(Build_``\ `R` |t_1| … |t_n|\ ``)`` :math:`{\rightarrow_{\iota}}` |t_i|.
+However, to take the :math:`{\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 ``simpl`` flags of the ``Arguments`` command in particular.
+There is currently no way to input unfolded primitive projections at the
+user-level, and one must use the ``Printing Primitive Projection Compatibility``
+to display unfolded primitive projections as matches and distinguish them from folded ones.
+
+
+Compatibility Projections and :g:`match`
+++++++++++++++++++++++++++++++++++++++++
+
+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 ``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 :g:`match` constructs on primitive records
+are desugared into substitution of the projections, they cannot be
+printed back as :g:`match` constructs.
+
+Variants and extensions of :g:`match`
+-------------------------------------
+
+.. _extended pattern-matching:
+
+Multiple and nested pattern-matching
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+The basic version of :g:`match` allows pattern-matching on simple
+patterns. As an extension, multiple nested patterns or disjunction of
+patterns are allowed, as in ML-like languages.
+
+The extension just acts as a macro that is expanded during parsing
+into a sequence of match on simple patterns. Especially, a
+construction defined using the extended match is generally printed
+under its expanded form (see ``Set Printing Matching`` in :ref:`controlling-match-pp`).
+
+See also: :ref:`extended pattern-matching`.
+
+
+Pattern-matching on boolean values: the if expression
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+For inductive types with exactly two constructors and for pattern-matching
+expressions that do not depend on the arguments of the constructors, it is possible
+to use a ``if … then … else`` notation. For instance, the definition
+
+.. coqtop:: all
+
+   Definition not (b:bool) :=
+   match b with
+   | true => false
+   | false => true
+   end.
+
+can be alternatively written
+
+.. coqtop:: reset all
+
+   Definition not (b:bool) := if b then false else true.
+
+More generally, for an inductive type with constructors |C_1| and |C_2|,
+we have the following equivalence
+
+::
+
+  if term [dep_ret_type] then term₁ else term₂ ≡
+  match term [dep_ret_type] with
+  | C₁ _ … _ => term₁
+  | C₂ _ … _ => term₂
+  end
+
+.. example::
+
+  .. coqtop:: all
+
+     Check (fun x (H:{x=0}+{x<>0}) =>
+     match H with
+     | left _ => true
+     | right _ => false
+     end).
+
+Notice that the printing uses the :g:`if` syntax because `sumbool` is
+declared as such (see :ref:`controlling-match-pp`).
+
+
+Irrefutable patterns: the destructuring let variants
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+Pattern-matching on terms inhabiting inductive type having only one
+constructor can be alternatively written using :g:`let … in …`
+constructions. There are two variants of them.
+
+
+First destructuring let syntax
+++++++++++++++++++++++++++++++
+
+The expression :g:`let (`\ |ident_1|:g:`, … ,` |ident_n|\ :g:`) :=` |term_0|\ :g:`in` |term_1| performs
+case analysis on |term_0| which must be in an inductive type with one
+constructor having itself :math:`n` arguments. Variables |ident_1| … |ident_n| are
+bound to the :math:`n` arguments of the constructor in expression |term_1|. For
+instance, the definition
+
+.. coqtop:: reset all
+
+   Definition fst (A B:Set) (H:A * B) := match H with
+   | pair x y => x
+   end.
+
+can be alternatively written
+
+.. coqtop:: reset all
+
+   Definition fst (A B:Set) (p:A * B) := let (x, _) := p in x.
+
+Notice that reduction is different from regular :g:`let … in …`
+construction since it happens only if |term_0| is in constructor form.
+Otherwise, the reduction is blocked.
+
+The pretty-printing of a definition by matching on a irrefutable
+pattern can either be done using :g:`match` or the :g:`let` construction
+(see Section :ref:`controlling-match-pp`).
+
+If term inhabits an inductive type with one constructor `C`, we have an
+equivalence between
+
+::
+
+   let (ident₁, …, identₙ) [dep_ret_type] := term in term'
+
+and
+
+::
+
+   match term [dep_ret_type] with
+   C ident₁ … identₙ => term'
+   end
+
+
+Second destructuring let syntax
++++++++++++++++++++++++++++++++
+
+Another destructuring let syntax is available for inductive types with
+one constructor by giving an arbitrary pattern instead of just a tuple
+for all the arguments. For example, the preceding example can be
+written:
+
+.. coqtop:: reset all
+
+   Definition fst (A B:Set) (p:A*B) := let 'pair x _ := p in x.
+
+This is useful to match deeper inside tuples and also to use notations
+for the pattern, as the syntax :g:`let ’p := t in b` allows arbitrary
+patterns to do the deconstruction. For example:
+
+.. coqtop:: all
+
+   Definition deep_tuple (A:Set) (x:(A*A)*(A*A)) : A*A*A*A :=
+   let '((a,b), (c, d)) := x in (a,b,c,d).
+
+   Notation " x 'With' p " := (exist _ x p) (at level 20).
+
+   Definition proj1_sig' (A:Set) (P:A->Prop) (t:{ x:A | P x }) : A :=
+   let 'x With p := t in x.
+
+When printing definitions which are written using this construct it
+takes precedence over let printing directives for the datatype under
+consideration (see Section :ref:`controlling-match-pp`).
+
+
+.. _controlling-match-pp:
+
+Controlling pretty-printing of match expressions
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+The following commands give some control over the pretty-printing
+of :g:`match` expressions.
+
+Printing nested patterns
++++++++++++++++++++++++++
+
+The Calculus of Inductive Constructions knows pattern-matching only
+over simple patterns. It is however convenient to re-factorize nested
+pattern-matching into a single pattern-matching over a nested
+pattern. |Coq|’s printer tries to do such limited re-factorization.
+
+.. cmd:: Set Printing Matching.
+
+This tells |Coq| to try to use nested patterns. This is the default
+behavior.
+
+.. cmd:: Unset Printing Matching.
+
+This tells |Coq| to print only simple pattern-matching problems in the
+same way as the |Coq| kernel handles them.
+
+.. cmd:: Test Printing Matching.
+
+This tells if the printing matching mode is on or off. The default is
+on.
+
+Factorization of clauses with same right-hand side
+++++++++++++++++++++++++++++++++++++++++++++++++++
+
+When several patterns share the same right-hand side, it is additionally
+possible to share the clauses using disjunctive patterns. Assuming that the
+printing matching mode is on, whether |Coq|'s printer shall try to do this kind
+of factorization is governed by the following commands:
+
+.. cmd:: Set Printing Factorizable Match Patterns.
+
+This tells |Coq|'s printer to try to use disjunctive patterns. This is the
+default behavior.
+
+.. cmd:: Unset Printing Factorizable Match Patterns.
+
+This tells |Coq|'s printer not to try to use disjunctive patterns.
+
+.. cmd:: Test Printing Factorizable Match Patterns.
+
+This tells if the factorization of clauses with same right-hand side is on or
+off.
+
+Use of a default clause
++++++++++++++++++++++++
+
+When several patterns share the same right-hand side which do not depend on the
+arguments of the patterns, yet an extra factorization is possible: the
+disjunction of patterns can be replaced with a `_` default clause. Assuming that
+the printing matching mode and the factorization mode are on, whether |Coq|'s
+printer shall try to use a default clause is governed by the following commands:
+
+.. cmd:: Set Printing Allow Default Clause.
+
+This tells |Coq|'s printer to use a default clause when relevant. This is the
+default behavior.
+
+.. cmd:: Unset Printing Allow Default Clause.
+
+This tells |Coq|'s printer not to use a default clause.
+         
+.. cmd:: Test Printing Allow Default Clause.
+
+This tells if the use of a default clause is allowed.
+
+Printing of wildcard patterns
+++++++++++++++++++++++++++++++
+
+Some variables in a pattern may not occur in the right-hand side of
+the pattern-matching clause. There are options to control the display
+of these variables.
+
+.. cmd:: Set Printing Wildcard.
+
+The variables having no occurrences in the right-hand side of the
+pattern-matching clause are just printed using the wildcard symbol
+“_”.
+
+.. cmd:: Unset Printing Wildcard.
+
+The variables, even useless, are printed using their usual name. But
+some non-dependent variables have no name. These ones are still
+printed using a “_”.
+
+.. cmd:: Test Printing Wildcard.
+
+This tells if the wildcard printing mode is on or off. The default is
+to print wildcard for useless variables.
+
+
+Printing of the elimination predicate
++++++++++++++++++++++++++++++++++++++
+
+In most of the cases, the type of the result of a matched term is
+mechanically synthesizable. Especially, if the result type does not
+depend of the matched term.
+
+.. cmd:: Set Printing Synth.
+
+The result type is not printed when |Coq| knows that it can re-
+synthesize it.
+
+.. cmd:: Unset Printing Synth.
+
+This forces the result type to be always printed.
+
+.. cmd:: Test Printing Synth.
+
+This tells if the non-printing of synthesizable types is on or off.
+The default is to not print synthesizable types.
+
+
+Printing matching on irrefutable patterns
+++++++++++++++++++++++++++++++++++++++++++
+
+If an inductive type has just one constructor, pattern-matching can be
+written using the first destructuring let syntax.
+
+.. cmd:: Add Printing Let @ident.
+
+   This adds `ident` to the list of inductive types for which pattern-matching
+   is written using a let expression.
+
+.. cmd:: Remove Printing Let @ident.
+
+   This removes ident from this list. Note that removing an inductive
+   type from this list has an impact only for pattern-matching written
+   using :g:`match`. Pattern-matching explicitly written using a destructuring
+   :g:`let` are not impacted.
+
+.. cmd:: Test Printing Let for @ident.
+
+   This tells if `ident` belongs to the list.
+
+.. cmd:: Print Table Printing Let.
+
+   This prints the list of inductive types for which pattern-matching is
+   written using a let expression.
+
+   The list of inductive types for which pattern-matching is written
+   using a :g:`let` expression is managed synchronously. This means that it is
+   sensitive to the command ``Reset``.
+
+
+Printing matching on booleans
++++++++++++++++++++++++++++++
+
+If an inductive type is isomorphic to the boolean type, pattern-matching
+can be written using ``if`` … ``then`` … ``else`` …:
+
+.. cmd:: Add Printing If @ident.
+
+   This adds ident to the list of inductive types for which pattern-matching is
+   written using an if expression.
+
+.. cmd:: Remove Printing If @ident.
+
+   This removes ident from this list.
+
+.. cmd:: Test Printing If for @ident.
+
+   This tells if ident belongs to the list.
+
+.. cmd:: Print Table Printing If.
+
+   This prints the list of inductive types for which pattern-matching is
+   written using an if expression.
+
+The list of inductive types for which pattern-matching is written
+using an ``if`` expression is managed synchronously. This means that it is
+sensitive to the command ``Reset``.
+
+This example emphasizes what the printing options offer.
+
+.. example::
+
+     .. coqtop:: all
+
+       Definition snd (A B:Set) (H:A * B) := match H with
+       | pair x y => y
+       end.
+
+       Test Printing Let for prod.
+
+       Print snd.
+
+       Remove Printing Let prod.
+
+       Unset Printing Synth.
+
+       Unset Printing Wildcard.
+
+       Print snd.
+
+.. _advanced-recursive-functions:
+       
+Advanced recursive functions
+----------------------------
+
+The following experimental command is available when the ``FunInd`` library has been loaded via ``Require Import FunInd``:
+
+.. cmd:: Function @ident {* @binder} { @decrease_annot } : @type := @term.
+
+This command can be seen as a generalization of ``Fixpoint``. It is actually a wrapper
+for several ways of defining a function *and other useful related
+objects*, namely: an induction principle that reflects the recursive
+structure of the function (see Section :ref:`TODO-8.5.5-functional-induction`) and its fixpoint equality.
+The meaning of this declaration is to define a function ident,
+similarly to ``Fixpoint`. Like in ``Fixpoint``, the decreasing argument must
+be given (unless the function is not recursive), but it might not
+necessarily be *structurally* decreasing. The point of the {} annotation
+is to name the decreasing argument *and* to describe which kind of
+decreasing criteria must be used to ensure termination of recursive
+calls.
+
+The ``Function`` construction also enjoys the ``with`` extension to define
+mutually recursive definitions. However, this feature does not work
+for non structurally recursive functions.
+
+See the documentation of functional induction (:ref:`TODO-8.5.5-functional-induction`)
+and ``Functional Scheme`` (:ref:`TODO-13.2-functional-scheme`) for how to use
+the induction principle to easily reason about the function.
+
+Remark: To obtain the right principle, it is better to put rigid
+parameters of the function as first arguments. For example it is
+better to define plus like this:
+
+.. coqtop:: reset none
+
+   Require Import FunInd.
+
+.. coqtop:: all
+
+   Function plus (m n : nat) {struct n} : nat :=
+   match n with
+   | 0 => m
+   | S p => S (plus m p)
+   end.
+
+than like this:
+
+.. coqtop:: reset all
+
+   Function plus (n m : nat) {struct n} : nat :=
+   match n with
+   | 0 => m
+   | S p => S (plus p m)
+   end.
+
+
+*Limitations*
+
+|term_0| must be built as a *pure pattern-matching tree* (:g:`match … with`)
+with applications only *at the end* of each branch.
+
+Function does not support partial application of the function being
+defined. Thus, the following example cannot be accepted due to the
+presence of partial application of `wrong` in the body of
+`wrong` :
+
+.. coqtop:: all
+
+   Fail Function wrong (C:nat) : nat :=
+   List.hd 0 (List.map wrong (C::nil)).
+
+For now, dependent cases are not treated for non structurally
+terminating functions.
+
+.. exn:: The recursive argument must be specified
+.. exn:: No argument name @ident
+.. exn:: Cannot use mutual definition with well-founded recursion or measure
+
+.. warn:: Cannot define graph for @ident
+
+    The generation of the graph relation (`R_ident`) used to compute the induction scheme of ident
+    raised a typing error. Only `ident` is defined; the induction scheme
+    will not be generated. This error happens generally when:
+
+    - the definition uses pattern matching on dependent types,
+      which ``Function`` cannot deal with yet.
+    - the definition is not a *pattern-matching tree* as explained above.
+
+.. warn:: Cannot define principle(s) for @ident
+
+     The generation of the graph relation (`R_ident`) succeeded but the induction principle
+     could not be built. Only `ident` is defined. Please report.
+
+.. warn:: Cannot build functional inversion principle
+
+     `functional inversion` will not be available for the function.
+
+See also: :ref:`TODO-13.2-generating-ind-principles` and ref:`TODO-8.5.5-functional-induction`
+
+Depending on the ``{…}`` annotation, different definition mechanisms are
+used by ``Function``. A more precise description is given below.
+
+.. cmdv:: Function @ident {* @binder } : @type := @term
+
+   Defines the not recursive function `ident` as if declared with `Definition`. Moreover
+   the following are defined:
+
+    + `ident_rect`, `ident_rec` and `ident_ind`, which reflect the pattern
+      matching structure of `term` (see the documentation of :ref:`TODO-1.3.3-Inductive`);
+    + The inductive `R_ident` corresponding to the graph of `ident` (silently);
+    + `ident_complete` and `ident_correct` which are inversion information
+      linking the function and its graph.
+
+.. cmdv:: Function @ident {* @binder } { struct @ident } : @type := @term
+
+   Defines the structural recursive function `ident` as if declared with ``Fixpoint``. Moreover the following are defined:
+
+    + The same objects as above;
+    + The fixpoint equation of `ident`: `ident_equation`.
+
+.. cmdv:: Function @ident {* @binder } { measure @term @ident } : @type := @term
+.. cmdv:: Function @ident {* @binder } { wf @term @ident } : @type := @term
+
+   Defines a recursive function by well-founded recursion. The module ``Recdef``
+   of the standard library must be loaded for this feature. The ``{}``
+   annotation is mandatory and must be one of the following:
+
+    + ``{measure`` `term` `ident` ``}`` with `ident` being the decreasing argument
+      and `term` being a function from type of `ident` to ``nat`` for which
+      value on the decreasing argument decreases (for the ``lt`` order on ``nat``)
+      at each recursive call of `term`. Parameters of the function are
+      bound in `term`\ ;
+    + ``{wf`` `term` `ident` ``}`` with `ident` being the decreasing argument and
+      `term` an ordering relation on the type of `ident` (i.e. of type
+      `T`\ :math:`_{\sf ident}` → `T`\ :math:`_{\sf ident}` → ``Prop``) for which the decreasing argument
+      decreases at each recursive call of `term`. The order must be well-founded.
+      Parameters of the function are bound in `term`.
+
+   Depending on the annotation, the user is left with some proof
+   obligations that will be used to define the function. These proofs
+   are: proofs that each recursive call is actually decreasing with
+   respect to the given criteria, and (if the criteria is `wf`) a proof
+   that the ordering relation is well-founded. Once proof obligations are
+   discharged, the following objects are defined:
+
+     + The same objects as with the struct;
+     + The lemma `ident`\ :math:`_{\sf tcc}` which collects all proof obligations in one
+       property;
+     + The lemmas `ident`\ :math:`_{\sf terminate}` and `ident`\ :math:`_{\sf F}` which is needed to be inlined
+       during extraction of ident.
+
+   The way this recursive function is defined is the subject of several
+   papers by Yves Bertot and Antonia Balaa on the one hand, and Gilles
+   Barthe, Julien Forest, David Pichardie, and Vlad Rusu on the other
+   hand. Remark: Proof obligations are presented as several subgoals
+   belonging to a Lemma `ident`\ :math:`_{\sf tcc}`.
+
+
+Section mechanism
+-----------------
+
+The sectioning mechanism can be used to to organize a proof in
+structured sections. Then local declarations become available (see
+Section :ref:`TODO-1.3.2-Definitions`).
+
+
+.. cmd:: Section @ident.
+
+   This command is used to open a section named `ident`.
+
+
+.. cmd:: End @ident.
+
+    This command closes the section named `ident`. After closing of the
+    section, the local declarations (variables and local definitions) get
+    *discharged*, meaning that they stop being visible and that all global
+    objects defined in the section are generalized with respect to the
+    variables and local definitions they each depended on in the section.
+
+    .. example::
+
+        .. coqtop:: all
+
+           Section s1.
+
+           Variables x y : nat.
+
+           Let y' := y.
+
+           Definition x' := S x.
+
+           Definition x'' := x' + y'.
+
+           Print x'.
+
+           End s1.
+
+           Print x'.
+
+          Print x''.
+
+    Notice the difference between the value of `x’` and `x’’` inside section
+    `s1` and outside.
+
+    .. exn:: This is not the last opened section
+
+**Remarks:**
+
+#. Most commands, like ``Hint``, ``Notation``, option management, … which
+   appear inside a section are canceled when the section is closed.
+
+
+Module system
+-------------
+
+The module system provides a way of packaging related elements
+together, as well as a means of massive abstraction.
+
+  .. productionlist:: modules
+    module_type       : qualid
+                      : | `module_type` with Definition qualid := term
+                      : | `module_type` with Module qualid := qualid
+                      : | qualid qualid … qualid
+                      : | !qualid qualid … qualid
+    module_binding    : ( [Import|Export] ident … ident : module_type )
+    module_bindings   : `module_binding` … `module_binding`
+    module_expression : qualid … qualid
+                      : | !qualid … qualid
+
+  Syntax of modules
+
+In the syntax of module application, the ! prefix indicates that any
+`Inline` directive in the type of the functor arguments will be ignored
+(see :ref:`named_module_type` below).
+
+
+.. cmd:: Module @ident.
+
+   This command is used to start an interactive module named `ident`.
+
+.. cmdv:: Module @ident {* @module_binding}.
+
+   Starts an interactive functor with
+   parameters given by module_bindings.
+
+.. cmdv:: Module @ident : @module_type.
+
+   Starts an interactive module specifying its module type.
+
+.. cmdv:: Module @ident {* @module_binding} : @module_type.
+
+   Starts an interactive functor with parameters given by the list of `module binding`, and output module
+   type `module_type`.
+
+.. cmdv:: Module @ident <: {+<: @module_type }.
+
+   Starts an interactive module satisfying each `module_type`.
+
+ .. cmdv:: Module @ident {* @module_binding} <: {+<; @module_type }.
+
+   Starts an interactive functor with parameters given by the list of `module_binding`. The output module type
+   is verified against each `module_type`.
+
+.. cmdv:: Module [ Import | Export ].
+
+   Behaves like ``Module``, but automatically imports or exports the module.
+
+Reserved commands inside an interactive module
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+.. cmd:: Include @module.
+
+   Includes the content of module in the current
+   interactive module. Here module can be a module expression or a module
+   type expression. If module is a high-order module or module type
+   expression then the system tries to instantiate module by the current
+   interactive module.
+
+.. cmd:: Include {+<+ @module}.
+
+   is a shortcut for the commands ``Include`` `module` for each `module`.
+
+.. cmd:: End @ident.
+
+   This command closes the interactive module `ident`. If the module type
+   was given the content of the module is matched against it and an error
+   is signaled if the matching fails. If the module is basic (is not a
+   functor) its components (constants, inductive types, submodules etc.)
+   are now available through the dot notation.
+
+    .. exn:: No such label @ident
+
+    .. exn:: Signature components for label @ident do not match
+
+    .. exn:: This is not the last opened module
+
+.. cmd:: Module @ident := @module_expression.
+
+    This command defines the module identifier `ident` to be equal
+    to `module_expression`.
+
+    .. cmdv:: Module @ident {* @module_binding} := @module_expression.
+
+       Defines a functor with parameters given by the list of `module_binding` and body `module_expression`.
+
+    .. cmdv:: Module @ident {* @module_binding} : @module_type := @module_expression.
+
+       Defines a functor with parameters given by the list of `module_binding` (possibly none), and output module type `module_type`,
+       with body `module_expression`.
+
+    .. cmdv:: Module @ident {* @module_binding} <: {+<: @module_type} := @module_expression.
+
+       Defines a functor with parameters given by module_bindings (possibly none) with body `module_expression`.
+       The body is checked against each |module_type_i|.
+
+    .. cmdv:: Module @ident {* @module_binding} := {+<+ @module_expression}.
+
+       is equivalent to an interactive module where each `module_expression` is included.
+
+.. _named_module_type:
+
+.. cmd:: Module Type @ident.
+
+This command is used to start an interactive module type `ident`.
+
+    .. cmdv:: Module Type @ident {* @module_binding}.
+
+       Starts an interactive functor type with parameters given by `module_bindings`.
+
+
+Reserved commands inside an interactive module type:
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+.. cmd:: Include @module.
+
+   Same as ``Include`` inside a module.
+
+.. cmd:: Include {+<+ @module}.
+
+   is a shortcut for the command ``Include`` `module` for each `module`.
+
+.. cmd:: @assumption_keyword Inline @assums.
+
+   The instance of this assumption will be automatically expanded at functor application, except when
+   this functor application is prefixed by a ``!`` annotation.
+
+.. cmd:: End @ident.
+
+   This command closes the interactive module type `ident`.
+
+   .. exn:: This is not the last opened module type
+
+.. cmd:: Module Type @ident := @module_type.
+
+   Defines a module type `ident` equal to `module_type`.
+
+    .. cmdv:: Module Type @ident {* @module_binding} := @module_type.
+
+       Defines a functor type `ident` specifying functors taking arguments `module_bindings` and
+       returning `module_type`.
+
+    .. cmdv:: Module Type @ident {* @module_binding} := {+<+ @module_type }.
+
+       is equivalent to an interactive module type were each `module_type` is included.
+
+.. cmd:: Declare Module @ident : @module_type.
+
+   Declares a module `ident` of type `module_type`.
+
+    .. cmdv:: Declare Module @ident {* @module_binding} : @module_type.
+
+       Declares a functor with parameters given by the list of `module_binding` and output module type
+       `module_type`.
+
+.. example::
+
+    Let us define a simple module.
+
+    .. coqtop:: all
+
+       Module M.
+
+       Definition T := nat.
+
+       Definition x := 0.
+
+       Definition y : bool.
+
+       exact true.
+
+       Defined.
+
+       End M.
+
+Inside a module one can define constants, prove theorems and do any
+other things that can be done in the toplevel. Components of a closed
+module can be accessed using the dot notation:
+
+.. coqtop:: all
+
+   Print M.x.
+
+A simple module type:
+
+.. coqtop:: all
+
+   Module Type SIG.
+
+   Parameter T : Set.
+
+   Parameter x : T.
+
+   End SIG.
+
+Now we can create a new module from M, giving it a less precise
+specification: the y component is dropped as well as the body of x.
+
+.. coqtop:: all
+
+   Module N : SIG with Definition T := nat := M.
+
+   Print N.T.
+
+   Print N.x.
+
+   Fail Print N.y.
+
+.. reset to remove N (undo in last coqtop block doesn't seem to do that), invisibly redefine M, SIG
+.. coqtop:: none reset
+
+   Module M.
+
+   Definition T := nat.
+
+   Definition x := 0.
+
+   Definition y : bool.
+
+   exact true.
+
+   Defined.
+
+   End M.
+
+   Module Type SIG.
+
+   Parameter T : Set.
+
+   Parameter x : T.
+
+   End SIG.
+
+The definition of ``N`` using the module type expression ``SIG`` with
+``Definition T := nat`` is equivalent to the following one:
+
+.. coqtop:: all
+
+   Module Type SIG'.
+
+   Definition T : Set := nat.
+
+   Parameter x : T.
+
+   End SIG'.
+
+   Module N : SIG' := M.
+
+If we just want to be sure that the our implementation satisfies a
+given module type without restricting the interface, we can use a
+transparent constraint
+
+.. coqtop:: all
+
+   Module P <: SIG := M.
+
+   Print P.y.
+
+Now let us create a functor, i.e. a parametric module
+
+.. coqtop:: all
+
+   Module Two (X Y: SIG).
+
+   Definition T := (X.T * Y.T)%type.
+
+   Definition x := (X.x, Y.x).
+
+   End Two.
+
+and apply it to our modules and do some computations:
+
+.. coqtop:: all
+
+   Module Q := Two M N.
+
+   Eval compute in (fst Q.x + snd Q.x).
+
+In the end, let us define a module type with two sub-modules, sharing
+some of the fields and give one of its possible implementations:
+
+.. coqtop:: all
+
+   Module Type SIG2.
+
+   Declare Module M1 : SIG.
+
+   Module M2 <: SIG.
+
+   Definition T := M1.T.
+
+   Parameter x : T.
+
+   End M2.
+
+   End SIG2.
+
+   Module Mod <: SIG2.
+
+   Module M1.
+
+   Definition T := nat.
+
+   Definition x := 1.
+
+   End M1.
+
+   Module M2 := M.
+
+   End Mod.
+
+Notice that ``M`` is a correct body for the component ``M2`` since its ``T``
+component is equal ``nat`` and hence ``M1.T`` as specified.
+
+**Remarks:**
+
+#. Modules and module types can be nested components of each other.
+#. One can have sections inside a module or a module type, but not a
+   module or a module type inside a section.
+#. Commands like ``Hint`` or ``Notation`` can also appear inside modules and
+   module types. Note that in case of a module definition like:
+
+::
+
+  Module N : SIG := M.
+
+or::
+
+  Module N : SIG. … End N.
+
+hints and the like valid for ``N`` are not those defined in ``M`` (or the module body) but the ones defined
+in ``SIG``.
+
+
+.. _import_qualid:
+
+.. cmd:: Import @qualid.
+
+    If `qualid` denotes a valid basic module (i.e. its module type is a
+    signature), makes its components available by their short names.
+
+.. example::
+
+    .. coqtop:: reset all
+
+       Module Mod.
+
+       Definition T:=nat.
+
+       Check T.
+
+       End Mod.
+
+       Check Mod.T.
+
+       Fail Check T.
+
+       Import Mod.
+
+       Check T.
+
+Some features defined in modules are activated only when a module is
+imported. This is for instance the case of notations (see :ref:`TODO-12.1-Notations`).
+
+Declarations made with the Local flag are never imported by theImport
+command. Such declarations are only accessible through their fully
+qualified name.
+
+.. example::
+
+    .. coqtop:: all
+
+       Module A.
+
+       Module B.
+
+       Local Definition T := nat.
+
+       End B.
+
+       End A.
+
+       Import A.
+
+       Fail Check B.T.
+
+    .. cmdv:: Export @qualid
+
+       When the module containing the command Export qualid
+       is imported, qualid is imported as well.
+
+    .. exn:: @qualid is not a module
+
+    .. warn:: Trying to mask the absolute name @qualid!
+
+.. cmd:: Print Module @ident.
+
+    Prints the module type and (optionally) the body of the module `ident`.
+
+.. cmd:: Print Module Type @ident.
+
+    Prints the module type corresponding to `ident`.
+
+.. opt:: Short Module Printing
+
+    This option (off by default) disables the printing of the types of fields,
+    leaving only their names, for the commands ``Print Module`` and ``Print Module Type``.
+
+.. cmd:: Locate Module @qualid.
+
+    Prints the full name of the module `qualid`.
+
+Libraries and qualified names
+---------------------------------
+
+Names of libraries
+~~~~~~~~~~~~~~~~~~
+
+The theories developed in |Coq| are stored in *library files* which are
+hierarchically classified into *libraries* and *sublibraries*. To
+express this hierarchy, library names are represented by qualified
+identifiers qualid, i.e. as list of identifiers separated by dots (see
+:ref:`TODO-1.2.3-identifiers`). For instance, the library file ``Mult`` of the standard
+|Coq| library ``Arith`` is named ``Coq.Arith.Mult``. The identifier that starts
+the name of a library is called a *library root*. All library files of
+the standard library of |Coq| have the reserved root |Coq| but library
+file names based on other roots can be obtained by using |Coq| commands
+(coqc, coqtop, coqdep, …) options ``-Q`` or ``-R`` (see :ref:`TODO-14.3.3-command-line-options`).
+Also, when an interactive |Coq| session starts, a library of root ``Top`` is
+started, unless option ``-top`` or ``-notop`` is set (see :ref:`TODO-14.3.3-command-line-options`).
+
+
+Qualified names
+~~~~~~~~~~~~~~~
+
+Library files are modules which possibly contain submodules which
+eventually contain constructions (axioms, parameters, definitions,
+lemmas, theorems, remarks or facts). The *absolute name*, or *full
+name*, of a construction in some library file is a qualified
+identifier starting with the logical name of the library file,
+followed by the sequence of submodules names encapsulating the
+construction and ended by the proper name of the construction.
+Typically, the absolute name ``Coq.Init.Logic.eq`` denotes Leibniz’
+equality defined in the module Logic in the sublibrary ``Init`` of the
+standard library of |Coq|.
+
+The proper name that ends the name of a construction is the short name
+(or sometimes base name) of the construction (for instance, the short
+name of ``Coq.Init.Logic.eq`` is ``eq``). Any partial suffix of the absolute
+name is a *partially qualified name* (e.g. ``Logic.eq`` is a partially
+qualified name for ``Coq.Init.Logic.eq``). Especially, the short name of a
+construction is its shortest partially qualified name.
+
+|Coq| does not accept two constructions (definition, theorem, …) with
+the same absolute name but different constructions can have the same
+short name (or even same partially qualified names as soon as the full
+names are different).
+
+Notice that the notion of absolute, partially qualified and short
+names also applies to library file names.
+
+**Visibility**
+
+|Coq| maintains a table called the name table which maps partially qualified
+names of constructions to absolute names. This table is updated by the
+commands ``Require`` (see :ref:`TODO-6.5.1-Require`), Import and Export (see :ref:`import_qualid`) and
+also each time a new declaration is added to the context. An absolute
+name is called visible from a given short or partially qualified name
+when this latter name is enough to denote it. This means that the
+short or partially qualified name is mapped to the absolute name in
+|Coq| name table. Definitions flagged as Local are only accessible with
+their fully qualified name (see :ref:`TODO-1.3.2-definitions`).
+
+It may happen that a visible name is hidden by the short name or a
+qualified name of another construction. In this case, the name that
+has been hidden must be referred to using one more level of
+qualification. To ensure that a construction always remains
+accessible, absolute names can never be hidden.
+
+.. example::
+
+    .. coqtop:: all
+
+       Check 0.
+
+       Definition nat := bool.
+
+       Check 0.
+
+       Check Datatypes.nat.
+
+       Locate nat.
+
+See also: Command Locate in :ref:`TODO-6.3.10-locate-qualid` and Locate Library in
+:ref:`TODO-6.6.11-locate-library`.
+
+
+Libraries and filesystem
+~~~~~~~~~~~~~~~~~~~~~~~~
+
+Please note that the questions described here have been subject to
+redesign in |Coq| v8.5. Former versions of |Coq| use the same terminology
+to describe slightly different things.
+
+Compiled files (``.vo`` and ``.vio``) store sub-libraries. In order to refer
+to them inside |Coq|, a translation from file-system names to |Coq| names
+is needed. In this translation, names in the file system are called
+*physical* paths while |Coq| names are contrastingly called *logical*
+names.
+
+A logical prefix Lib can be associated to a physical pathpath using
+the command line option ``-Q`` `path` ``Lib``. All subfolders of path are
+recursively associated to the logical path ``Lib`` extended with the
+corresponding suffix coming from the physical path. For instance, the
+folder ``path/fOO/Bar`` maps to ``Lib.fOO.Bar``. Subdirectories corresponding
+to invalid |Coq| identifiers are skipped, and, by convention,
+subdirectories named ``CVS`` or ``_darcs`` are skipped too.
+
+Thanks to this mechanism, .vo files are made available through the
+logical name of the folder they are in, extended with their own
+basename. For example, the name associated to the file
+``path/fOO/Bar/File.vo`` is ``Lib.fOO.Bar.File``. The same caveat applies for
+invalid identifiers. When compiling a source file, the ``.vo`` file stores
+its logical name, so that an error is issued if it is loaded with the
+wrong loadpath afterwards.
+
+Some folders have a special status and are automatically put in the
+path. |Coq| commands associate automatically a logical path to files in
+the repository trees rooted at the directory from where the command is
+launched, coqlib/user-contrib/, the directories listed in the
+`$COQPATH`, `${XDG_DATA_HOME}/coq/` and `${XDG_DATA_DIRS}/coq/`
+environment variables (see`http://standards.freedesktop.org/basedir-
+spec/basedir-spec-latest.html`_) with the same physical-to-logical
+translation and with an empty logical prefix.
+
+The command line option ``-R`` is a variant of ``-Q`` which has the strictly
+same behavior regarding loadpaths, but which also makes the
+corresponding ``.vo`` files available through their short names in a way
+not unlike the ``Import`` command (see :ref:`import_qualid`). For instance, ``-R`` `path` ``Lib``
+associates to the ``filepath/fOO/Bar/File.vo`` the logical name
+``Lib.fOO.Bar.File``, but allows this file to be accessed through the
+short names ``fOO.Bar.File,Bar.File`` and ``File``. If several files with
+identical base name are present in different subdirectories of a
+recursive loadpath, which of these files is found first may be system-
+dependent and explicit qualification is recommended. The ``From`` argument
+of the ``Require`` command can be used to bypass the implicit shortening
+by providing an absolute root to the required file (see :ref:`TODO-6.5.1-require-qualid`).
+
+There also exists another independent loadpath mechanism attached to
+OCaml object files (``.cmo`` or ``.cmxs``) rather than |Coq| object
+files as described above. The OCaml loadpath is managed using
+the option ``-I`` `path` (in the OCaml world, there is neither a
+notion of logical name prefix nor a way to access files in
+subdirectories of path). See the command ``Declare`` ``ML`` ``Module`` in
+:ref:`TODO-6.5-compiled-files` to understand the need of the OCaml loadpath.
+
+See :ref:`TODO-14.3.3-command-line-options` for a more general view over the |Coq| command
+line options.
+
+
+Implicit arguments
+------------------
+
+An implicit argument of a function is an argument which can be
+inferred from contextual knowledge. There are different kinds of
+implicit arguments that can be considered implicit in different ways.
+There are also various commands to control the setting or the
+inference of implicit arguments.
+
+
+The different kinds of implicit arguments
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+Implicit arguments inferable from the knowledge of other arguments of a function
+++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
+
+The first kind of implicit arguments covers the arguments that are
+inferable from the knowledge of the type of other arguments of the
+function, or of the type of the surrounding context of the
+application. Especially, such implicit arguments correspond to
+parameters dependent in the type of the function. Typical implicit
+arguments are the type arguments in polymorphic functions. There are
+several kinds of such implicit arguments.
+
+**Strict Implicit Arguments**
+
+An implicit argument can be either strict or non strict. An implicit
+argument is said to be *strict* if, whatever the other arguments of the
+function are, it is still inferable from the type of some other
+argument. Technically, an implicit argument is strict if it
+corresponds to a parameter which is not applied to a variable which
+itself is another parameter of the function (since this parameter may
+erase its arguments), not in the body of a match, and not itself
+applied or matched against patterns (since the original form of the
+argument can be lost by reduction).
+
+For instance, the first argument of
+::
+
+  cons: forall A:Set, A -> list A -> list A
+
+in module ``List.v`` is strict because :g:`list` is an inductive type and :g:`A`
+will always be inferable from the type :g:`list A` of the third argument of
+:g:`cons`. On the contrary, the second argument of a term of type
+::
+
+  forall P:nat->Prop, forall n:nat, P n -> ex nat P
+
+is implicit but not strict, since it can only be inferred from the
+type :g:`P n` of the third argument and if :g:`P` is, e.g., :g:`fun _ => True`, it
+reduces to an expression where ``n`` does not occur any longer. The first
+argument :g:`P` is implicit but not strict either because it can only be
+inferred from :g:`P n` and :g:`P` is not canonically inferable from an arbitrary
+:g:`n` and the normal form of :g:`P n`. Consider, e.g., that :g:`n` is :math:`0` and the third
+argument has type :g:`True`, then any :g:`P` of the form
+::
+
+  fun n => match n with 0 => True | _ => anything end
+
+would be a solution of the inference problem.
+
+**Contextual Implicit Arguments**
+
+An implicit argument can be *contextual* or not. An implicit argument
+is said *contextual* if it can be inferred only from the knowledge of
+the type of the context of the current expression. For instance, the
+only argument of::
+
+  nil : forall A:Set, list A`
+
+is contextual. Similarly, both arguments of a term of type::
+
+  forall P:nat->Prop, forall n:nat, P n \/ n = 0
+
+are contextual (moreover, :g:`n` is strict and :g:`P` is not).
+
+**Reversible-Pattern Implicit Arguments**
+
+There is another class of implicit arguments that can be reinferred
+unambiguously if all the types of the remaining arguments are known.
+This is the class of implicit arguments occurring in the type of
+another argument in position of reversible pattern, which means it is
+at the head of an application but applied only to uninstantiated
+distinct variables. Such an implicit argument is called *reversible-
+pattern implicit argument*. A typical example is the argument :g:`P` of
+nat_rec in
+::
+
+  nat_rec : forall P : nat -> Set, P 0 ->
+    (forall n : nat, P n -> P (S n)) -> forall x : nat, P x
+
+(:g:`P` is reinferable by abstracting over :g:`n` in the type :g:`P n`).
+
+See :ref:`controlling-rev-pattern-implicit-args` for the automatic declaration of reversible-pattern
+implicit arguments.
+
+Implicit arguments inferable by resolution
+++++++++++++++++++++++++++++++++++++++++++
+
+This corresponds to a class of non-dependent implicit arguments that
+are solved based on the structure of their type only.
+
+
+Maximal or non maximal insertion of implicit arguments
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+In case a function is partially applied, and the next argument to be
+applied is an implicit argument, two disciplines are applicable. In
+the first case, the function is considered to have no arguments
+furtherly: one says that the implicit argument is not maximally
+inserted. In the second case, the function is considered to be
+implicitly applied to the implicit arguments it is waiting for: one
+says that the implicit argument is maximally inserted.
+
+Each implicit argument can be declared to have to be inserted
+maximally or non maximally. This can be governed argument per argument
+by the command ``Implicit Arguments`` (see Section :ref:`declare-implicit-args`) or globally by the
+command ``Set Maximal Implicit Insertion`` (see Section :ref:`controlling-insertion-implicit-args`).
+See also :ref:`displaying-implicit-args`.
+
+
+Casual use of implicit arguments
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+In a given expression, if it is clear that some argument of a function
+can be inferred from the type of the other arguments, the user can
+force the given argument to be guessed by replacing it by “_”. If
+possible, the correct argument will be automatically generated.
+
+.. exn:: Cannot infer a term for this placeholder.
+
+   |Coq| was not able to deduce an instantiation of a “_”.
+
+.. _declare-implicit-args:
+
+Declaration of implicit arguments
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+In case one wants that some arguments of a given object (constant,
+inductive types, constructors, assumptions, local or not) are always
+inferred by |Coq|, one may declare once and for all which are the
+expected implicit arguments of this object. There are two ways to do
+this, *a priori* and *a posteriori*.
+
+
+Implicit Argument Binders
++++++++++++++++++++++++++
+
+In the first setting, one wants to explicitly give the implicit
+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:
+
+.. coqtop:: all
+
+   Definition id {A : Type} (x : A) : A := x.
+
+This automatically declares the argument A of id as a maximally
+inserted implicit argument. One can then do as-if the argument was
+absent in every situation but still be able to specify it if needed:
+
+.. coqtop:: all
+
+   Definition compose {A B C} (g : B -> C) (f : A -> B) := fun x => g (f x).
+
+   Goal forall A, compose id id = id (A:=A).
+
+
+The syntax is supported in all top-level definitions:
+``Definition``, ``Fixpoint``, ``Lemma`` and so on. For (co-)inductive datatype
+declarations, the semantics are the following: an inductive parameter
+declared as an implicit argument need not be repeated in the inductive
+definition but will become implicit for the constructors of the
+inductive only, not the inductive type itself. For example:
+
+.. coqtop:: all
+
+   Inductive list {A : Type} : Type :=
+   | nil : list
+   | cons : A -> list -> list.
+
+   Print list.
+
+One can always specify the parameter if it is not uniform using the
+usual implicit arguments disambiguation syntax.
+
+
+Declaring Implicit Arguments
+++++++++++++++++++++++++++++
+
+To set implicit arguments *a posteriori*, one can use the command:
+
+.. cmd:: Arguments @qualid {* @possibly_bracketed_ident }.
+
+where the list of `possibly_bracketed_ident` is a prefix of the list of
+arguments of `qualid` where the ones to be declared implicit are
+surrounded by square brackets and the ones to be declared as maximally
+inserted implicits are surrounded by curly braces.
+
+After the above declaration is issued, implicit arguments can just
+(and have to) be skipped in any expression involving an application
+of `qualid`.
+
+Implicit arguments can be cleared with the following syntax:
+
+.. cmd:: Arguments @qualid : clear implicits.
+
+.. cmdv:: Global Arguments @qualid {* @possibly_bracketed_ident }
+
+   Says to recompute the implicit arguments of
+   `qualid` after ending of the current section if any, enforcing the
+   implicit arguments known from inside the section to be the ones
+   declared by the command.
+
+.. cmdv:: Local Arguments @qualid {* @possibly_bracketed_ident }.
+
+   When in a module, tell not to activate the
+   implicit arguments ofqualid declared by this command to contexts that
+   require the module.
+
+.. cmdv:: {? Global | Local } Arguments @qualid {*, {+ @possibly_bracketed_ident } }.
+
+   For names of constants, inductive types,
+   constructors, lemmas which can only be applied to a fixed number of
+   arguments (this excludes for instance constants whose type is
+   polymorphic), multiple implicit arguments declarations can be given.
+   Depending on the number of arguments qualid is applied to in practice,
+   the longest applicable list of implicit arguments is used to select
+   which implicit arguments are inserted. For printing, the omitted
+   arguments are the ones of the longest list of implicit arguments of
+   the sequence.
+
+.. example::
+
+    .. coqtop:: reset all
+
+       Inductive list (A:Type) : Type :=
+       | nil : list A
+       | cons : A -> list A -> list A.
+
+       Check (cons nat 3 (nil nat)).
+
+       Arguments cons [A] _ _.
+
+       Arguments nil [A].
+
+       Check (cons 3 nil).
+
+       Fixpoint map (A B:Type) (f:A->B) (l:list A) : list B := match l with nil => nil | cons a t => cons (f a) (map A B f t) end.
+
+       Fixpoint length (A:Type) (l:list A) : nat := match l with nil => 0 | cons _ m => S (length A m) end.
+
+       Arguments map [A B] f l.
+
+       Arguments length {A} l. (* A has to be maximally inserted *)
+
+       Check (fun l:list (list nat) => map length l).
+
+       Arguments map [A B] f l, [A] B f l, A B f l.
+
+       Check (fun l => map length l = map (list nat) nat length l).
+
+Remark: To know which are the implicit arguments of an object, use the
+command ``Print Implicit`` (see :ref:`displaying-implicit-args`).
+
+
+Automatic declaration of implicit arguments
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+|Coq| can also automatically detect what are the implicit arguments of a
+defined object. The command is just
+
+.. cmd:: Arguments @qualid : default implicits.
+
+The auto-detection is governed by options telling if strict,
+contextual, or reversible-pattern implicit arguments must be
+considered or not (see :ref:`controlling-strict-implicit-args`, :ref:`controlling-strict-implicit-args`,
+:ref:`controlling-rev-pattern-implicit-args`, and also :ref:`controlling-insertion-implicit-args`).
+
+.. cmdv:: Global Arguments @qualid : default implicits
+
+    Tell to recompute the
+    implicit arguments of qualid after ending of the current section if
+    any.
+
+.. cmdv:: Local Arguments @qualid : default implicits
+
+       When in a module, tell not to activate the implicit arguments of `qualid` computed by this
+       declaration to contexts that requires the module.
+
+.. example::
+
+   .. coqtop:: reset all
+
+       Inductive list (A:Set) : Set :=
+       | nil : list A
+       | cons : A -> list A -> list A.
+
+       Arguments cons : default implicits.
+
+       Print Implicit cons.
+
+       Arguments nil : default implicits.
+
+       Print Implicit nil.
+
+       Set Contextual Implicit.
+
+       Arguments nil : default implicits.
+
+       Print Implicit nil.
+
+The computation of implicit arguments takes account of the unfolding
+of constants. For instance, the variable ``p`` below has type
+``(Transitivity R)`` which is reducible to
+``forall x,y:U, R x y -> forall z:U, R y z -> R x z``. As the variables ``x``, ``y`` and ``z``
+appear strictly in the body of the type, they are implicit.
+
+.. coqtop:: reset none
+
+   Set Warnings "-local-declaration".
+
+.. coqtop:: all
+
+   Variable X : Type.
+
+   Definition Relation := X -> X -> Prop.
+
+   Definition Transitivity (R:Relation) := forall x y:X, R x y -> forall z:X, R y z -> R x z.
+
+   Variables (R : Relation) (p : Transitivity R).
+
+   Arguments p : default implicits.
+
+   Print p.
+
+   Print Implicit p.
+
+   Variables (a b c : X) (r1 : R a b) (r2 : R b c).
+
+   Check (p r1 r2).
+
+
+Mode for automatic declaration of implicit arguments
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+In case one wants to systematically declare implicit the arguments
+detectable as such, one may switch to the automatic declaration of
+implicit arguments mode by using the command:
+
+.. cmd:: Set Implicit Arguments.
+
+Conversely, one may unset the mode by using ``Unset Implicit Arguments``.
+The mode is off by default. Auto-detection of implicit arguments is
+governed by options controlling whether strict and contextual implicit
+arguments have to be considered or not.
+
+.. _controlling-strict-implicit-args:
+
+Controlling strict implicit arguments
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+When the mode for automatic declaration of implicit arguments is on,
+the default is to automatically set implicit only the strict implicit
+arguments plus, for historical reasons, a small subset of the non-strict
+implicit arguments. To relax this constraint and to set
+implicit all non strict implicit arguments by default, use the command:
+
+.. cmd:: Unset Strict Implicit.
+
+Conversely, use the command ``Set Strict Implicit`` to restore the
+original mode that declares implicit only the strict implicit
+arguments plus a small subset of the non strict implicit arguments.
+
+In the other way round, to capture exactly the strict implicit
+arguments and no more than the strict implicit arguments, use the
+command
+
+.. cmd:: Set Strongly Strict Implicit.
+
+Conversely, use the command ``Unset Strongly Strict Implicit`` to let the
+option “Strict Implicit” decide what to do.
+
+Remark: In versions of |Coq| prior to version 8.0, the default was to
+declare the strict implicit arguments as implicit.
+
+.. _controlling-contextual-implicit-args:
+
+Controlling contextual implicit arguments
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+By default, |Coq| does not automatically set implicit the contextual
+implicit arguments. To tell |Coq| to infer also contextual implicit
+argument, use command
+
+.. cmd:: Set Contextual Implicit.
+
+Conversely, use command ``Unset Contextual Implicit`` to unset the
+contextual implicit mode.
+
+.. _controlling-rev-pattern-implicit-args:
+
+Controlling reversible-pattern implicit arguments
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+By default, |Coq| does not automatically set implicit the reversible-pattern
+implicit arguments. To tell |Coq| to infer also reversible-
+pattern implicit argument, use command
+
+.. cmd:: Set Reversible Pattern Implicit.
+
+Conversely, use command ``Unset Reversible Pattern Implicit`` to unset the
+reversible-pattern implicit mode.
+
+.. _controlling-insertion-implicit-args:
+
+Controlling the insertion of implicit arguments not followed by explicit arguments
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+Implicit arguments can be declared to be automatically inserted when a
+function is partially applied and the next argument of the function is
+an implicit one. In case the implicit arguments are automatically
+declared (with the command ``Set Implicit Arguments``), the command
+
+.. cmd:: Set Maximal Implicit Insertion.
+
+is used to tell to declare the implicit arguments with a maximal
+insertion status. By default, automatically declared implicit
+arguments are not declared to be insertable maximally. To restore the
+default mode for maximal insertion, use the command
+
+.. cmd:: Unset Maximal Implicit Insertion.
+
+Explicit applications
+~~~~~~~~~~~~~~~~~~~~~
+
+In presence of non-strict or contextual argument, or in presence of
+partial applications, the synthesis of implicit arguments may fail, so
+one may have to give explicitly certain implicit arguments of an
+application. The syntax for this is ``(`` `ident` ``:=`` `term` ``)`` where `ident` is the
+name of the implicit argument and term is its corresponding explicit
+term. Alternatively, one can locally deactivate the hiding of implicit
+arguments of a function by using the notation `@qualid` |term_1| … |term_n|.
+This syntax extension is given in the following grammar:
+
+.. _explicit_app_grammar:
+
+  .. productionlist:: explicit_apps
+       term     : @ qualid term … `term`
+                : | @ qualid
+                : | qualid `argument` … `argument`
+       argument : `term`
+                : | (ident := `term`)
+
+  Syntax for explicitly giving implicit arguments
+
+.. example:: (continued)
+
+    .. coqtop:: all
+
+       Check (p r1 (z:=c)).
+
+       Check (p (x:=a) (y:=b) r1 (z:=c) r2).
+
+
+Renaming implicit arguments
+~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+Implicit arguments names can be redefined using the following syntax:
+
+.. cmd:: Arguments @qualid {* @name} : @rename.
+
+With the assert flag, ``Arguments`` can be used to assert that a given
+object has the expected number of arguments and that these arguments
+are named as expected.
+
+.. example:: (continued)
+
+.. coqtop:: all
+
+   Arguments p [s t] _ [u] _: rename.
+
+   Check (p r1 (u:=c)).
+
+   Check (p (s:=a) (t:=b) r1 (u:=c) r2).
+
+   Fail Arguments p [s t] _ [w] _ : assert.
+
+.. _displaying-implicit-args:
+
+Displaying what the implicit arguments are
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+To display the implicit arguments associated to an object, and to know
+if each of them is to be used maximally or not, use the command
+
+.. cmd:: Print Implicit @qualid.
+
+Explicit displaying of implicit arguments for pretty-printing
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+By default the basic pretty-printing rules hide the inferable implicit
+arguments of an application. To force printing all implicit arguments,
+use command
+
+.. cmd:: Set Printing Implicit.
+
+Conversely, to restore the hiding of implicit arguments, use command
+
+.. cmd:: Unset Printing Implicit.
+
+By default the basic pretty-printing rules display the implicit
+arguments that are not detected as strict implicit arguments. This
+“defensive” mode can quickly make the display cumbersome so this can
+be deactivated by using the command
+
+.. cmd:: Unset Printing Implicit Defensive.
+
+Conversely, to force the display of non strict arguments, use command
+
+.. cmd:: Set Printing Implicit Defensive.
+
+See also: ``Set Printing All`` in :ref:`printing_constructions_full`.
+
+Interaction with subtyping
+~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+When an implicit argument can be inferred from the type of more than
+one of the other arguments, then only the type of the first of these
+arguments is taken into account, and not an upper type of all of them.
+As a consequence, the inference of the implicit argument of “=” fails
+in
+
+.. coqtop:: all
+
+   Fail Check nat = Prop.
+
+but succeeds in
+
+.. coqtop:: all
+
+   Check Prop = nat.
+
+
+Deactivation of implicit arguments for parsing
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+Use of implicit arguments can be deactivated by issuing the command:
+
+.. cmd:: Set Parsing Explicit.
+
+In this case, all arguments of constants, inductive types,
+constructors, etc, including the arguments declared as implicit, have
+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:
+
+.. cmd:: Unset Parsing Explicit.
+
+Canonical structures
+~~~~~~~~~~~~~~~~~~~~
+
+A canonical structure is an instance of a record/structure type that
+can be used to solve unification problems involving a projection
+applied to an unknown structure instance (an implicit argument) and a
+value. The complete documentation of canonical structures can be found
+in :ref:`canonicalstructures`; here only a simple example is given.
+
+Assume that `qualid` denotes an object ``(Build_struc`` |c_1| … |c_n| ``)`` in the
+structure *struct* of which the fields are |x_1|, …, |x_n|. Assume that
+`qualid` is declared as a canonical structure using the command
+
+.. cmd:: Canonical Structure @qualid.
+
+Then, each time an equation of the form ``(``\ |x_i| ``_)`` |eq_beta_delta_iota_zeta| |c_i| has to be
+solved during the type-checking process, `qualid` is used as a solution.
+Otherwise said, `qualid` is canonically used to extend the field |c_i|
+into a complete structure built on |c_i|.
+
+Canonical structures are particularly useful when mixed with coercions
+and strict implicit arguments. Here is an example.
+
+.. coqtop:: all
+
+   Require Import Relations.
+
+   Require Import EqNat.
+
+   Set Implicit Arguments.
+
+   Unset Strict Implicit.
+
+   Structure Setoid : Type := {Carrier :> Set; Equal : relation Carrier;
+                               Prf_equiv : equivalence Carrier Equal}.
+
+   Definition is_law (A B:Setoid) (f:A -> B) := forall x y:A, Equal x y -> Equal (f x) (f y).
+
+   Axiom eq_nat_equiv : equivalence nat eq_nat.
+
+   Definition nat_setoid : Setoid := Build_Setoid eq_nat_equiv.
+
+   Canonical Structure nat_setoid.
+
+Thanks to ``nat_setoid`` declared as canonical, the implicit arguments ``A``
+and ``B`` can be synthesized in the next statement.
+
+.. coqtop:: all
+
+   Lemma is_law_S : is_law S.
+
+Remark: If a same field occurs in several canonical structure, then
+only the structure declared first as canonical is considered.
+
+.. cmdv:: Canonical Structure @ident := @term : @type.
+
+.. cmdv:: Canonical Structure @ident := @term.
+
+.. cmdv:: Canonical Structure @ident : @type := @term.
+
+These are equivalent to a regular definition of `ident` followed by the declaration
+``Canonical Structure`` `ident`.
+
+See also: more examples in user contribution category (Rocq/ALGEBRA).
+
+
+Print Canonical Projections.
+++++++++++++++++++++++++++++
+
+This displays the list of global names that are components of some
+canonical structure. For each of them, the canonical structure of
+which it is a projection is indicated. For instance, the above example
+gives the following output:
+
+.. coqtop:: all
+
+   Print Canonical Projections.
+
+
+Implicit types of variables
+~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+It is possible to bind variable names to a given type (e.g. in a
+development using arithmetic, it may be convenient to bind the names `n`
+or `m` to the type ``nat`` of natural numbers). The command for that is
+
+.. cmd:: Implicit Types {+ @ident } : @type.
+
+The effect of the command is to automatically set the type of bound
+variables starting with `ident` (either `ident` itself or `ident` followed by
+one or more single quotes, underscore or digits) to be `type` (unless
+the bound variable is already declared with an explicit type in which
+case, this latter type is considered).
+
+.. example::
+
+    .. coqtop:: all
+
+       Require Import List.
+
+       Implicit Types m n : nat.
+
+       Lemma cons_inj_nat : forall m n l, n :: l = m :: l -> n = m.
+
+       intros m n.
+
+       Lemma cons_inj_bool : forall (m n:bool) l, n :: l = m :: l -> n = m.
+
+.. cmdv:: Implicit Type @ident : @type.
+
+  This is useful for declaring the implicit type of a single variable.
+
+.. cmdv:: Implicit Types {+ ( {+ @ident } : @term ) }
+
+  Adds blocks of implicit types with different specifications.
+
+Implicit generalization
+~~~~~~~~~~~~~~~~~~~~~~~
+
+.. index:: `{ }
+.. index:: `( )
+
+Implicit generalization is an automatic elaboration of a statement
+with free variables into a closed statement where these variables are
+quantified explicitly. Implicit generalization is done inside binders
+starting with a \` and terms delimited by \`{ } and \`( ), always
+introducing maximally inserted implicit arguments for the generalized
+variables. Inside implicit generalization delimiters, free variables
+in the current context are automatically quantified using a product or
+a lambda abstraction to generate a closed term. In the following
+statement for example, the variables n and m are automatically
+generalized and become explicit arguments of the lemma as we are using
+\`( ):
+
+.. coqtop:: all
+
+   Generalizable All Variables.
+
+   Lemma nat_comm : `(n = n + 0).
+
+One can control the set of generalizable identifiers with
+the ``Generalizable`` vernacular command to avoid unexpected
+generalizations when mistyping identifiers. There are several commands
+that specify which variables should be generalizable.
+
+.. cmd:: Generalizable All Variables.
+
+   All variables are candidate for
+   generalization if they appear free in the context under a
+   generalization delimiter. This may result in confusing errors in case
+   of typos. In such cases, the context will probably contain some
+   unexpected generalized variable.
+
+.. cmd:: Generalizable No Variables.
+
+   Disable implicit generalization  entirely. This is the default behavior.
+
+.. cmd:: Generalizable (Variable | Variables) {+ @ident }.
+
+   Allow generalization of the given identifiers only. Calling this command multiple times
+   adds to the allowed identifiers.
+
+.. cmd:: Global Generalizable.
+
+   Allows exporting the choice of generalizable variables.
+
+One can also use implicit generalization for binders, in which case
+the generalized variables are added as binders and set maximally
+implicit.
+
+.. coqtop:: all
+
+   Definition id `(x : A) : A := x.
+
+   Print id.
+
+The generalizing binders \`{ } and \`( ) work similarly to their
+explicit counterparts, only binding the generalized variables
+implicitly, as maximally-inserted arguments. In these binders, the
+binding name for the bound object is optional, whereas the type is
+mandatory, dually to regular binders.
+
+
+Coercions
+---------
+
+Coercions can be used to implicitly inject terms from one *class* in
+which they reside into another one. A *class* is either a sort
+(denoted by the keyword ``Sortclass``), a product type (denoted by the
+keyword ``Funclass``), or a type constructor (denoted by its name), e.g.
+an inductive type or any constant with a type of the form
+``forall (`` |x_1| : |A_1| ) … ``(``\ |x_n| : |A_n|\ ``)``, `s` where `s` is a sort.
+
+Then the user is able to apply an object that is not a function, but
+can be coerced to a function, and more generally to consider that a
+term of type ``A`` is of type ``B`` provided that there is a declared coercion
+between ``A`` and ``B``. The main command is
+
+.. cmd:: Coercion @qualid : @class >-> @class.
+
+which declares the construction denoted by qualid as a coercion
+between the two given classes.
+
+More details and examples, and a description of the commands related
+to coercions are provided in :ref:`implicitcoercions`.
+
+.. _printing_constructions_full:
+
+Printing constructions in full
+------------------------------
+
+Coercions, implicit arguments, the type of pattern-matching, but also
+notations (see :ref:`syntaxextensionsandinterpretationscopes`) can obfuscate the behavior of some
+tactics (typically the tactics applying to occurrences of subterms are
+sensitive to the implicit arguments). The command
+
+.. cmd:: Set Printing All.
+
+deactivates all high-level printing features such as coercions,
+implicit arguments, returned type of pattern-matching, notations and
+various syntactic sugar for pattern-matching or record projections.
+Otherwise said, ``Set Printing All`` includes the effects of the commands
+``Set Printing Implicit``, ``Set Printing Coercions``, ``Set Printing Synth``,
+``Unset Printing Projections``, and ``Unset Printing Notations``. To reactivate
+the high-level printing features, use the command
+
+.. cmd:: Unset Printing All.
+
+Printing universes
+------------------
+
+The following command:
+
+.. cmd:: Set Printing Universes.
+
+activates the display of the actual level of each occurrence of ``Type``.
+See :ref:`TODO-4.1.1-sorts` for details. This wizard option, in combination
+with ``Set Printing All`` (see :ref:`printing_constructions_full`) can help to diagnose failures
+to unify terms apparently identical but internally different in the
+Calculus of Inductive Constructions. To reactivate the display of the
+actual level of the occurrences of Type, use
+
+.. cmd:: Unset Printing Universes.
+
+The constraints on the internal level of the occurrences of Type
+(see :ref:`TODO-4.1.1-sorts`) can be printed using the command
+
+.. cmd:: Print {? Sorted} Universes.
+
+If the optional ``Sorted`` option is given, each universe will be made
+equivalent to a numbered label reflecting its level (with a linear
+ordering) in the universe hierarchy.
+
+This command also accepts an optional output filename:
+
+.. cmd:: Print {? Sorted} Universes @string.
+
+If `string` ends in ``.dot`` or ``.gv``, the constraints are printed in the DOT
+language, and can be processed by Graphviz tools. The format is
+unspecified if `string` doesn’t end in ``.dot`` or ``.gv``.
+
+
+Existential variables
+---------------------
+
+|Coq| terms can include existential variables which represents unknown
+subterms to eventually be replaced by actual subterms.
+
+Existential variables are generated in place of unsolvable implicit
+arguments or “_” placeholders when using commands such as ``Check`` (see
+Section :ref:`TODO-6.3.1-check`) or when using tactics such as ``refine`` (see Section
+:ref:`TODO-8.2.3-refine`), as well as in place of unsolvable instances when using
+tactics such that ``eapply`` (see Section :ref:`TODO-8.2.4-apply`). An existential
+variable is defined in a context, which is the context of variables of
+the placeholder which generated the existential variable, and a type,
+which is the expected type of the placeholder.
+
+As a consequence of typing constraints, existential variables can be
+duplicated in such a way that they possibly appear in different
+contexts than their defining context. Thus, any occurrence of a given
+existential variable comes with an instance of its original context.
+In the simple case, when an existential variable denotes the
+placeholder which generated it, or is used in the same context as the
+one in which it was generated, the context is not displayed and the
+existential variable is represented by “?” followed by an identifier.
+
+.. coqtop:: all
+
+   Parameter identity : forall (X:Set), X -> X.
+
+   Check identity _ _.
+
+   Check identity _ (fun x => _).
+
+In the general case, when an existential variable ``?``\ `ident` appears
+outside of its context of definition, its instance, written under the
+form
+
+| ``{`` :n:`{*; @ident:=@term}` ``}``
+
+is appending to its name, indicating how the variables of its defining context are instantiated.
+The variables of the context of the existential variables which are
+instantiated by themselves are not written, unless the flag ``Printing Existential Instances``
+is on (see Section :ref:`explicit-display-existentials`), and this is why an
+existential variable used in the same context as its context of definition is written with no instance.
+
+.. coqtop:: all
+
+   Check (fun x y => _) 0 1.
+
+   Set Printing Existential Instances.
+
+   Check (fun x y => _) 0 1.
+
+Existential variables can be named by the user upon creation using
+the syntax ``?``\ `ident`. This is useful when the existential
+variable needs to be explicitly handled later in the script (e.g.
+with a named-goal selector, see :ref:`TODO-9.2-goal-selectors`).
+
+.. _explicit-display-existentials:
+
+Explicit displaying of existential instances for pretty-printing
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+The command:
+
+.. cmd:: Set Printing Existential Instances.
+
+activates the full display of how the context of an existential
+variable is instantiated at each of the occurrences of the existential
+variable.
+
+To deactivate the full display of the instances of existential
+variables, use
+
+.. cmd:: Unset Printing Existential Instances.
+
+Solving existential variables using tactics
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+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 ``ltac:(``\ `tacexpr`\ ``)``, 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 binding as well as those
+introduced by tactic binding. The expression `tacexpr` can be any tactic
+expression as described in :ref:`thetacticlanguage`.
+
+.. coqtop:: all
+
+   Definition foo (x : nat) : nat := ltac:(exact x).
+
+This construction is useful when one wants to define complicated terms
+using highly automated tactics without resorting to writing the proof-term
+by means of the interactive proof engine.
+
+This mechanism is comparable to the ``Declare Implicit Tactic`` command
+defined at :ref:`TODO-8.9.7-implicit-automation`, except that the used
+tactic is local to each hole instead of being declared globally.