aboutsummaryrefslogtreecommitdiff
path: root/doc/refman
diff options
context:
space:
mode:
Diffstat (limited to 'doc/refman')
-rw-r--r--doc/refman/Classes.tex2
-rw-r--r--doc/refman/Extraction.tex7
-rw-r--r--doc/refman/RefMan-cic.tex24
-rw-r--r--doc/refman/RefMan-ext.tex292
-rw-r--r--doc/refman/RefMan-gal.tex2
-rw-r--r--doc/refman/RefMan-ind.tex510
-rw-r--r--doc/refman/RefMan-ltac.tex4
-rw-r--r--doc/refman/RefMan-pro.tex34
-rw-r--r--doc/refman/RefMan-sch.tex7
-rw-r--r--doc/refman/RefMan-syn.tex98
-rw-r--r--doc/refman/RefMan-tac.tex155
-rw-r--r--doc/refman/RefMan-uti.tex39
-rw-r--r--doc/refman/Universes.tex46
13 files changed, 469 insertions, 751 deletions
diff --git a/doc/refman/Classes.tex b/doc/refman/Classes.tex
index acfc4bea93..5966ac468c 100644
--- a/doc/refman/Classes.tex
+++ b/doc/refman/Classes.tex
@@ -554,7 +554,7 @@ more efficient resolution behavior (the option is off by default). When
a solution to the typeclass goal of this class is found, we never
backtrack on it, assuming that it is canonical.
-\subsection{\tt Typeclasses eauto := [debug] [dfs | bfs] [\emph{depth}]}
+\subsection{\tt Typeclasses eauto := [debug] [(dfs) | (bfs)] [\emph{depth}]}
\comindex{Typeclasses eauto}
\label{TypeclassesEauto}
diff --git a/doc/refman/Extraction.tex b/doc/refman/Extraction.tex
index 01dbcfb1cb..fa3d61b1cd 100644
--- a/doc/refman/Extraction.tex
+++ b/doc/refman/Extraction.tex
@@ -19,6 +19,12 @@ be used (abusively) to refer to any of the three.
%% the one in previous versions of \Coq: there is no more
%% an explicit toplevel for the language (formerly called \textsc{Fml}).
+Before using any of the commands or options described in this chapter,
+the extraction framework should first be loaded explicitly
+via {\tt Require Extraction}. Note that in earlier versions of Coq, these
+commands and options were directly available without any preliminary
+{\tt Require}.
+
\asection{Generating ML code}
\comindex{Extraction}
\comindex{Recursive Extraction}
@@ -501,6 +507,7 @@ We can now extract this program to \ocaml:
Reset Initial.
\end{coq_eval}
\begin{coq_example}
+Require Extraction.
Require Import Euclid Wf_nat.
Extraction Inline gt_wf_rec lt_wf_rec induction_ltof2.
Recursive Extraction eucl_dev.
diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex
index fdd2725810..96fb1eb752 100644
--- a/doc/refman/RefMan-cic.tex
+++ b/doc/refman/RefMan-cic.tex
@@ -461,6 +461,13 @@ recursively convertible to $u'_1$, or, symmetrically, $u_2$ is $\lb
x:T\mto u'_2$ and $u_1\,x$ is recursively convertible to $u'_2$. We
then write $\WTEGCONV{t_1}{t_2}$.
+Apart from this we consider two instances of polymorphic and cumulative (see Chapter~\ref{Universes-full}) inductive types (see below)
+convertible $\WTEGCONV{t\ w_1 \dots w_m}{t\ w_1' \dots w_m'}$ if we have subtypings (see below) in both directions, i.e.,
+$\WTEGLECONV{t\ w_1 \dots w_m}{t\ w_1' \dots w_m'}$ and $\WTEGLECONV{t\ w_1' \dots w_m'}{t\ w_1 \dots w_m}$.
+Furthermore, we consider $\WTEGCONV{c\ v_1 \dots v_m}{c'\ v_1' \dots v_m'}$ convertible if $\WTEGCONV{v_i}{v_i'}$
+and we have that $c$ and $c'$ are the same constructors of different instances the same inductive types (differing only in universe levels)
+such that $\WTEG{c\ v_1 \dots v_m}{t\ w_1 \dots w_m}$ and $\WTEG{c'\ v_1' \dots v_m'}{t'\ w_1' \dots w_m'}$ and we have $\WTEGCONV{t\ w_1 \dots w_m}{t\ w_1' \dots w_m'}$.
+
The convertibility relation allows introducing a new typing rule
which says that two convertible well-formed types have the same
inhabitants.
@@ -480,6 +487,17 @@ convertibility into a {\em subtyping} relation inductively defined by:
\item $\WTEGLECONV{\Prop}{\Set}$, hence, by transitivity,
$\WTEGLECONV{\Prop}{\Type(i)}$, for any $i$
\item if $\WTEGCONV{T}{U}$ and $\WTELECONV{\Gamma::(x:T)}{T'}{U'}$ then $\WTEGLECONV{\forall~x:T, T'}{\forall~x:U, U'}$.
+\item if $\Ind{}{p}{\Gamma_I}{\Gamma_C}$ is a universe polymorphic and cumulative (see Chapter~\ref{Universes-full})
+ inductive type (see below) and $(t : \forall\Gamma_P,\forall\Gamma_{\mathit{Arr}(t)}, \Sort)\in\Gamma_I$
+ and $(t' : \forall\Gamma_P',\forall\Gamma_{\mathit{Arr}(t)}', \Sort')\in\Gamma_I$
+ are two different instances of \emph{the same} inductive type (differing only in universe levels) with constructors
+ \[[c_1: \forall\Gamma_P,\forall T_{1,1} \dots T_{1,n_1},t\ v_{1,1} \dots v_{1,m}; \dots; c_k: \forall\Gamma_P,\forall T_{k, 1} \dots T_{k,n_k},t\ v_{n,1}\dots v_{n,m}]\]
+ and
+ \[[c_1: \forall\Gamma_P',\forall T_{1,1}' \dots T_{1,n_1}',t'\ v_{1,1}' \dots v_{1,m}'; \dots; c_k: \forall\Gamma_P',\forall T_{k, 1}' \dots T_{k,n_k}',t\ v_{n,1}'\dots v_{n,m}']\]
+ respectively then $\WTEGLECONV{t\ w_1 \dots w_m}{t\ w_1' \dots w_m'}$ (notice that $t$ and $t'$ are both fully applied, i.e., they have a sort as a type)
+ if $\WTEGCONV{w_i}{w_i'}$ for $1 \le i \le m$ and we have
+ \[ \WTEGLECONV{T_{i,j}}{T_{i,j}'} \text{ and } \WTEGLECONV{A_i}{A_i'}\]
+ where $\Gamma_{\mathit{Arr}(t)} = [a_1 : A_1; a_1 : A_l]$ and $\Gamma_{\mathit{Arr}(t)} = [a_1 : A_1'; a_1 : A_l']$.
\end{enumerate}
The conversion rule up to subtyping is now exactly:
@@ -530,8 +548,12 @@ Formally, we can represent any {\em inductive definition\index{definition!induct
These inductive definitions, together with global assumptions and global definitions, then form the global environment.
%
Additionally, for any $p$ there always exists $\Gamma_P=[a_1:A_1;\dots;a_p:A_p]$
-such that each $(t:T)\in\Gamma_I\cup\Gamma_C$ can be written as:
+such that each $T$ in $(t:T)\in\Gamma_I\cup\Gamma_C$ can be written as:
$\forall\Gamma_P, T^\prime$ where $\Gamma_P$ is called the {\em context of parameters\index{context of parameters}}.
+Furthermore, we must have that each $T$ in $(t:T)\in\Gamma_I$ can be written as:
+$\forall\Gamma_P,\forall\Gamma_{\mathit{Arr}(t)}, \Sort$ where $\Gamma_{\mathit{Arr}(t)}$ is called the
+{\em Arity} of the inductive type\index{arity of inductive type} $t$ and
+$\Sort$ is called the sort of the inductive type $t$.
\paragraph{Examples}
diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex
index 6dd0ddf81d..713f344cbe 100644
--- a/doc/refman/RefMan-ext.tex
+++ b/doc/refman/RefMan-ext.tex
@@ -38,21 +38,19 @@ construction allows defining ``signatures''.
\end{figure}
\noindent In the expression
-
-\smallskip
-{\tt Record} {\ident} {\params} \texttt{:}
- {\sort} := {\ident$_0$} \verb+{+
- {\ident$_1$} \binders$_1$ \texttt{:} {\term$_1$};
- \dots
- {\ident$_n$} \binders$_n$ \texttt{:} {\term$_n$} \verb+}+.
-\smallskip
-
+\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$}, ..,
-{\ident$_n$} are the names of fields and {\tt forall} \binders$_1${\tt ,} {\term$_1$}, ..., {\tt forall} \binders$_n${\tt ,} {\term$_n$}
+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
@@ -82,26 +80,15 @@ Record Rat : Set := mkRat
forall x y z:nat, (x * y) = top /\ (x * z) = bottom -> x = 1}.
\end{coq_example}
-Remark here that the field
-\verb+Rat_cond+ depends on the field \verb+bottom+.
-
-%Let us now see the work done by the {\tt Record} macro.
-%First the macro generates an inductive definition
-%with just one constructor:
-%
-%\medskip
-%\noindent
-%{\tt Inductive {\ident} \zeroone{\binders} : {\sort} := \\
-%\mbox{}\hspace{0.4cm} {\ident$_0$} : forall ({\ident$_1$}:{\term$_1$}) ..
-%({\ident$_n$}:{\term$_n$}), {\ident} {\rm\sl params}.}
-%\medskip
+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} :=} \\
-\qquad {\tt
- {\ident$_0$} ({\ident$_1$}:{\term$_1$}) .. ({\ident$_n$}:{\term$_n$}).}
+{\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
@@ -109,28 +96,9 @@ the record.
As an example, let us define the rational $1/2$:
\begin{coq_example*}
-Require Import Arith.
Theorem one_two_irred :
forall x y z:nat, x * y = 1 /\ x * z = 2 -> x = 1.
-\end{coq_example*}
-\begin{coq_eval}
-Lemma mult_m_n_eq_m_1 : forall m n:nat, m * n = 1 -> m = 1.
-destruct m; trivial.
-intros; apply f_equal with (f := S).
-destruct m; trivial.
-destruct n; simpl in H.
- rewrite <- mult_n_O in H.
- discriminate.
- rewrite <- plus_n_Sm in H.
- discriminate.
-Qed.
-
-intros x y z [H1 H2].
- apply mult_m_n_eq_m_1 with (n := y); trivial.
-\end{coq_eval}
-\ldots
-\begin{coq_example*}
-Qed.
+Admitted.
\end{coq_example*}
\begin{coq_example}
Definition half := mkRat true 1 2 (O_S 1) one_two_irred.
@@ -139,80 +107,6 @@ Definition half := mkRat true 1 2 (O_S 1) one_two_irred.
Check half.
\end{coq_example}
-The macro generates also, when it is possible, the projection
-functions for destructuring an object of type {\ident}. These
-projection functions have the same name that 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 half.(top).
-Eval compute in half.(bottom).
-Eval compute in half.(Rat_bottom_cond).
-\end{coq_example}
-\begin{coq_eval}
-Reset Initial.
-\end{coq_eval}
-
-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.
-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}).
-
-\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.
-
-\Rem {\tt Structure} is a synonym of the keyword {\tt Record}.
-
-\Rem Creation of an object of record type can be done by calling {\ident$_0$}
-and passing arguments in the correct order.
-
-\begin{coq_example}
-Record point := { x : nat; y : nat }.
-Definition a := Build_point 5 3.
-\end{coq_example}
-
\begin{figure}[t]
\begin{centerframe}
\begin{tabular}{lcl}
@@ -226,15 +120,17 @@ Definition a := Build_point 5 3.
\label{fig:fieldsyntax}
\end{figure}
-A syntax is available for creating objects by using named fields, as
+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 b := {| x := 5; y := 3 |}.
-Definition c := {| y := 3; x := 5 |}.
+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
@@ -256,23 +152,52 @@ This syntax can also be used for pattern matching.
\begin{coq_example}
Eval compute in (
- match b with
- | {| y := S n |} => n
+ match half with
+ | {| sign := true; top := n |} => n
| _ => 0
end).
\end{coq_example}
-\begin{coq_eval}
-Reset Initial.
-\end{coq_eval}
+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}
-\Rem A syntax for projections based on a dot notation is
-available. The command to activate it is
+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}
@@ -285,18 +210,66 @@ available. The command to activate it is
\label{fig:projsyntax}
\end{figure}
-The corresponding grammar rules are given 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{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}.
-To deactivate the printing of projections, use
-{\tt Unset Printing Projections}.
+\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}
@@ -721,29 +694,31 @@ a given type. See Section~\ref{Show}.
\section{Advanced recursive functions}
-The \emph{experimental} command
+The following \emph{experimental} command is available
+when the {\tt FunInd} library has been loaded via {\tt Require Import FunInd}:
\begin{center}
\texttt{Function {\ident} {\binder$_1$}\ldots{\binder$_n$}
\{decrease\_annot\} : type$_0$ := \term$_0$}
\comindex{Function}
\label{Function}
\end{center}
-can be seen as a generalization of {\tt Fixpoint}. It is actually a
-wrapper for several ways of defining a function \emph{and other useful
+This command can be seen as a generalization of {\tt Fixpoint}. It is actually
+a wrapper for several ways of defining a function \emph{and other useful
related objects}, namely: an induction principle that reflects the
-recursive structure of the function (see \ref{FunInduction}), and its
-fixpoint equality. The meaning of this
+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 must not
-necessary be \emph{structurally} decreasing. The point of the {\tt
+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 enjoys also the {\tt with} extension
+The {\tt Function} construction also enjoys the {\tt with} extension
to define mutually recursive definitions. However, this feature does
-not work for non structural recursive functions. % VRAI??
+not work for non structurally recursive functions. % VRAI??
See the documentation of {\tt functional induction}
(see Section~\ref{FunInduction}) and {\tt Functional Scheme}
@@ -774,7 +749,7 @@ Function plus (n m : nat) {struct n} : nat :=
\end{coq_example*}
\paragraph[Limitations]{Limitations\label{sec:Function-limitations}}
-\term$_0$ must be build as a \emph{pure pattern-matching tree}
+\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.
@@ -801,7 +776,7 @@ For now dependent cases are not treated for non structurally terminating functio
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.
+ the ident is defined; the induction scheme will not be generated.
This error happens generally when:
@@ -873,14 +848,14 @@ the following:
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
+ 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
+ \term$_0$. The order must be well founded. Parameters of the
function are bound in \term$_0$.
\end{itemize}
@@ -2009,6 +1984,11 @@ Check (fun x y => _) 0 1.
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}}
diff --git a/doc/refman/RefMan-gal.tex b/doc/refman/RefMan-gal.tex
index 3814e4403a..71977d3e9d 100644
--- a/doc/refman/RefMan-gal.tex
+++ b/doc/refman/RefMan-gal.tex
@@ -3,7 +3,7 @@
\label{BNF-syntax} % Used referred to as a chapter label
This chapter describes \gallina, the specification language of {\Coq}.
-It allows developing mathematical theories and to prove specifications
+It allows developing mathematical theories and proofs of specifications
of programs. The theories are built from axioms, hypotheses,
parameters, lemmas, theorems and definitions of constants, functions,
predicates and sets. The syntax of logical objects involved in
diff --git a/doc/refman/RefMan-ind.tex b/doc/refman/RefMan-ind.tex
deleted file mode 100644
index 43bd2419f0..0000000000
--- a/doc/refman/RefMan-ind.tex
+++ /dev/null
@@ -1,510 +0,0 @@
-
-%\documentstyle[11pt]{article}
-%\input{title}
-
-%\include{macros}
-%\makeindex
-
-%\begin{document}
-%\coverpage{The module {\tt Equality}}{Cristina CORNES}
-
-%\tableofcontents
-
-\chapter[Tactics for inductive types and families]{Tactics for inductive types and families\label{Addoc-equality}}
-
-This chapter details a few special tactics useful for inferring facts
-from inductive hypotheses. They can be considered as tools that
-macro-generate complicated uses of the basic elimination tactics for
-inductive types.
-
-Sections \ref{inversion_introduction} to \ref{inversion_using} present
-inversion tactics and Section~\ref{scheme} describes
-a command {\tt Scheme} for automatic generation of induction schemes
-for mutual inductive types.
-
-%\end{document}
-%\documentstyle[11pt]{article}
-%\input{title}
-
-%\begin{document}
-%\coverpage{Module Inv: Inversion Tactics}{Cristina CORNES}
-
-\section[Generalities about inversion]{Generalities about inversion\label{inversion_introduction}}
-When working with (co)inductive predicates, we are very often faced to
-some of these situations:
-\begin{itemize}
-\item we have an inconsistent instance of an inductive predicate in the
- local context of hypotheses. Thus, the current goal can be trivially
- proved by absurdity.
-
-\item we have a hypothesis that is an instance of an inductive
- predicate, and the instance has some variables whose constraints we
- would like to derive.
-\end{itemize}
-
-The inversion tactics are very useful to simplify the work in these
-cases. Inversion tools can be classified in three groups:
-\begin{enumerate}
-\item tactics for inverting an instance without stocking the inversion
- lemma in the context:
- (\texttt{Dependent}) \texttt{Inversion} and
- (\texttt{Dependent}) \texttt{Inversion\_clear}.
-\item commands for generating and stocking in the context the inversion
- lemma corresponding to an instance: \texttt{Derive}
- (\texttt{Dependent}) \texttt{Inversion}, \texttt{Derive}
- (\texttt{Dependent}) \texttt{Inversion\_clear}.
-\item tactics for inverting an instance using an already defined
- inversion lemma: \texttt{Inversion \ldots using}.
-\end{enumerate}
-
-These tactics work for inductive types of arity $(\vec{x}:\vec{T})s$
-where $s \in \{Prop,Set,Type\}$. Sections \ref{inversion_primitive},
-\ref{inversion_derivation} and \ref{inversion_using}
-describe respectively each group of tools.
-
-As inversion proofs may be large in size, we recommend the user to
-stock the lemmas whenever the same instance needs to be inverted
-several times.\\
-
-Let's consider the relation \texttt{Le} over natural numbers and the
-following variables:
-
-\begin{coq_eval}
-Restore State "Initial".
-\end{coq_eval}
-
-\begin{coq_example*}
-Inductive Le : nat -> nat -> Set :=
- | LeO : forall n:nat, Le 0%N n
- | LeS : forall n m:nat, Le n m -> Le (S n) (S m).
-Variable P : nat -> nat -> Prop.
-Variable Q : forall n m:nat, Le n m -> Prop.
-\end{coq_example*}
-
-For example purposes we defined \verb+Le: nat->nat->Set+
- but we may have defined
-it \texttt{Le} of type \verb+nat->nat->Prop+ or \verb+nat->nat->Type+.
-
-
-\section[Inverting an instance]{Inverting an instance\label{inversion_primitive}}
-\subsection{The non dependent case}
-\begin{itemize}
-
-\item \texttt{Inversion\_clear} \ident~\\
-\index{Inversion-clear@{\tt Inversion\_clear}}
- Let the type of \ident~ in the local context be $(I~\vec{t})$,
- where $I$ is a (co)inductive predicate. Then,
- \texttt{Inversion} applied to \ident~ derives for each possible
- constructor $c_i$ of $(I~\vec{t})$, {\bf all} the necessary
- conditions that should hold for the instance $(I~\vec{t})$ to be
- proved by $c_i$. Finally it erases \ident~ from the context.
-
-
-
-For example, consider the goal:
-\begin{coq_eval}
-Lemma ex : forall n m:nat, Le (S n) m -> P n m.
-intros.
-\end{coq_eval}
-
-\begin{coq_example}
-Show.
-\end{coq_example}
-
-To prove the goal we may need to reason by cases on \texttt{H} and to
- derive that \texttt{m} is necessarily of
-the form $(S~m_0)$ for certain $m_0$ and that $(Le~n~m_0)$.
-Deriving these conditions corresponds to prove that the
-only possible constructor of \texttt{(Le (S n) m)} is
-\texttt{LeS} and that we can invert the
-\texttt{->} in the type of \texttt{LeS}.
-This inversion is possible because \texttt{Le} is the smallest set closed by
-the constructors \texttt{LeO} and \texttt{LeS}.
-
-
-\begin{coq_example}
-inversion_clear H.
-\end{coq_example}
-
-Note that \texttt{m} has been substituted in the goal for \texttt{(S m0)}
-and that the hypothesis \texttt{(Le n m0)} has been added to the
-context.
-
-\item \texttt{Inversion} \ident~\\
-\index{Inversion@{\tt Inversion}}
- This tactic differs from {\tt Inversion\_clear} in the fact that
- it adds the equality constraints in the context and
- it does not erase the hypothesis \ident.
-
-
-In the previous example, {\tt Inversion\_clear}
-has substituted \texttt{m} by \texttt{(S m0)}. Sometimes it is
-interesting to have the equality \texttt{m=(S m0)} in the
-context to use it after. In that case we can use \texttt{Inversion} that
-does not clear the equalities:
-
-\begin{coq_example*}
-Undo.
-\end{coq_example*}
-\begin{coq_example}
-inversion H.
-\end{coq_example}
-
-\begin{coq_eval}
-Undo.
-\end{coq_eval}
-
-Note that the hypothesis \texttt{(S m0)=m} has been deduced and
-\texttt{H} has not been cleared from the context.
-
-\end{itemize}
-
-\begin{Variants}
-
-\item \texttt{Inversion\_clear } \ident~ \texttt{in} \ident$_1$ \ldots
- \ident$_n$\\
-\index{Inversion_clear...in@{\tt Inversion\_clear...in}}
- Let \ident$_1$ \ldots \ident$_n$, be identifiers in the local context. This
- tactic behaves as generalizing \ident$_1$ \ldots \ident$_n$, and then performing
- {\tt Inversion\_clear}.
-
-\item \texttt{Inversion } \ident~ \texttt{in} \ident$_1$ \ldots \ident$_n$\\
-\index{Inversion ... in@{\tt Inversion ... in}}
- Let \ident$_1$ \ldots \ident$_n$, be identifiers in the local context. This
- tactic behaves as generalizing \ident$_1$ \ldots \ident$_n$, and then performing
- \texttt{Inversion}.
-
-
-\item \texttt{Simple Inversion} \ident~ \\
-\index{Simple Inversion@{\tt Simple Inversion}}
- It is a very primitive inversion tactic that derives all the necessary
- equalities but it does not simplify
- the constraints as \texttt{Inversion} and
- {\tt Inversion\_clear} do.
-
-\end{Variants}
-
-
-\subsection{The dependent case}
-\begin{itemize}
-\item \texttt{Dependent Inversion\_clear} \ident~\\
-\index{Dependent Inversion-clear@{\tt Dependent Inversion\_clear}}
- Let the type of \ident~ in the local context be $(I~\vec{t})$,
- where $I$ is a (co)inductive predicate, and let the goal depend both on
- $\vec{t}$ and \ident. Then,
- \texttt{Dependent Inversion\_clear} applied to \ident~ derives
- for each possible constructor $c_i$ of $(I~\vec{t})$, {\bf all} the
- necessary conditions that should hold for the instance $(I~\vec{t})$ to be
- proved by $c_i$. It also substitutes \ident~ for the corresponding
- term in the goal and it erases \ident~ from the context.
-
-
-For example, consider the goal:
-\begin{coq_eval}
-Lemma ex_dep : forall (n m:nat) (H:Le (S n) m), Q (S n) m H.
-intros.
-\end{coq_eval}
-
-\begin{coq_example}
-Show.
-\end{coq_example}
-
-As \texttt{H} occurs in the goal, we may want to reason by cases on its
-structure and so, we would like inversion tactics to
-substitute \texttt{H} by the corresponding term in constructor form.
-Neither \texttt{Inversion} nor {\tt Inversion\_clear} make such a
-substitution. To have such a behavior we use the dependent inversion tactics:
-
-\begin{coq_example}
-dependent inversion_clear H.
-\end{coq_example}
-
-Note that \texttt{H} has been substituted by \texttt{(LeS n m0 l)} and
-\texttt{m} by \texttt{(S m0)}.
-
-
-\end{itemize}
-
-\begin{Variants}
-
-\item \texttt{Dependent Inversion\_clear } \ident~ \texttt{ with } \term\\
-\index{Dependent Inversion_clear...with@{\tt Dependent Inversion\_clear...with}}
- \noindent Behaves as \texttt{Dependent Inversion\_clear} but allows giving
- explicitly the good generalization of the goal. It is useful when
- the system fails to generalize the goal automatically. If
- \ident~ has type $(I~\vec{t})$ and $I$ has type
- $(\vec{x}:\vec{T})s$, then \term~ must be of type
- $I:(\vec{x}:\vec{T})(I~\vec{x})\rightarrow s'$ where $s'$ is the
- type of the goal.
-
-
-
-\item \texttt{Dependent Inversion} \ident~\\
-\index{Dependent Inversion@{\tt Dependent Inversion}}
- This tactic differs from \texttt{Dependent Inversion\_clear} in the fact that
- it also adds the equality constraints in the context and
- it does not erase the hypothesis \ident~.
-
-\item \texttt{Dependent Inversion } \ident~ \texttt{ with } \term \\
-\index{Dependent Inversion...with@{\tt Dependent Inversion...with}}
- Analogous to \texttt{Dependent Inversion\_clear .. with..} above.
-\end{Variants}
-
-
-
-\section[Deriving the inversion lemmas]{Deriving the inversion lemmas\label{inversion_derivation}}
-\subsection{The non dependent case}
-
-The tactics (\texttt{Dependent}) \texttt{Inversion} and (\texttt{Dependent})
-{\tt Inversion\_clear} work on a
-certain instance $(I~\vec{t})$ of an inductive predicate. At each
-application, they inspect the given instance and derive the
-corresponding inversion lemma. If we have to invert the same
-instance several times it is recommended to stock the lemma in the
-context and to reuse it whenever we need it.
-
-The families of commands \texttt{Derive Inversion}, \texttt{Derive
-Dependent Inversion}, \texttt{Derive} \\ {\tt Inversion\_clear} and \texttt{Derive Dependent Inversion\_clear}
-allow to generate inversion lemmas for given instances and sorts. Next
-section describes the tactic \texttt{Inversion}$\ldots$\texttt{using} that refines the
-goal with a specified inversion lemma.
-
-\begin{itemize}
-
-\item \texttt{Derive Inversion\_clear} \ident~ \texttt{with}
- $(\vec{x}:\vec{T})(I~\vec{t})$ \texttt{Sort} \sort~ \\
-\index{Derive Inversion_clear...with@{\tt Derive Inversion\_clear...with}}
- Let $I$ be an inductive predicate and $\vec{x}$ the variables
- occurring in $\vec{t}$. This command generates and stocks
- the inversion lemma for the sort \sort~ corresponding to the instance
- $(\vec{x}:\vec{T})(I~\vec{t})$ with the name \ident~ in the {\bf
- global} environment. When applied it is equivalent to have
- inverted the instance with the tactic {\tt Inversion\_clear}.
-
-
- For example, to generate the inversion lemma for the instance
- \texttt{(Le (S n) m)} and the sort \texttt{Prop} we do:
-\begin{coq_example}
-Derive Inversion_clear leminv with (forall n m:nat, Le (S n) m) Sort
- Prop.
-\end{coq_example}
-
-Let us inspect the type of the generated lemma:
-\begin{coq_example}
-Check leminv.
-\end{coq_example}
-
-
-
-\end{itemize}
-
-%\variants
-%\begin{enumerate}
-%\item \verb+Derive Inversion_clear+ \ident$_1$ \ident$_2$ \\
-%\index{Derive Inversion_clear@{\tt Derive Inversion\_clear}}
-% Let \ident$_1$ have type $(I~\vec{t})$ in the local context ($I$
-% an inductive predicate). Then, this command has the same semantics
-% as \verb+Derive Inversion_clear+ \ident$_2$~ \verb+with+
-% $(\vec{x}:\vec{T})(I~\vec{t})$ \verb+Sort Prop+ where $\vec{x}$ are the free
-% variables of $(I~\vec{t})$ declared in the local context (variables
-% of the global context are considered as constants).
-%\item \verb+Derive Inversion+ \ident$_1$~ \ident$_2$~\\
-%\index{Derive Inversion@{\tt Derive Inversion}}
-% Analogous to the previous command.
-%\item \verb+Derive Inversion+ $num$ \ident~ \ident~ \\
-%\index{Derive Inversion@{\tt Derive Inversion}}
-% This command behaves as \verb+Derive Inversion+ \ident~ {\it
-% namehyp} performed on the goal number $num$.
-%
-%\item \verb+Derive Inversion_clear+ $num$ \ident~ \ident~ \\
-%\index{Derive Inversion_clear@{\tt Derive Inversion\_clear}}
-% This command behaves as \verb+Derive Inversion_clear+ \ident~
-% \ident~ performed on the goal number $num$.
-%\end{enumerate}
-
-
-
-A derived inversion lemma is adequate for inverting the instance
-with which it was generated, \texttt{Derive} applied to
-different instances yields different lemmas. In general, if we generate
-the inversion lemma with
-an instance $(\vec{x}:\vec{T})(I~\vec{t})$ and a sort $s$, the inversion lemma will
-expect a predicate of type $(\vec{x}:\vec{T})s$ as first argument. \\
-
-\begin{Variant}
-\item \texttt{Derive Inversion} \ident~ \texttt{with}
- $(\vec{x}:\vec{T})(I~\vec{t})$ \texttt{Sort} \sort\\
-\index{Derive Inversion...with@{\tt Derive Inversion...with}}
- Analogous of \texttt{Derive Inversion\_clear .. with ..} but
- when applied it is equivalent to having
- inverted the instance with the tactic \texttt{Inversion}.
-\end{Variant}
-
-\subsection{The dependent case}
-\begin{itemize}
-\item \texttt{Derive Dependent Inversion\_clear} \ident~ \texttt{with}
- $(\vec{x}:\vec{T})(I~\vec{t})$ \texttt{Sort} \sort~ \\
-\index{Derive Dependent Inversion\_clear...with@{\tt Derive Dependent Inversion\_clear...with}}
- Let $I$ be an inductive predicate. This command generates and stocks
- the dependent inversion lemma for the sort \sort~ corresponding to the instance
- $(\vec{x}:\vec{T})(I~\vec{t})$ with the name \ident~ in the {\bf
- global} environment. When applied it is equivalent to having
- inverted the instance with the tactic \texttt{Dependent Inversion\_clear}.
-\end{itemize}
-
-\begin{coq_example}
-Derive Dependent Inversion_clear leminv_dep with
- (forall n m:nat, Le (S n) m) Sort Prop.
-\end{coq_example}
-
-\begin{coq_example}
-Check leminv_dep.
-\end{coq_example}
-
-\begin{Variants}
-\item \texttt{Derive Dependent Inversion} \ident~ \texttt{with}
- $(\vec{x}:\vec{T})(I~\vec{t})$ \texttt{Sort} \sort~ \\
-\index{Derive Dependent Inversion...with@{\tt Derive Dependent Inversion...with}}
- Analogous to \texttt{Derive Dependent Inversion\_clear}, but when
- applied it is equivalent to having
- inverted the instance with the tactic \texttt{Dependent Inversion}.
-
-\end{Variants}
-
-\section[Using already defined inversion lemmas]{Using already defined inversion lemmas\label{inversion_using}}
-\begin{itemize}
-\item \texttt{Inversion} \ident \texttt{ using} \ident$'$ \\
-\index{Inversion...using@{\tt Inversion...using}}
- Let \ident~ have type $(I~\vec{t})$ ($I$ an inductive
- predicate) in the local context, and \ident$'$ be a (dependent) inversion
- lemma. Then, this tactic refines the current goal with the specified
- lemma.
-
-
-\begin{coq_eval}
-Abort.
-\end{coq_eval}
-
-\begin{coq_example}
-Show.
-\end{coq_example}
-\begin{coq_example}
-inversion H using leminv.
-\end{coq_example}
-
-
-\end{itemize}
-\variant
-\begin{enumerate}
-\item \texttt{Inversion} \ident~ \texttt{using} \ident$'$ \texttt{in} \ident$_1$\ldots \ident$_n$\\
-\index{Inversion...using...in@{\tt Inversion...using...in}}
-This tactic behaves as generalizing \ident$_1$\ldots \ident$_n$,
-then doing \texttt{Use Inversion} \ident~\ident$'$.
-\end{enumerate}
-
-\section[\tt Scheme ...]{\tt Scheme ...\index{Scheme@{\tt Scheme}}\label{Scheme}
-\label{scheme}}
-The {\tt Scheme} command is a high-level tool for generating
-automatically (possibly mutual) induction principles for given types
-and sorts. Its syntax follows the schema :
-
-\noindent
-{\tt Scheme {\ident$_1$} := Induction for \term$_1$ Sort {\sort$_1$} \\
- with\\
- \mbox{}\hspace{0.1cm} .. \\
- with {\ident$_m$} := Induction for {\term$_m$} Sort
- {\sort$_m$}}\\
-\term$_1$ \ldots \term$_m$ are different inductive types belonging to
-the same package of mutual inductive definitions. This command
-generates {\ident$_1$}\ldots{\ident$_m$} to be mutually recursive
-definitions. Each term {\ident$_i$} proves a general principle
-of mutual induction for objects in type {\term$_i$}.
-
-\Example
-The definition of principle of mutual induction for {\tt tree} and
-{\tt forest} over the sort {\tt Set} is defined by the command:
-\begin{coq_eval}
-Restore State "Initial".
-Variables A B : Set.
-Inductive tree : Set :=
- node : A -> forest -> tree
-with forest : Set :=
- | leaf : B -> forest
- | cons : tree -> forest -> forest.
-\end{coq_eval}
-\begin{coq_example*}
-Scheme tree_forest_rec := Induction for tree
- Sort Set
- with forest_tree_rec := Induction for forest Sort Set.
-\end{coq_example*}
-You may now look at the type of {\tt tree\_forest\_rec} :
-\begin{coq_example}
-Check tree_forest_rec.
-\end{coq_example}
-This principle involves two different predicates for {\tt trees} and
-{\tt forests}; it also has three premises each one corresponding to a
-constructor of one of the inductive definitions.
-
-The principle {\tt tree\_forest\_rec} shares exactly the same
-premises, only the conclusion now refers to the property of forests.
-\begin{coq_example}
-Check forest_tree_rec.
-\end{coq_example}
-
-\begin{Variant}
-\item {\tt Scheme {\ident$_1$} := Minimality for \term$_1$ Sort {\sort$_1$} \\
- with\\
- \mbox{}\hspace{0.1cm} .. \\
- with {\ident$_m$} := Minimality for {\term$_m$} Sort
- {\sort$_m$}}\\
-Same as before but defines a non-dependent elimination principle more
-natural in case of inductively defined relations.
-\end{Variant}
-
-\Example
-With the predicates {\tt odd} and {\tt even} inductively defined as:
-% \begin{coq_eval}
-% Restore State "Initial".
-% \end{coq_eval}
-\begin{coq_example*}
-Inductive odd : nat -> Prop :=
- oddS : forall n:nat, even n -> odd (S n)
-with even : nat -> Prop :=
- | evenO : even 0%N
- | evenS : forall n:nat, odd n -> even (S n).
-\end{coq_example*}
-The following command generates a powerful elimination
-principle:
-\begin{coq_example*}
-Scheme odd_even := Minimality for odd Sort Prop
- with even_odd := Minimality for even Sort Prop.
-\end{coq_example*}
-The type of {\tt odd\_even} for instance will be:
-\begin{coq_example}
-Check odd_even.
-\end{coq_example}
-The type of {\tt even\_odd} shares the same premises but the
-conclusion is {\tt (n:nat)(even n)->(Q n)}.
-
-\subsection[\tt Combined Scheme ...]{\tt Combined Scheme ...\index{CombinedScheme@{\tt Combined Scheme}}\label{CombinedScheme}
-\label{combinedscheme}}
-The {\tt Combined Scheme} command is a tool for combining
-induction principles generated by the {\tt Scheme} command.
-Its syntax follows the schema :
-
-\noindent
-{\tt Combined Scheme {\ident$_0$} from {\ident$_1$}, .., {\ident$_n$}}\\
-\ident$_1$ \ldots \ident$_n$ are different inductive principles that must belong to
-the same package of mutual inductive principle definitions. This command
-generates {\ident$_0$} to be the conjunction of the principles: it is
-build from the common premises of the principles and concluded by the
-conjunction of their conclusions. For exemple, we can combine the
-induction principles for trees and forests:
-
-\begin{coq_example*}
-Combined Scheme tree_forest_mutind from tree_ind, forest_ind.
-Check tree_forest_mutind.
-\end{coq_example*}
-
-%\end{document}
-
diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex
index bb679ecba7..f3bc2dd05e 100644
--- a/doc/refman/RefMan-ltac.tex
+++ b/doc/refman/RefMan-ltac.tex
@@ -392,7 +392,7 @@ all selected goals.
\item{} [{\ident}] {\tt :} {\tacexpr}
In this variant, {\tacexpr} is applied locally to a goal
- previously named by the user.
+ previously named by the user (see~\ref{ExistentialVariables}).
\item {\num} {\tt :} {\tacexpr}
@@ -891,7 +891,7 @@ behavior can be retrieved with the {\tt Tactic Compat Context} flag.
\end{Variants}
-\subsubsection[Pattern matching on goals]{Pattern matching on goals\index{Ltac!match goal@\texttt{match goal}}
+\subsubsection[Pattern matching on goals]{Pattern matching on goals\index{Ltac!match goal@\texttt{match goal}}\label{ltac-match-goal}
\index{Ltac!match reverse goal@\texttt{match reverse goal}}
\index{match goal@\texttt{match goal}!in Ltac}
\index{match reverse goal@\texttt{match reverse goal}!in Ltac}}
diff --git a/doc/refman/RefMan-pro.tex b/doc/refman/RefMan-pro.tex
index 0760d716e3..95fee3241c 100644
--- a/doc/refman/RefMan-pro.tex
+++ b/doc/refman/RefMan-pro.tex
@@ -421,28 +421,30 @@ This command displays the current goals.
\item \errindex{No focused proof}
\end{ErrMsgs}
+\item {\tt Show {\ident}.}\\
+ Displays the named goal {\ident}.
+ This is useful in particular to display a shelved goal but only works
+ if the corresponding existential variable has been named by the user
+ (see~\ref{ExistentialVariables}) as in the following example.
+
+\begin{coq_eval}
+Reset Initial.
+\end{coq_eval}
+
+\begin{coq_example*}
+Goal exists n, n = 0.
+ eexists ?[n].
+\end{coq_example*}
+\begin{coq_example}
+ Show n.
+\end{coq_example}
+
\item {\tt Show Script.}\comindex{Show Script}\\
Displays the whole list of tactics applied from the beginning
of the current proof.
This tactics script may contain some holes (subgoals not yet proved).
They are printed under the form \verb!<Your Tactic Text here>!.
-%% \item {\tt Show Tree.}\comindex{Show Tree}\\
-%% This command can be seen as a more structured way of
-%% displaying the state of the proof than that
-%% provided by {\tt Show Script}. Instead of just giving
-%% the list of tactics that have been applied, it
-%% shows the derivation tree constructed by then.
-%% Each node of the tree contains the conclusion
-%% of the corresponding sub-derivation (i.e. a
-%% goal with its corresponding local context) and
-%% the tactic that has generated all the
-%% sub-derivations. The leaves of this tree are
-%% the goals which still remain to be proved.
-
-%\item {\tt Show Node}\comindex{Show Node}\\
-% Not yet documented
-
\item {\tt Show Proof.}\comindex{Show Proof}\\
It displays the proof term generated by the
tactics that have been applied.
diff --git a/doc/refman/RefMan-sch.tex b/doc/refman/RefMan-sch.tex
index 53aa6b86ab..d3719bed46 100644
--- a/doc/refman/RefMan-sch.tex
+++ b/doc/refman/RefMan-sch.tex
@@ -196,8 +196,10 @@ Check tree_forest_mutind.
The {\tt Functional Scheme} command is a high-level experimental
tool for generating automatically induction principles
-corresponding to (possibly mutually recursive) functions. Its
-syntax follows the schema:
+corresponding to (possibly mutually recursive) functions.
+First, it must be made available via {\tt Require Import FunInd}.
+ Its
+syntax then follows the schema:
\begin{quote}
{\tt Functional Scheme {\ident$_1$} := Induction for \ident'$_1$ Sort {\sort$_1$} \\
with\\
@@ -319,6 +321,7 @@ of a tree or a forest. Note that we use \texttt{Function} which
generally produces better principles.
\begin{coq_example*}
+Require Import FunInd.
Function tree_size (t:tree) : nat :=
match t with
| node A f => S (forest_size f)
diff --git a/doc/refman/RefMan-syn.tex b/doc/refman/RefMan-syn.tex
index ecaf82806e..084317776b 100644
--- a/doc/refman/RefMan-syn.tex
+++ b/doc/refman/RefMan-syn.tex
@@ -13,7 +13,7 @@ described in Section~\ref{scopes}.
were present for a while in {\Coq} are no longer available from {\Coq}
version 8.0. The underlying AST structure is also no longer available.
The functionalities of the command {\tt Syntactic Definition} are
-still available, see Section~\ref{Abbreviations}.
+still available; see Section~\ref{Abbreviations}.
\section[Notations]{Notations\label{Notation}
\comindex{Notation}}
@@ -35,8 +35,8 @@ The expression \texttt{(and A B)} is the abbreviated term and the
string \verb="A /\ B"= (called a {\em notation}) tells how it is
symbolically written.
-A notation is always surrounded by double quotes (excepted when the
-abbreviation is a single identifier, see \ref{Abbreviations}). The
+A notation is always surrounded by double quotes (except when the
+abbreviation is a single identifier; see \ref{Abbreviations}). The
notation is composed of {\em tokens} separated by spaces. Identifiers
in the string (such as \texttt{A} and \texttt{B}) are the {\em
parameters} of the notation. They must occur at least once each in the
@@ -68,7 +68,7 @@ declaration of the notation.
\subsection[Precedences and associativity]{Precedences and associativity\index{Precedences}
\index{Associativity}}
-Mixing different symbolic notations in a same text may cause serious
+Mixing different symbolic notations in the same text may cause serious
parsing ambiguity. To deal with the ambiguity of notations, {\Coq}
uses precedence levels ranging from 0 to 100 (plus one extra level
numbered 200) and associativity rules.
@@ -88,8 +88,8 @@ precedence level to each notation, knowing that a lower level binds
more than a higher level. Hence the level for disjunction must be
higher than the level for conjunction.
-Since connectives are the less tight articulation points of a text, it
-is reasonable to choose levels not so far from the higher level which
+Since connectives are not tight articulation points of a text, it
+is reasonable to choose levels not so far from the highest level which
is 100, for example 85 for disjunction and 80 for
conjunction\footnote{which are the levels effectively chosen in the
current implementation of {\Coq}}.
@@ -102,10 +102,10 @@ even consider that the expression is not well-formed and that
parentheses are mandatory (this is a ``no associativity'')\footnote{
{\Coq} accepts notations declared as no associative but the parser on
which {\Coq} is built, namely {\camlpppp}, currently does not implement the
-no-associativity and replace it by a left associativity; hence it is
+no-associativity and replaces it by a left associativity; hence it is
the same for {\Coq}: no-associativity is in fact left associativity}.
We don't know of a special convention of the associativity of
-disjunction and conjunction, let's apply for instance a right
+disjunction and conjunction, so let's apply for instance a right
associativity (which is the choice of {\Coq}).
Precedence levels and associativity rules of notations have to be
@@ -701,11 +701,11 @@ Notation}.
% Introduction
An {\em interpretation scope} is a set of notations for terms with
-their interpretation. Interpretation scopes provides with a weak,
-purely syntactical form of notations overloading: a same notation, for
-instance the infix symbol \verb=+= can be used to denote distinct
-definitions of an additive operator. Depending on which interpretation
-scopes is currently open, the interpretation is different.
+their interpretation. Interpretation scopes provide a weak,
+purely syntactical form of notation overloading: the same notation, for
+instance the infix symbol \verb=+=, can be used to denote distinct
+definitions of the additive operator. Depending on which interpretation
+scope is currently open, the interpretation is different.
Interpretation scopes can include an interpretation for
numerals and strings. However, this is only made possible at the
{\ocaml} level.
@@ -889,7 +889,8 @@ statically. For instance, if {\tt f} is a polymorphic function of type
recognized as an argument to be interpreted in scope {\scope}.
\comindex{Bind Scope}
-More generally, any {\class} (see Chapter~\ref{Coercions-full}) can be
+\label{bindscope}
+More generally, any coercion {\class} (see Chapter~\ref{Coercions-full}) can be
bound to an interpretation scope. The command to do it is
\begin{quote}
{\tt Bind Scope} {\scope} \texttt{with} {\class}
@@ -908,7 +909,7 @@ Open Scope nat_scope. (* Define + on the nat as the default for + *)
Check (fun x y1 y2 z t => P _ (x + t) ((f _ (y1 + y2) + z))).
\end{coq_example}
-\Rem The scope {\tt type\_scope} has also a local effect on
+\Rem The scopes {\tt type\_scope} and {\tt function\_scope} also have a local effect on
interpretation. See the next section.
\SeeAlso The command to show the scopes bound to the arguments of a
@@ -940,10 +941,21 @@ Check # @@%mybool #.
The scope {\tt type\_scope} has a special status. It is a primitive
interpretation scope which is temporarily activated each time a
-subterm of an expression is expected to be a type. This includes goals
-and statements, types of binders, domain and codomain of implication,
-codomain of products, and more generally any type argument of a
-declared or defined constant.
+subterm of an expression is expected to be a type. It is delimited by
+the key {\tt type}, and bound to the coercion class {\tt Sortclass}. It is also
+used in certain situations where an expression is statically known to
+be a type, including the conclusion and the type of hypotheses within
+an {\tt Ltac} goal match (see Section~\ref{ltac-match-goal})
+the statement of a theorem, the type of
+a definition, the type of a binder, the domain and codomain of
+implication, the codomain of products, and more generally any type
+argument of a declared or defined constant.
+
+\subsection[The {\tt function\_scope} interpretation scope]{The {\tt function\_scope} interpretation scope\index{function\_scope@\texttt{function\_scope}}}
+
+The scope {\tt function\_scope} also has a special status.
+It is temporarily activated each time the argument of a global reference is
+recognized to be a {\tt Funclass instance}, i.e., of type {\tt forall x:A, B} or {\tt A -> B}.
\subsection{Interpretation scopes used in the standard library of {\Coq}}
@@ -953,38 +965,39 @@ commands {\tt Print Scopes} or {\tt Print Scope {\scope}}.
\subsubsection{\tt type\_scope}
-This includes infix {\tt *} for product types and infix {\tt +} for
-sum types. It is delimited by key {\tt type}.
+This scope includes infix {\tt *} for product types and infix {\tt +} for
+sum types. It is delimited by key {\tt type}, and bound to the coercion class
+{\tt Sortclass}, as described at \ref{bindscope}.
\subsubsection{\tt nat\_scope}
-This includes the standard arithmetical operators and relations on
+This scope includes the standard arithmetical operators and relations on
type {\tt nat}. Positive numerals in this scope are mapped to their
canonical representent built from {\tt O} and {\tt S}. The scope is
-delimited by key {\tt nat}.
+delimited by key {\tt nat}, and bound to the type {\tt nat} (see \ref{bindscope}).
\subsubsection{\tt N\_scope}
-This includes the standard arithmetical operators and relations on
+This scope includes the standard arithmetical operators and relations on
type {\tt N} (binary natural numbers). It is delimited by key {\tt N}
and comes with an interpretation for numerals as closed term of type {\tt Z}.
\subsubsection{\tt Z\_scope}
-This includes the standard arithmetical operators and relations on
+This scope includes the standard arithmetical operators and relations on
type {\tt Z} (binary integer numbers). It is delimited by key {\tt Z}
and comes with an interpretation for numerals as closed term of type {\tt Z}.
\subsubsection{\tt positive\_scope}
-This includes the standard arithmetical operators and relations on
+This scope includes the standard arithmetical operators and relations on
type {\tt positive} (binary strictly positive numbers). It is
delimited by key {\tt positive} and comes with an interpretation for
numerals as closed term of type {\tt positive}.
\subsubsection{\tt Q\_scope}
-This includes the standard arithmetical operators and relations on
+This scope includes the standard arithmetical operators and relations on
type {\tt Q} (rational numbers defined as fractions of an integer and
a strictly positive integer modulo the equality of the
numerator-denominator cross-product). As for numerals, only $0$ and
@@ -993,13 +1006,13 @@ interpretations are $\frac{0}{1}$ and $\frac{1}{1}$ respectively).
\subsubsection{\tt Qc\_scope}
-This includes the standard arithmetical operators and relations on the
+This scope includes the standard arithmetical operators and relations on the
type {\tt Qc} of rational numbers defined as the type of irreducible
fractions of an integer and a strictly positive integer.
\subsubsection{\tt real\_scope}
-This includes the standard arithmetical operators and relations on
+This scope includes the standard arithmetical operators and relations on
type {\tt R} (axiomatic real numbers). It is delimited by key {\tt R}
and comes with an interpretation for numerals as term of type {\tt
R}. The interpretation is based on the binary decomposition. The
@@ -1014,35 +1027,40 @@ those of {\tt R}.
\subsubsection{\tt bool\_scope}
-This includes notations for the boolean operators. It is
-delimited by key {\tt bool}.
+This scope includes notations for the boolean operators. It is
+delimited by key {\tt bool}, and bound to the type {\tt bool} (see \ref{bindscope}).
\subsubsection{\tt list\_scope}
-This includes notations for the list operators. It is
-delimited by key {\tt list}.
+This scope includes notations for the list operators. It is
+delimited by key {\tt list}, and bound to the type {\tt list} (see \ref{bindscope}).
+
+\subsubsection{\tt function\_scope}
+
+This scope is delimited by the key {\tt function}, and bound to the coercion class {\tt Funclass},
+as described at \ref{bindscope}.
\subsubsection{\tt core\_scope}
-This includes the notation for pairs. It is delimited by key {\tt core}.
+This scope includes the notation for pairs. It is delimited by key {\tt core}.
\subsubsection{\tt string\_scope}
-This includes notation for strings as elements of the type {\tt
+This scope includes notation for strings as elements of the type {\tt
string}. Special characters and escaping follow {\Coq} conventions
on strings (see Section~\ref{strings}). Especially, there is no
convention to visualize non printable characters of a string. The
file {\tt String.v} shows an example that contains quotes, a newline
-and a beep (i.e. the ascii character of code 7).
+and a beep (i.e. the ASCII character of code 7).
\subsubsection{\tt char\_scope}
-This includes interpretation for all strings of the form
-\verb!"!$c$\verb!"! where $c$ is an ascii character, or of the form
+This scope includes interpretation for all strings of the form
+\verb!"!$c$\verb!"! where $c$ is an ASCII character, or of the form
\verb!"!$nnn$\verb!"! where $nnn$ is a three-digits number (possibly
with leading 0's), or of the form \verb!""""!. Their respective
-denotations are the ascii code of $c$, the decimal ascii code $nnn$,
-or the ascii code of the character \verb!"! (i.e. the ascii code
+denotations are the ASCII code of $c$, the decimal ASCII code $nnn$,
+or the ASCII code of the character \verb!"! (i.e. the ASCII code
34), all of them being represented in the type {\tt ascii}.
\subsection{Displaying informations about scopes}
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 253eb7f01b..ecb89b5fb8 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -352,7 +352,7 @@ Section~\ref{pattern} to transform the goal so that it gets the form
The tactic {\tt eapply} behaves like {\tt apply} but it does not fail
when no instantiations are deducible for some variables in the
- premises. Rather, it turns these variables into
+ premises. Rather, it turns these variables into
existential variables which are variables still to instantiate (see
Section~\ref{evars}). The instantiation is intended to be found
later in the proof.
@@ -1053,21 +1053,31 @@ dependencies. This tactic is the inverse of {\tt intro}.
\label{move}
This moves the hypothesis named {\ident$_1$} in the local context
-after the hypothesis named {\ident$_2$}. The proof term is not changed.
+after the hypothesis named {\ident$_2$}, where ``after'' is in
+reference to the direction of the move. The proof term is not changed.
-If {\ident$_1$} comes before {\ident$_2$} in the order of dependencies,
-then all the hypotheses between {\ident$_1$} and {\ident$_2$} that
-(possibly indirectly) depend on {\ident$_1$} are moved too.
+If {\ident$_1$} comes before {\ident$_2$} in the order of
+dependencies, then all the hypotheses between {\ident$_1$} and
+{\ident$_2$} that (possibly indirectly) depend on {\ident$_1$} are
+moved too, and all of them are thus moved after {\ident$_2$} in the
+order of dependencies.
If {\ident$_1$} comes after {\ident$_2$} in the order of dependencies,
then all the hypotheses between {\ident$_1$} and {\ident$_2$} that
-(possibly indirectly) occur in {\ident$_1$} are moved too.
+(possibly indirectly) occur in the type of {\ident$_1$} are moved
+too, and all of them are thus moved before {\ident$_2$} in the order
+of dependencies.
\begin{Variants}
\item {\tt move {\ident$_1$} before {\ident$_2$}}
-This moves {\ident$_1$} towards and just before the hypothesis named {\ident$_2$}.
+This moves {\ident$_1$} towards and just before the hypothesis named
+{\ident$_2$}. As for {\tt move {\ident$_1$} after {\ident$_2$}},
+dependencies over {\ident$_1$} (when {\ident$_1$} comes before
+{\ident$_2$} in the order of dependencies) or in the type of
+{\ident$_1$} (when {\ident$_1$} comes after {\ident$_2$} in the order
+of dependencies) are moved too.
\item {\tt move {\ident} at top}
@@ -1084,13 +1094,30 @@ This moves {\ident} at the bottom of the local context (at the end of the contex
\item \errindex{No such hypothesis}
\item \errindex{Cannot move {\ident$_1$} after {\ident$_2$}:
- it occurs in {\ident$_2$}}
+ it occurs in the type of {\ident$_2$}}
\item \errindex{Cannot move {\ident$_1$} after {\ident$_2$}:
it depends on {\ident$_2$}}
\end{ErrMsgs}
+\Example
+
+\begin{coq_example}
+Goal forall x :nat, x = 0 -> forall z y:nat, y=y-> 0=x.
+intros x H z y H0.
+move x after H0.
+Undo.
+move x before H0.
+Undo.
+move H0 after H.
+Undo.
+move H0 before H.
+\end{coq_example}
+\begin{coq_eval}
+Abort.
+\end{coq_eval}
+
\subsection{\tt rename {\ident$_1$} into {\ident$_2$}}
\tacindex{rename}
@@ -1384,7 +1411,7 @@ in the list of subgoals remaining to prove.
quantifications or non-dependent implications) are instantiated
by concrete terms coming either from arguments \term$_1$
$\ldots$ \term$_n$ or from a bindings list (see
- Section~\ref{Binding-list} for more about bindings lists).
+ Section~\ref{Binding-list} for more about bindings lists).
In the first form the application to \term$_1$ {\ldots}
\term$_n$ can be partial. The first form is equivalent to
{\tt assert ({\ident} := {\ident} {\term$_1$} \dots\ \term$_n$)}.
@@ -1488,23 +1515,33 @@ The {\tt evar} tactic creates a new local definition named \ident\ with
type \term\ in the context. The body of this binding is a fresh
existential variable.
-\subsection{\tt instantiate ( {\num} := {\term} )}
+\subsection{\tt instantiate ( {\ident} := {\term} )}
\tacindex{instantiate}
\label{instantiate}
The {\tt instantiate} tactic refines (see Section~\ref{refine})
-an existential variable
-with the term \term. The \num\ argument is the position of the
-existential variable from right to left in the conclusion. This cannot be
-the number of the existential variable since this number is different
-in every session.
+an existential variable {\ident} with the term {\term}.
+It is equivalent to {\tt only [\ident]: refine \term} (preferred alternative).
+
+\begin{Remarks}
+\item To be able to refer to an existential variable by name, the
+user must have given the name explicitly (see~\ref{ExistentialVariables}).
-When you are referring to hypotheses which you did not name
+\item When you are referring to hypotheses which you did not name
explicitly, be aware that Coq may make a different decision on how to
name the variable in the current goal and in the context of the
existential variable. This can lead to surprising behaviors.
+\end{Remarks}
\begin{Variants}
+
+ \item {\tt instantiate ( {\num} := {\term} )}
+ This variant allows to refer to an existential variable which was not
+ named by the user. The {\num} argument is the position of the
+ existential variable from right to left in the goal.
+ Because this variant is not robust to slight changes in the goal,
+ its use is strongly discouraged.
+
\item {\tt instantiate ( {\num} := {\term} ) in \ident}
\item {\tt instantiate ( {\num} := {\term} ) in ( Value of {\ident} )}
@@ -2113,13 +2150,15 @@ The tactic \texttt{functional induction} performs
case analysis and induction following the definition of a function. It
makes use of a principle generated by \texttt{Function}
(see Section~\ref{Function}) or \texttt{Functional Scheme}
-(see Section~\ref{FunScheme}).
+(see Section~\ref{FunScheme}). Note that this tactic is only available
+after a {\tt Require Import FunInd}.
\begin{coq_eval}
Reset Initial.
Import Nat.
\end{coq_eval}
\begin{coq_example}
+Require Import FunInd.
Functional Scheme minus_ind := Induction for minus Sort Prop.
Check minus_ind.
Lemma le_minus (n m:nat) : n - m <= n.
@@ -2565,6 +2604,21 @@ Abort.
This tactic behaves as generalizing \ident$_1$\dots\ \ident$_n$,
then doing \texttt{inversion {\ident} using \ident$'$}.
+\item \tacindex{inversion\_sigma} \texttt{inversion\_sigma}
+
+ This tactic turns equalities of dependent pairs (e.g.,
+ \texttt{existT P x p = existT P y q}, frequently left over by
+ \texttt{inversion} on a dependent type family) into pairs of
+ equalities (e.g., a hypothesis \texttt{H : x = y} and a hypothesis
+ of type \texttt{rew H in p = q}); these hypotheses can subsequently
+ be simplified using \texttt{subst}, without ever invoking any kind
+ of axiom asserting uniqueness of identity proofs. If you want to
+ explicitly specify the hypothesis to be inverted, or name the
+ generated hypotheses, you can invoke \texttt{induction H as [H1 H2]
+ using eq\_sigT\_rect}. This tactic also works for \texttt{sig},
+ \texttt{sigT2}, and \texttt{sig2}, and there are similar
+ \texttt{eq\_sig\emph{*}\_rect} induction lemmas.
+
\end{Variants}
\firstexample
@@ -2659,6 +2713,64 @@ dependent inversion_clear H.
Note that \texttt{H} has been substituted by \texttt{(LeS n m0 l)} and
\texttt{m} by \texttt{(S m0)}.
+\example{Using \texorpdfstring{\texttt{inversion\_sigma}}{inversion\_sigma}}
+
+Let us consider the following inductive type of length-indexed lists,
+and a lemma about inverting equality of \texttt{cons}:
+
+\begin{coq_eval}
+Reset Initial.
+Set Printing Compact Contexts.
+\end{coq_eval}
+
+\begin{coq_example*}
+Require Coq.Logic.Eqdep_dec.
+
+Inductive vec A : nat -> Type :=
+| nil : vec A O
+| cons {n} (x : A) (xs : vec A n) : vec A (S n).
+
+Lemma invert_cons : forall A n x xs y ys,
+ @cons A n x xs = @cons A n y ys
+ -> xs = ys.
+Proof.
+\end{coq_example*}
+
+\begin{coq_example}
+intros A n x xs y ys H.
+\end{coq_example}
+
+After performing \texttt{inversion}, we are left with an equality of
+\texttt{existT}s:
+
+\begin{coq_example}
+inversion H.
+\end{coq_example}
+
+We can turn this equality into a usable form with
+\texttt{inversion\_sigma}:
+
+\begin{coq_example}
+inversion_sigma.
+\end{coq_example}
+
+To finish cleaning up the proof, we will need to use the fact that
+that all proofs of \texttt{n = n} for \texttt{n} a \texttt{nat} are
+\texttt{eq\_refl}:
+
+\begin{coq_example}
+let H := match goal with H : n = n |- _ => H end in
+pose proof (Eqdep_dec.UIP_refl_nat _ H); subst H.
+simpl in *.
+\end{coq_example}
+
+Finally, we can finish the proof:
+
+\begin{coq_example}
+assumption.
+Qed.
+\end{coq_example}
+
\subsection{\tt fix {\ident} {\num}}
\tacindex{fix}
\label{tactic:fix}
@@ -2959,7 +3071,7 @@ activated, {\tt subst} also deals with the following corner cases:
\item The presence of a recursive equation which without the option
would be a cause of failure of {\tt subst}.
-
+
\item A context with cyclic dependencies as with hypotheses {\tt
\ident$_1$ = f~\ident$_2$} and {\tt \ident$_2$ = g~\ident$_1$} which
without the option would be a cause of failure of {\tt subst}.
@@ -3254,7 +3366,7 @@ a sort of strong normalization with two key differences:
\begin{itemize}
\item They unfold a constant if and only if it leads to a
$\iota$-reduction, i.e. reducing a match or unfolding a fixpoint.
-\item While reducing a constant unfolding to (co)fixpoints,
+\item While reducing a constant unfolding to (co)fixpoints,
the tactics use the name of the
constant the (co)fixpoint comes from instead of the (co)fixpoint
definition in recursive calls.
@@ -3985,7 +4097,7 @@ Abort.
& & e * & \text{ Kleene star } \\
& & \texttt{emp} & \text{ empty } \\
& & \texttt{eps} & \text{ epsilon } \\
- & & \texttt{(} e \texttt{)} &
+ & & \texttt{(} e \texttt{)} &
\end{array}\]
The \texttt{emp} regexp does not match any search path while
@@ -4797,6 +4909,7 @@ that performs inversion on hypothesis {\ident} of the form
\texttt{\qualid\ \term$_1$\dots\term$_n$\ = \term} or \texttt{\term\ =
\qualid\ \term$_1$\dots\term$_n$} where \qualid\ must have been
defined using \texttt{Function} (see Section~\ref{Function}).
+Note that this tactic is only available after a {\tt Require Import FunInd}.
\begin{ErrMsgs}
\item \errindex{Hypothesis {\ident} must contain at least one Function}
@@ -5148,7 +5261,7 @@ Reset Initial.
\subsection[\tt swap \num$_1$ \num$_2$]{\tt swap \num$_1$ \num$_2$\tacindex{swap}}
-This tactic switches the position of the goals of indices $\num_1$ and $\num_2$. If either $\num_1$ or $\num_2$ is negative then goals are counted from the end of the focused goal list. Goals are indexed from $1$, there is no goal with position $0$.
+This tactic switches the position of the goals of indices $\num_1$ and $\num_2$. If either $\num_1$ or $\num_2$ is negative then goals are counted from the end of the focused goal list. Goals are indexed from $1$, there is no goal with position $0$.
\Example
\begin{coq_example*}
diff --git a/doc/refman/RefMan-uti.tex b/doc/refman/RefMan-uti.tex
index 08cdbee503..fee4de3364 100644
--- a/doc/refman/RefMan-uti.tex
+++ b/doc/refman/RefMan-uti.tex
@@ -98,7 +98,7 @@ Such command generates the following files:
An optional file {\bf {\tt CoqMakefile.local}} can be provided by the user in order to extend {\tt CoqMakefile}. In particular one can declare custom actions to be performed before or after the build process. Similarly one can customize the install target or even provide new targets. Extension points are documented in the {\tt CoqMakefile} file.
The extensions of the files listed in {\tt \_CoqProject} is
-used in order to decide how to build them In particular:
+used in order to decide how to build them. In particular:
\begin{itemize}
\item {\Coq} files must use the \texttt{.v} extension
@@ -121,6 +121,43 @@ and status of rules shall change in the future. Users are advised to
include {\tt Makefile.conf} or call a target of the generated Makefile
as in {\tt make -f Makefile target} from another Makefile.
+One way to get access to all targets of the generated
+\texttt{CoqMakefile} is to have a generic target for invoking unknown
+targets. For example:
+\begin{verbatim}
+# KNOWNTARGETS will not be passed along to CoqMakefile
+KNOWNTARGETS := CoqMakefile extra-stuff extra-stuff2
+# KNOWNFILES will not get implicit targets from the final rule, and so
+# depending on them won't invoke the submake
+# Warning: These files get declared as PHONY, so any targets depending
+# on them always get rebuilt
+KNOWNFILES := Makefile _CoqProject
+
+.DEFAULT_GOAL := invoke-coqmakefile
+
+CoqMakefile: Makefile _CoqProject
+ $(COQBIN)coq_makefile -f _CoqProject -o CoqMakefile
+
+invoke-coqmakefile: CoqMakefile
+ $(MAKE) --no-print-directory -f CoqMakefile $(filter-out $(KNOWNTARGETS),$(MAKECMDGOALS))
+
+.PHONY: invoke-coqmakefile $(KNOWNFILES)
+
+####################################################################
+####################################################################
+####################################################################
+####################################################################
+## Your targets here ##
+####################################################################
+####################################################################
+####################################################################
+####################################################################
+
+# This should be the last rule, to handle any targets not declared above
+%: invoke-coqmakefile
+ @true
+\end{verbatim}
+
\paragraph{Notes for users of {\tt coq\_makefile} with version $<$ 8.7}
\begin{itemize}
diff --git a/doc/refman/Universes.tex b/doc/refman/Universes.tex
index 36518e6fae..2bb1301c79 100644
--- a/doc/refman/Universes.tex
+++ b/doc/refman/Universes.tex
@@ -131,6 +131,52 @@ producing global universe constraints, one can use the
polymorphically, not at a single instance.
\end{itemize}
+\asection{{\tt Cumulative, NonCumulative}}
+\comindex{Cumulative}
+\comindex{NonCumulative}
+\optindex{Inductive Cumulativity}
+
+Inductive types, coinductive types, variants and records can be
+declared cumulative using the \texttt{Cumulative}. Alternatively,
+there is an option \texttt{Set Inductive Cumulativity} which when set,
+makes all subsequent inductive definitions cumulative. Consider the examples below.
+\begin{coq_example*}
+Polymorphic Cumulative Inductive list {A : Type} :=
+| nil : list
+| cons : A -> list -> list.
+\end{coq_example*}
+\begin{coq_example}
+Print list.
+\end{coq_example}
+When printing \texttt{list}, the part of the output of the form
+\texttt{$\mathtt{\sim}$@\{i\} <= $\mathtt{\sim}$@\{j\} iff }
+indicates the universe constraints in order to have the subtyping
+$\WTEGLECONV{\mathtt{list@\{i\}} A}{\mathtt{list@\{j\}} B}$
+(for fully applied instances of \texttt{list}) whenever $\WTEGCONV{A}{B}$.
+In the case of \texttt{list} there is no constraint!
+This also means that any two instances of \texttt{list} are convertible:
+$\WTEGCONV{\mathtt{list@\{i\}} A}{\mathtt{list@\{j\}} B}$ whenever $\WTEGCONV{A}{B}$ and
+furthermore their corresponding (when fully applied to convertible arguments) constructors.
+See Chapter~\ref{Cic} for more details on convertibility and subtyping.
+Also notice the subtyping constraints for the \emph{non-cumulative} version of list:
+\begin{coq_example*}
+Polymorphic NonCumulative Inductive list' {A : Type} :=
+| nil' : list'
+| cons' : A -> list' -> list'.
+\end{coq_example*}
+\begin{coq_example}
+Print list'.
+\end{coq_example}
+The following is an example of a record with non-trivial subtyping relation:
+\begin{coq_example*}
+Polymorphic Cumulative Record packType := {pk : Type}.
+\end{coq_example*}
+\begin{coq_example}
+Print packType.
+\end{coq_example}
+Notice that as expected, \texttt{packType@\{i\}} and \texttt{packType@\{j\}} are convertible if and only if \texttt{i $=$ j}.
+
+
\asection{Global and local universes}
Each universe is declared in a global or local environment before it can
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 00:55:46 +0000