aboutsummaryrefslogtreecommitdiff
path: root/doc
diff options
context:
space:
mode:
Diffstat (limited to 'doc')
-rw-r--r--doc/faq/fk.bib2
-rw-r--r--doc/refman/Classes.tex177
-rw-r--r--doc/refman/Extraction.tex2
-rw-r--r--doc/refman/Micromega.tex90
-rw-r--r--doc/refman/Program.tex19
-rw-r--r--doc/refman/RefMan-com.tex6
-rw-r--r--doc/refman/RefMan-ext.tex12
-rw-r--r--doc/refman/RefMan-gal.tex4
-rw-r--r--doc/refman/RefMan-ltac.tex32
-rw-r--r--doc/refman/RefMan-oth.tex23
-rw-r--r--doc/refman/RefMan-pre.tex133
-rw-r--r--doc/refman/RefMan-syn.tex38
-rw-r--r--doc/refman/RefMan-tac.tex183
-rw-r--r--doc/refman/RefMan-uti.tex8
-rw-r--r--doc/refman/biblio.bib2
-rw-r--r--doc/stdlib/index-list.html.template1
16 files changed, 598 insertions, 134 deletions
diff --git a/doc/faq/fk.bib b/doc/faq/fk.bib
index 4d90efcdb1..3410427dee 100644
--- a/doc/faq/fk.bib
+++ b/doc/faq/fk.bib
@@ -2171,7 +2171,7 @@ Decomposition}},
@Misc{ProofGeneral,
author = {David Aspinall},
title = {Proof General},
- note = {\url{http://proofgeneral.inf.ed.ac.uk/}}
+ note = {\url{https://proofgeneral.github.io/}}
}
diff --git a/doc/refman/Classes.tex b/doc/refman/Classes.tex
index e8ebb9f995..bd8ee450ef 100644
--- a/doc/refman/Classes.tex
+++ b/doc/refman/Classes.tex
@@ -9,10 +9,6 @@
\aauthor{Matthieu Sozeau}
\label{typeclasses}
-\begin{flushleft}
- \em The status of Type Classes is experimental.
-\end{flushleft}
-
This chapter presents a quick reference of the commands related to type
classes. For an actual introduction to type classes, there is a
description of the system \cite{sozeau08} and the literature on type
@@ -382,6 +378,70 @@ projections as instances. This is almost equivalent to {\tt Hint Resolve
Declares variables according to the given binding context, which might
use implicit generalization (see \ref{SectionContext}).
+\asubsection{\tt typeclasses eauto}
+\tacindex{typeclasses eauto}
+
+The {\tt typeclasses eauto} tactic uses a different resolution engine
+than {\tt eauto} and {\tt auto}. The main differences are the following:
+\begin{itemize}
+\item Contrary to {\tt eauto} and {\tt auto}, the resolution is done
+ entirely in the new proof engine (as of Coq v8.6), meaning that
+ backtracking is available among dependent subgoals, and shelving goals
+ is supported. {\tt typeclasses eauto} is a multi-goal tactic.
+ It analyses the dependencies between subgoals to avoid
+ backtracking on subgoals that are entirely independent.
+\item When called with no arguments, {\tt typeclasses eauto} uses the
+ {\tt typeclass\_instances} database by default (instead of {\tt
+ core}).
+ Dependent subgoals are automatically shelved, and shelved
+ goals can remain after resolution ends (following the behavior of
+ \Coq{} 8.5).
+
+ \emph{Note: } As of Coq 8.6, {\tt all:once (typeclasses eauto)}
+ faithfully mimicks what happens during typeclass resolution when it is
+ called during refinement/type-inference, except that \emph{only}
+ declared class subgoals are considered at the start of resolution
+ during type inference, while ``all'' can select non-class subgoals as
+ well. It might move to {\tt all:typeclasses eauto} in future versions
+ when the refinement engine will be able to backtrack.
+\item When called with specific databases (e.g. {\tt with}), {\tt
+ typeclasses eauto} allows shelved goals to remain at any point
+ during search and treat typeclasses goals like any other.
+\item The transparency information of databases is used consistently for
+ all hints declared in them. It is always used when calling the unifier.
+ When considering the local hypotheses, we use the transparent
+ state of the first hint database given. Using an empty database
+ (created with {\tt Create HintDb} for example) with
+ unfoldable variables and constants as the first argument of
+ typeclasses eauto hence makes resolution with the local hypotheses use
+ full conversion during unification.
+\end{itemize}
+
+\begin{Variants}
+\item \label{depth} {\tt typeclasses eauto \zeroone{\num}}
+ \emph{Warning:} The semantics for the limit {\num} is different than
+ for {\tt auto}. By default, if no limit is given the search is
+ unbounded. Contrary to {\tt auto}, introduction steps ({\tt intro})
+ are counted, which might result in larger limits being necessary
+ when searching with {\tt typeclasses eauto} than {\tt auto}.
+
+\item \label{with} {\tt typeclasses eauto with {\ident}$_1$ \ldots {\ident}$_n$}.
+ This variant runs resolution with the given hint databases. It treats
+ typeclass subgoals the same as other subgoals (no shelving of
+ non-typeclass goals in particular).
+\end{Variants}
+
+\asubsection{\tt autoapply {\term} with {\ident}}
+\tacindex{autoapply}
+
+The tactic {\tt autoapply} applies a term using the transparency
+information of the hint database {\ident}, and does \emph{no} typeclass
+resolution. This can be used in {\tt Hint Extern}'s for typeclass
+instances (in hint db {\tt typeclass\_instances}) to
+allow backtracking on the typeclass subgoals created by the lemma
+application, rather than doing type class resolution locally at the hint
+application time.
+
\subsection{\tt Typeclasses Transparent, Opaque {\ident$_1$ \ldots \ident$_n$}}
\comindex{Typeclasses Transparent}
\comindex{Typeclasses Opaque}
@@ -400,20 +460,123 @@ abbreviate a type, like {\tt relation A := A -> A -> Prop}.
This is equivalent to {\tt Hint Transparent,Opaque} {\ident} {\tt: typeclass\_instances}.
+\subsection{\tt Set Typeclasses Dependency Order}
+\optindex{Typeclasses Dependency Order}
+
+This option (on by default since 8.6) respects the dependency order between
+subgoals, meaning that subgoals which are depended on by other subgoals
+come first, while the non-dependent subgoals were put before the
+dependent ones previously (Coq v8.5 and below). This can result in quite
+different performance behaviors of proof search.
+
+\subsection{\tt Set Typeclasses Filtered Unification}
+\optindex{Typeclasses Filtered Unification}
+
+This option, available since Coq 8.6 and off by default, switches the
+hint application procedure to a filter-then-unify strategy. To apply a
+hint, we first check that the goal \emph{matches} syntactically the
+inferred or specified pattern of the hint, and only then try to
+\emph{unify} the goal with the conclusion of the hint. This can
+drastically improve performance by calling unification less often,
+matching syntactic patterns being very quick. This also provides more
+control on the triggering of instances. For example, forcing a constant
+to explicitely appear in the pattern will make it never apply on a goal
+where there is a hole in that place.
+
+\subsection{\tt Set Typeclasses Legacy Resolution}
+\optindex{Typeclasses Legacy Resolution}
+
+This option (off by default) uses the 8.5 implementation of resolution.
+Use for compatibility purposes only (porting and debugging).
+
+\subsection{\tt Set Typeclasses Module Eta}
+\optindex{Typeclasses Modulo Eta}
+
+This option allows eta-conversion for functions and records during
+unification of type-classes. This option is now unsupported in 8.6 with
+{\tt Typeclasses Filtered Unification} set, but still affects the
+default unification strategy, and the one used in {\tt Legacy
+ Resolution} mode. It is \emph{unset} by default. If {\tt Typeclasses
+ Filtered Unification} is set, this has no effect and unification will
+find solutions up-to eta conversion. Note however that syntactic
+pattern-matching is not up-to eta.
+
+\subsection{\tt Set Typeclasses Limit Intros}
+\optindex{Typeclasses Limit Intros}
+
+This option (on by default in Coq 8.6 and below) controls the ability to
+apply hints while avoiding (functional) eta-expansions in the generated
+proof term. It does so by allowing hints that conclude in a product to
+apply to a goal with a matching product directly, avoiding an
+introduction. \emph{Warning:} this can be expensive as it requires
+rebuilding hint clauses dynamically, and does not benefit from the
+invertibility status of the product introduction rule, resulting in
+potentially more expensive proof-search (i.e. more useless
+backtracking).
+
+\subsection{\tt Set Typeclass Resolution After Apply}
+\optindex{Typeclasses Resolution After Apply}
+\emph{Deprecated since 8.6}
+
+This option (off by default in Coq 8.6 and 8.5) controls the resolution
+of typeclass subgoals generated by the {\tt apply} tactic.
+
+\subsection{\tt Set Typeclass Resolution For Conversion}
+\optindex{Typeclasses Resolution For Conversion}
+
+This option (on by default) controls the use of typeclass resolution
+when a unification problem cannot be solved during
+elaboration/type-inference. With this option on, when a unification
+fails, typeclass resolution is tried before launching unification once again.
+
+\subsection{\tt Set Typeclasses Strict Resolution}
+\optindex{Typeclasses Strict Resolution}
+
+Typeclass declarations introduced when this option is set have a
+stricter resolution behavior (the option is off by default). When
+looking for unifications of a goal with an instance of this class, we
+``freeze'' all the existentials appearing in the goals, meaning that
+they are considered rigid during unification and cannot be instantiated.
+
+\subsection{\tt Set Typeclasses Unique Solutions}
+\optindex{Typeclasses Unique Solutions}
+
+When a typeclass resolution is launched we ensure that it has a single
+solution or fail. This ensures that the resolution is canonical, but can
+make proof search much more expensive.
+
+\subsection{\tt Set Typeclasses Unique Instances}
+\optindex{Typeclasses Unique Instances}
+
+Typeclass declarations introduced when this option is set have a
+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}]}
\comindex{Typeclasses eauto}
\label{TypeclassesEauto}
-This command allows customization of the type class resolution tactic,
-based on a variant of eauto. The flags semantics are:
+This command allows more global customization of the type class
+resolution tactic.
+The semantics of the options are:
\begin{itemize}
\item {\tt debug} In debug mode, the trace of successfully applied
tactics is printed.
\item {\tt dfs, bfs} This sets the search strategy to depth-first search
(the default) or breadth-first search.
-\item {\emph{depth}} This sets the depth of the search (the default is 100).
+\item {\emph{depth}} This sets the depth limit of the search.
\end{itemize}
+\subsection{\tt Set Typeclasses Debug [Verbosity {\num}]}
+\optindex{Typeclasses Debug}
+\optindex{Typeclasses Debug Verbosity}
+
+These options allow to see the resolution steps of typeclasses that are
+performed during search. The {\tt Debug} option is synonymous to
+{\tt Debug Verbosity 1}, and {\tt Debug Verbosity 2} provides more
+information (tried tactics, shelving of goals, etc\ldots).
+
\subsection{\tt Set Refine Instance Mode}
\optindex{Refine Instance Mode}
diff --git a/doc/refman/Extraction.tex b/doc/refman/Extraction.tex
index 9da23b54ed..01dbcfb1cb 100644
--- a/doc/refman/Extraction.tex
+++ b/doc/refman/Extraction.tex
@@ -448,7 +448,7 @@ let dp x y f = Pair ((Obj.magic f () x), (Obj.magic f () y))
happens when there is a quantification over types inside the type
of a constructor; for example:
\begin{verbatim}
-Inductive anything : Set := dummy : forall A:Set, A -> anything.
+Inductive anything : Type := dummy : forall A:Set, A -> anything.
\end{verbatim}
which corresponds to the definition of an ML dynamic type.
diff --git a/doc/refman/Micromega.tex b/doc/refman/Micromega.tex
index 1efed6ef76..4daf98f87a 100644
--- a/doc/refman/Micromega.tex
+++ b/doc/refman/Micromega.tex
@@ -4,16 +4,19 @@
\asection{Short description of the tactics}
-\tacindex{psatz} \tacindex{lra}
+\tacindex{psatz} \tacindex{lra} \tacindex{lia} \tacindex{nia} \tacindex{nra}
\label{sec:psatz-hurry}
The {\tt Psatz} module ({\tt Require Import Psatz.}) gives access to
several tactics for solving arithmetic goals over {\tt Z}, {\tt Q}, and
{\tt R}:\footnote{Support for {\tt nat} and {\tt N} is obtained by
- pre-processing the goal with the {\tt zify} tactic.}
+ pre-processing the goal with the {\tt zify} tactic.}.
+It also possible to get the tactics for integers by a {\tt Require Import Lia}, rationals {\tt Require Import Lqa}
+and reals {\tt Require Import Lra}.
\begin{itemize}
\item {\tt lia} is a decision procedure for linear integer arithmetic (see Section~\ref{sec:lia});
\item {\tt nia} is an incomplete proof procedure for integer non-linear arithmetic (see Section~\ref{sec:nia});
-\item {\tt lra} is a decision procedure for linear (real or rational) arithmetic goals (see Section~\ref{sec:lra});
+\item {\tt lra} is a decision procedure for linear (real or rational) arithmetic (see Section~\ref{sec:lra});
+\item {\tt nra} is an incomplete proof procedure for non-linear (real or rational) arithmetic (see Section~\ref{sec:nra});
\item {\tt psatz D n} where {\tt D} is {\tt Z} or {\tt Q} or {\tt R}, and
{\tt n} is an optional integer limiting the proof search depth is is an
incomplete proof procedure for non-linear arithmetic. It is based on
@@ -114,36 +117,6 @@ The deductive power of {\tt lra} is the combined deductive power of {\tt ring\_s
%
There is also an overlap with the {\tt field} tactic {\emph e.g.}, {\tt x = 10 * x / 10} is solved by {\tt lra}.
-\asection{{\tt psatz}: a proof procedure for non-linear arithmetic}
-\label{sec:psatz}
-The {\tt psatz} tactic explores the $\mathit{Cone}$ by increasing degrees -- hence the depth parameter $n$.
-In theory, such a proof search is complete -- if the goal is provable the search eventually stops.
-Unfortunately, the external oracle is using numeric (approximate) optimization techniques that might miss a
-refutation.
-
-To illustrate the working of the tactic, consider we wish to prove the following Coq goal.
-\begin{coq_eval}
-Require Import ZArith Psatz.
-Open Scope Z_scope.
-\end{coq_eval}
-\begin{coq_example*}
-Goal forall x, -x^2 >= 0 -> x - 1 >= 0 -> False.
-\end{coq_example*}
-\begin{coq_eval}
-intro x; psatz Z 2.
-\end{coq_eval}
-Such a goal is solved by {\tt intro x; psatz Z 2}. The oracle returns the
-cone expression $2 \times (\mathbf{x-1}) + (\mathbf{x-1}) \times
-(\mathbf{x-1}) + \mathbf{-x^2}$ (polynomial hypotheses are printed in
-bold). By construction, this expression belongs to $\mathit{Cone}(\{-x^2,
-x -1\})$. Moreover, by running {\tt ring} we obtain $-1$. By
-Theorem~\ref{thm:psatz}, the goal is valid.
-%
-
-%% \paragraph{The {\tt sos} tactic} -- where {\tt sos} stands for \emph{sum of squares} -- tries to prove that a
-%% single polynomial $p$ is positive by expressing it as a sum of squares \emph{i.e.,} $\sum_{i\in S} p_i^2$.
-%% This amounts to searching for $p$ in the cone without generators \emph{i.e.}, $Cone(\{\})$.
-%
\asection{{\tt lia}: a tactic for linear integer arithmetic}
\tacindex{lia}
@@ -219,22 +192,61 @@ Our current oracle tries to find an expression $e$ with a small range $[c_1,c_2]
We generate $c_2 - c_1$ subgoals which contexts are enriched with an equation $e = i$ for $i \in [c_1,c_2]$ and
recursively search for a proof.
-\asection{{\tt nia}: a proof procedure for non-linear integer arithmetic}
-\tacindex{nia}
-\label{sec:nia}
-The {\tt nia} tactic is an {\emph experimental} proof procedure for non-linear integer arithmetic.
+
+\asection{{\tt nra}: a proof procedure for non-linear arithmetic}
+\tacindex{nra}
+\label{sec:nra}
+The {\tt nra} tactic is an {\emph experimental} proof procedure for non-linear arithmetic.
%
The tactic performs a limited amount of non-linear reasoning before running the
-linear prover of {\tt lia}.
+linear prover of {\tt lra}.
This pre-processing does the following:
\begin{itemize}
\item If the context contains an arithmetic expression of the form $e[x^2]$ where $x$ is a
monomial, the context is enriched with $x^2\ge 0$;
\item For all pairs of hypotheses $e_1\ge 0$, $e_2 \ge 0$, the context is enriched with $e_1 \times e_2 \ge 0$.
\end{itemize}
-After pre-processing, the linear prover of {\tt lia} searches for a proof
+After this pre-processing, the linear prover of {\tt lra} searches for a proof
by abstracting monomials by variables.
+\asection{{\tt nia}: a proof procedure for non-linear integer arithmetic}
+\tacindex{nia}
+\label{sec:nia}
+The {\tt nia} tactic is a proof procedure for non-linear integer arithmetic.
+%
+It performs a pre-processing similar to {\tt nra}. The obtained goal is solved using the linear integer prover {\tt lia}.
+
+\asection{{\tt psatz}: a proof procedure for non-linear arithmetic}
+\label{sec:psatz}
+The {\tt psatz} tactic explores the $\mathit{Cone}$ by increasing degrees -- hence the depth parameter $n$.
+In theory, such a proof search is complete -- if the goal is provable the search eventually stops.
+Unfortunately, the external oracle is using numeric (approximate) optimization techniques that might miss a
+refutation.
+
+To illustrate the working of the tactic, consider we wish to prove the following Coq goal.
+\begin{coq_eval}
+Require Import ZArith Psatz.
+Open Scope Z_scope.
+\end{coq_eval}
+\begin{coq_example*}
+Goal forall x, -x^2 >= 0 -> x - 1 >= 0 -> False.
+\end{coq_example*}
+\begin{coq_eval}
+intro x; psatz Z 2.
+\end{coq_eval}
+Such a goal is solved by {\tt intro x; psatz Z 2}. The oracle returns the
+cone expression $2 \times (\mathbf{x-1}) + (\mathbf{x-1}) \times
+(\mathbf{x-1}) + \mathbf{-x^2}$ (polynomial hypotheses are printed in
+bold). By construction, this expression belongs to $\mathit{Cone}(\{-x^2,
+x -1\})$. Moreover, by running {\tt ring} we obtain $-1$. By
+Theorem~\ref{thm:psatz}, the goal is valid.
+%
+
+%% \paragraph{The {\tt sos} tactic} -- where {\tt sos} stands for \emph{sum of squares} -- tries to prove that a
+%% single polynomial $p$ is positive by expressing it as a sum of squares \emph{i.e.,} $\sum_{i\in S} p_i^2$.
+%% This amounts to searching for $p$ in the cone without generators \emph{i.e.}, $Cone(\{\})$.
+%
+
%%% Local Variables:
diff --git a/doc/refman/Program.tex b/doc/refman/Program.tex
index 11dd3a0517..2fc1c8764a 100644
--- a/doc/refman/Program.tex
+++ b/doc/refman/Program.tex
@@ -63,10 +63,27 @@ will be first rewritten to:
previous one, an inequality is added in the context of the second
branch. See for example the definition of {\tt div2} below, where the second
branch is typed in a context where $\forall p, \_ <> S (S p)$.
-
+
\item Coercion. If the object being matched is coercible to an inductive
type, the corresponding coercion will be automatically inserted. This also
works with the previous mechanism.
+
+\end{itemize}
+
+There are options to control the generation of equalities
+and coercions.
+
+\begin{itemize}
+\item {\tt Unset Program Cases}\optindex{Program Cases} This deactivates
+ the special treatment of pattern-matching generating equalities and
+ inequalities when using \Program\ (it is on by default). All
+ pattern-matchings and let-patterns are handled using the standard
+ algorithm of Coq (see Section~\ref{Mult-match-full}) when this option is
+ deactivated.
+\item {\tt Unset Program Generalized Coercion}\optindex{Program
+ Generalized Coercion} This deactivates the coercion of general
+ inductive types when using \Program\ (the option is on by default).
+ Coercion of subset types and pairs is still active in this case.
\end{itemize}
\subsection{Syntactic control over equalities}
diff --git a/doc/refman/RefMan-com.tex b/doc/refman/RefMan-com.tex
index 6f85849888..c1e552a5da 100644
--- a/doc/refman/RefMan-com.tex
+++ b/doc/refman/RefMan-com.tex
@@ -199,6 +199,12 @@ The following command-line options are recognized by the commands {\tt
available for {\tt coqc} only; it is the counterpart of {\tt
-compile-verbose}.
+ \item[{\tt -w} (all|none|w$_1$,\ldots,w$_n$)]\ %
+
+ Configure the display of warnings. This option expects {\tt all}, {\tt none}
+ or a comma-separated list of warning names or categories (see
+ Section~\ref{SetWarnings}).
+
%Mostly unused in the code
%\item[{\tt -debug}]\ %
%
diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex
index 51e881bff4..b475a5233c 100644
--- a/doc/refman/RefMan-ext.tex
+++ b/doc/refman/RefMan-ext.tex
@@ -1315,10 +1315,10 @@ command:
\begin{quote}
\tt Arguments {\qualid} \nelist{\possiblybracketedident}{}
\end{quote}
-where the list of {\possiblybracketedident} is the list of all 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.
+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
@@ -1591,7 +1591,7 @@ Implicit arguments names can be redefined using the following syntax:
{\tt Arguments {\qualid} \nelist{\name}{} : rename}
\end{quote}
-Without the {\tt rename} flag, {\tt Arguments} can be used to assert
+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.
@@ -1600,7 +1600,7 @@ these arguments are named as expected.
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] _.
+Fail Arguments p [s t] _ [w] _ : assert.
\end{coq_example}
diff --git a/doc/refman/RefMan-gal.tex b/doc/refman/RefMan-gal.tex
index fcccd9cb4b..99eee44e03 100644
--- a/doc/refman/RefMan-gal.tex
+++ b/doc/refman/RefMan-gal.tex
@@ -273,6 +273,7 @@ called \CIC). The formal presentation of {\CIC} is given in Chapter
{\binder} & ::= & {\name} & (\ref{Binders}) \\
& $|$ & {\tt (} \nelist{\name}{} {\tt :} {\term} {\tt )} &\\
& $|$ & {\tt (} {\name} {\typecstr} {\tt :=} {\term} {\tt )} &\\
+ & $|$ & {\tt '} {\pattern} &\\
& & &\\
{\name} & ::= & {\ident} &\\
& $|$ & {\tt \_} &\\
@@ -410,7 +411,8 @@ bound variable cannot be synthesized by the system, it can be
specified with the notation {\tt (}\,{\ident}\,{\tt :}\,{\type}\,{\tt
)}. There is also a notation for a sequence of binding variables
sharing the same type: {\tt (}\,{\ident$_1$}\ldots{\ident$_n$}\,{\tt
-:}\,{\type}\,{\tt )}.
+:}\,{\type}\,{\tt )}. A binder can also be any pattern prefixed by a quote,
+e.g. {\tt '(x,y)}.
Some constructions allow the binding of a variable to value. This is
called a ``let-binder''. The entry {\binder} of the grammar accepts
diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex
index 5ba3c308a6..9378529cbe 100644
--- a/doc/refman/RefMan-ltac.tex
+++ b/doc/refman/RefMan-ltac.tex
@@ -26,6 +26,7 @@ problems.
\def\tacarg{\nterm{tacarg}}
\def\cpattern{\nterm{cpattern}}
\def\selector{\textrm{\textsl{selector}}}
+\def\toplevelselector{\textrm{\textsl{toplevel\_selector}}}
The syntax of the tactic language is given Figures~\ref{ltac}
and~\ref{ltac-aux}. See Chapter~\ref{BNF-syntax} for a description of
@@ -105,7 +106,7 @@ is understood as
& | & {\tt exactly\_once} {\tacexprpref}\\
& | & {\tt timeout} {\it (}{\naturalnumber} {\it |} {\ident}{\it )} {\tacexprpref}\\
& | & {\tt time} \zeroone{\qstring} {\tacexprpref}\\
-& | & {\selector} {\tt :} {\tacexprpref}\\
+& | & {\tt only} {\selector} {\tt :} {\tacexprpref}\\
& | & {\tacexprinf} \\
\\
{\tacexprinf} & ::= &
@@ -209,11 +210,14 @@ is understood as
\\
\selector & ::= &
[{\ident}]\\
-& $|$ & {\tt all}\\
-& $|$ & {\tt par}\\
& $|$ & {\integer}\\
& $|$ & \nelist{{\it (}{\integer} {\it |} {\integer} {\tt -} {\integer}{\it )}}
- {\tt ,}
+ {\tt ,}\\
+\\
+\toplevelselector & ::= &
+ \selector\\
+& $|$ & {\tt all}\\
+& $|$ & {\tt par}
\end{tabular}
\end{centerframe}
\caption{Syntax of the tactic language (continued)}
@@ -374,7 +378,12 @@ for $=1,...,n$. It fails if the number of focused goals is not exactly $n$.
We can restrict the application of a tactic to a subset of
the currently focused goals with:
\begin{quote}
-{\selector} {\tt :} {\tacexpr}
+ {\toplevelselector} {\tt :} {\tacexpr}
+\end{quote}
+We can also use selectors as a tactical, which allows to use them nested in
+a tactic expression, by using the keyword {\tt only}:
+\begin{quote}
+ {\tt only} {\selector} {\tt :} {\tacexpr}
\end{quote}
When selecting several goals, the tactic {\tacexpr} is applied globally to
all selected goals.
@@ -396,11 +405,12 @@ all selected goals.
of goals described by the given ranges. You can write a single
$n$ as a shortcut for $n$-$n$ when specifying multiple ranges.
- \item {\tt all: } {\tacexpr}
+ \item {\tt all:} {\tacexpr}
In this variant, {\tacexpr} is applied to all focused goals.
+ {\tt all:} can only be used at the toplevel of a tactic expression.
- \item {\tt par: } {\tacexpr}
+ \item {\tt par:} {\tacexpr}
In this variant, {\tacexpr} is applied to all focused goals
in parallel. The number of workers can be controlled via the
@@ -409,7 +419,7 @@ all selected goals.
on goals containing no existential variables and {\tacexpr} must
either solve the goal completely or do nothing (i.e. it cannot make
some progress).
- {\tt par: } can only be used at the top level of a tactic expression.
+ {\tt par:} can only be used at the toplevel of a tactic expression.
\end{Variants}
@@ -1158,7 +1168,7 @@ using the syntax:
\end{quote}
A previous definition of {\qualid} must exist in the environment.
The new definition will always be used instead of the old one and
-it goes accross module boundaries.
+it goes across module boundaries.
If preceded by the keyword {\tt Local} the tactic definition will not
be exported outside the current module.
@@ -1277,9 +1287,9 @@ Prints the profile
Prints a profile for all tactics that start with {\qstring}. Append a period (.) to the string if you only want exactly that name.
\begin{quote}
-{\tt Reset Profile}.
+{\tt Reset Ltac Profile}.
\end{quote}
-Resets the profile, that is, deletes all accumulated information
+Resets the profile, that is, deletes all accumulated information. Note that backtracking across a {\tt Reset Ltac Profile} will not restore the information.
\begin{coq_eval}
Reset Initial.
diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex
index aea2bae38d..56ce753cd6 100644
--- a/doc/refman/RefMan-oth.tex
+++ b/doc/refman/RefMan-oth.tex
@@ -87,7 +87,7 @@ is restored when the current \emph{section} ends.
\item {\tt Global Unset {\rm\sl flag}.\comindex{Global Unset}}\\
This command switches {\rm\sl flag} off. The original state of
{\rm\sl flag} is \emph{not} restored at the end of the module. Additionally,
-if set in a file, {\rm\sl flag} is switched on when the file is
+if set in a file, {\rm\sl flag} is switched off when the file is
{\tt Require}-d.
\end{Variants}
@@ -914,6 +914,19 @@ This command turns off the normal displaying.
\subsection[\tt Unset Silent.]{\tt Unset Silent.\optindex{Silent}}
This command turns the normal display on.
+\subsection[\tt Set Warnings ``(\nterm{w}$_1$,\ldots,%
+ \nterm{w}$_n$)''.]{{\tt Set Warnings ``(\nterm{w}$_1$,\ldots,%
+ \nterm{w}$_n$)''}.\optindex{Warnings}}
+\label{SetWarnings}
+This command configures the display of warnings. It is experimental, and
+expects, between quotes, a comma-separated list of warning names or
+categories. Adding~\texttt{-} in front of a warning or category disables it,
+adding~\texttt{+} makes it an error. It is possible to use the special
+categories \texttt{all} and \texttt{default}, the latter containing the warnings
+enabled by default. The flags are interpreted from left to right, so in case of
+an overlap, the flags on the right have higher priority, meaning that
+\texttt{A,-A} is equivalent to \texttt{-A}.
+
\subsection[\tt Set Search Output Name Only.]{\tt Set Search Output Name Only.\optindex{Search Output Name Only}
\label{Search-Output-Name-Only}
\index{Search Output Name Only mode}}
@@ -947,6 +960,14 @@ time of writing this documentation, the default value is 50).
\subsection[\tt Test Printing Depth.]{\tt Test Printing Depth.\optindex{Printing Depth}}
This command displays the current nesting depth used for display.
+\subsection[\tt Set Printing Dependent Evars Line.]{\tt Set Printing Dependent Evars Line.\optindex{Printing Dependent Evars Line}}
+This command enables the printing of the ``{\tt (dependent evars: \ldots)}''
+line when {\tt -emacs} is passed.
+
+\subsection[\tt Unset Printing Dependent Evars Line.]{\tt Unset Printing Dependent Evars Line.\optindex{Printing Dependent Evars Line}}
+This command disables the printing of the ``{\tt (dependent evars: \ldots)}''
+line when {\tt -emacs} is passed.
+
%\subsection{\tt Abstraction ...}
%Not yet documented.
diff --git a/doc/refman/RefMan-pre.tex b/doc/refman/RefMan-pre.tex
index cb2ab5dc2f..f36969e821 100644
--- a/doc/refman/RefMan-pre.tex
+++ b/doc/refman/RefMan-pre.tex
@@ -1087,6 +1087,139 @@ Paris, January 2015, revised December 2015,\\
Hugo Herbelin, Matthieu Sozeau and the {\Coq} development team\\
\end{flushright}
+\section*{Credits: version 8.6}
+
+{\Coq} version 8.6 contains the result of refinements, stabilization of
+8.5's features and cleanups of the internals of the system. Over the
+year of (now time-based) development, about 450 bugs were resolved and
+over 100 contributions integrated. The main user visible changes are:
+\begin{itemize}
+\item A new, faster state-of-the-art universe constraint checker, by
+ Jacques-Henri Jourdan.
+\item In CoqIDE and other asynchronous interfaces, more fine-grained
+ asynchronous processing and error reporting by Enrico Tassi, making {\Coq}
+ capable of recovering from errors and continue processing the document.
+\item More access to the proof engine features from Ltac: goal
+ management primitives, range selectors and a {\tt typeclasses
+ eauto} engine handling multiple goals and multiple successes, by
+ Cyprien Mangin, Matthieu Sozeau and Arnaud Spiwack.
+\item Tactic behavior uniformization and specification, generalization
+ of intro-patterns by Hugo Herbelin and others.
+\item A brand new warning system allowing to control warnings, turn them
+ into errors or ignore them selectively by Maxime Dénès, Guillaume
+ Melquiond, Pierre-Marie Pédrot and others.
+\item Irrefutable patterns in abstractions, by Daniel de Rauglaudre.
+\item The {\tt ssreflect} subterm selection algorithm by Georges Gonthier and
+ Enrico Tassi is now accessible to tactic writers through the {\tt ssrmatching}
+ plugin.
+\item Integration of {\tt LtacProf}, a profiler for {\tt Ltac} by Jason
+ Gross, Paul Steckler, Enrico Tassi and Tobias Tebbi.
+\end{itemize}
+
+{\Coq} 8.6 also comes with a bunch of smaller-scale changes and
+improvements regarding the different components of the system. We shall
+only list a few of them.
+
+The {\tt iota} reduction flag is now a shorthand for {\tt match}, {\tt
+ fix} and {\tt cofix} flags controlling the corresponding reduction
+rules (by Hugo Herbelin and Maxime Dénès).
+
+Maxime Dénès maintained the native compilation machinery.
+
+Pierre-Marie Pédrot separated the Ltac code from general purpose
+tactics, and generalized and rationalized the handling of generic
+arguments, allowing to create new versions of Ltac more easily in the
+future.
+
+In patterns and terms, {\tt @}, abbreviations and notations are now
+interpreted the same way, by Hugo Herbelin.
+
+Name handling for universes has been improved by Pierre-Marie Pédrot and
+Matthieu Sozeau. The minimization algorithm has been improved by
+Matthieu Sozeau.
+
+The unifier has been improved by Hugo Herbelin and Matthieu Sozeau,
+fixing some incompatibilities introduced in Coq 8.5. Unification
+constraints can now be left floating around and be seen by the user
+thanks to a new option. The {\tt Keyed Unification} mode has been
+improved by Matthieu Sozeau.
+
+The typeclass resolution engine and associated proof-search tactic have
+been reimplemented on top of the proof-engine monad, providing better
+integration in tactics, and new options have been introduced to control
+it, by Matthieu Sozeau with help from Théo Zimmermann.
+
+The efficiency of the whole system has been significantly improved
+thanks to contributions from Pierre-Marie Pédrot, Maxime Dénès and
+Matthieu Sozeau and performance issue tracking by Jason Gross and Paul
+Steckler.
+
+Standard library improvements by Jason Gross, Sébastien Hinderer, Pierre
+Letouzey and others.
+
+Emilio Jesús Gallego Arias contributed many cleanups and refactorings of
+the pretty-printing and user interface communication components.
+
+Frédéric Besson maintained the micromega tactic.
+
+The OPAM repository for {\Coq} packages has been maintained by Guillaume
+Claret, Guillaume Melquiond, Matthieu Sozeau, Enrico Tassi and others. A
+list of packages is now available at \url{https://coq.inria.fr/opam/www/}.
+
+Packaging tools and software development kits were prepared by Michael
+Soegtrop with the help of Maxime Dénès and Enrico Tassi for Windows, and
+Maxime Dénès and Matthieu Sozeau for MacOS X. Packages are now regularly
+built on the continuous integration server. {\Coq} now comes with a {\tt
+ META} file usable with {\tt ocamlfind}, contributed by Emilio Jesús
+Gallego Arias, Gregory Malecha, and Matthieu Sozeau.
+
+Matej Košík maintained and greatly improved the continuous integration
+setup and the testing of {\Coq} contributions. He also contributed many
+API improvement and code cleanups throughout the system.
+
+The contributors for this version are Bruno Barras, C.J. Bell, Yves
+Bertot, Frédéric Besson, Pierre Boutillier, Tej Chajed, Guillaume
+Claret, Xavier Clerc, Pierre Corbineau, Pierre Courtieu, Maxime Dénès,
+Ricky Elrod, Emilio Jesús Gallego Arias, Jason Gross, Hugo Herbelin,
+Sébastien Hinderer, Jacques-Henri Jourdan, Matej Kosik, Xavier Leroy,
+Pierre Letouzey, Gregory Malecha, Cyprien Mangin, Erik Martin-Dorel,
+Guillaume Melquiond, Clément Pit--Claudel, Pierre-Marie Pédrot, Daniel
+de Rauglaudre, Lionel Rieg, Gabriel Scherer, Thomas Sibut-Pinote,
+Matthieu Sozeau, Arnaud Spiwack, Paul Steckler, Enrico Tassi, Laurent
+Théry, Nickolai Zeldovich and Théo Zimmermann. The development process
+was coordinated by Hugo Herbelin and Matthieu Sozeau with the help of
+Maxime Dénès, who was also in charge of the release process.
+
+Many power users helped to improve the design of the new features via
+the bug tracker, the pull request system, the {\Coq} development mailing
+list or the coq-club mailing list. Special thanks to the users who
+contributed patches and intensive brain-storming and code reviews,
+starting with Cyril Cohen, Jason Gross, Robbert Krebbers, Jonathan
+Leivent, Xavier Leroy, Gregory Malecha, Clément Pit--Claudel, Gabriel
+Scherer and Beta Ziliani. It would however be impossible to mention
+exhaustively the names of everybody who to some extent influenced the
+development.
+
+Version 8.6 is the first release of {\Coq} developed on a time-based
+development cycle. Its development spanned 10 months from the release of
+{\Coq} 8.5 and was based on a public roadmap. To date, it contains more
+external contributions than any previous {\Coq} system. Code reviews
+were systematically done before integration of new features, with an
+important focus given to compatibility and performance issues, resulting
+in a hopefully more robust release than {\Coq} 8.5.
+
+Coq Enhancement Proposals (CEPs for short) were introduced by Enrico
+Tassi to provide more visibility and a discussion period on new
+features, they are publicly available \url{https://github.com/coq/ceps}.
+
+Started during this period, an effort is led by Yves Bertot and Maxime
+Dénès to put together a {\Coq} consortium.
+
+\begin{flushright}
+Paris, November 2016,\\
+Matthieu Sozeau and the {\Coq} development team\\
+\end{flushright}
+
%new Makefile
diff --git a/doc/refman/RefMan-syn.tex b/doc/refman/RefMan-syn.tex
index 1f08b6a2f1..1fcc1c0df4 100644
--- a/doc/refman/RefMan-syn.tex
+++ b/doc/refman/RefMan-syn.tex
@@ -321,6 +321,10 @@ Sometimes, a notation is expected only for the parser.
To do so, the option {\em only parsing} is allowed in the list of modifiers of
\texttt{Notation}.
+Conversely, the {\em only printing} can be used to declare
+that a notation should only be used for printing and should not declare a
+parsing rule. In particular, such notations do not modify the parser.
+
\subsection{The \texttt{Infix} command
\comindex{Infix}}
@@ -480,6 +484,7 @@ Locate "exists _ .. _ , _".
& $|$ & {\ident} {\tt global} \\
& $|$ & {\ident} {\tt bigint} \\
& $|$ & {\tt only parsing} \\
+ & $|$ & {\tt only printing} \\
& $|$ & {\tt format} {\str}
\end{tabular}
\end{centerframe}
@@ -584,6 +589,14 @@ Notation "[| t * ( x , y , .. , z ) ; ( a , b , .. , c ) * u |]" :=
(t at level 39).
\end{coq_example*}
+Recursive patterns can occur several times on the right-hand side.
+Here is an example:
+
+\begin{coq_example*}
+Notation "[> a , .. , b <]" :=
+ (cons a .. (cons b nil) .., cons b .. (cons a nil) ..).
+\end{coq_example*}
+
Notations with recursive patterns can be reserved like standard
notations, they can also be declared within interpretation scopes (see
section \ref{scopes}).
@@ -629,7 +642,16 @@ empty. Here is an example of recursive notation with closed binders:
\begin{coq_example*}
Notation "'mylet' f x .. y := t 'in' u":=
(let f := fun x => .. (fun y => t) .. in u)
- (x closed binder, y closed binder, at level 200, right associativity).
+ (at level 200, x closed binder, y closed binder, right associativity).
+\end{coq_example*}
+
+A recursive pattern for binders can be used in position of a recursive
+pattern for terms. Here is an example:
+
+\begin{coq_example*}
+Notation ``'FUNAPP' x .. y , f'' :=
+ (fun x => .. (fun y => (.. (f x) ..) y ) ..)
+ (at level 200, x binder, y binder, right associativity).
\end{coq_example*}
\subsection{Summary}
@@ -789,13 +811,13 @@ constant have to be interpreted in a given scope. The command is
\begin{quote}
{\tt Arguments} {\qualid} \nelist{\name {\tt \%}\scope}{}
\end{quote}
-where the list is the list of the arguments of {\qualid} eventually
-annotated with their {\scope}. Grouping round parentheses can
-be used to decorate multiple arguments with the same scope.
-{\scope} can be either a scope name or its delimiting key. For example
-the following command puts the first two arguments of {\tt plus\_fct}
-in the scope delimited by the key {\tt F} ({\tt Rfun\_scope}) and the
-last argument in the scope delimited by the key {\tt R} ({\tt R\_scope}).
+where the list is a prefix of the list of the arguments of {\qualid} eventually
+annotated with their {\scope}. Grouping round parentheses can be used to
+decorate multiple arguments with the same scope. {\scope} can be either a scope
+name or its delimiting key. For example the following command puts the first two
+arguments of {\tt plus\_fct} in the scope delimited by the key {\tt F} ({\tt
+ Rfun\_scope}) and the last argument in the scope delimited by the key {\tt R}
+({\tt R\_scope}).
\begin{coq_example*}
Arguments plus_fct (f1 f2)%F x%R.
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index c4ea1f5f9c..01dc1dec9b 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -46,13 +46,13 @@ goal selector (see Section \ref{ltac:selector}).
If no selector is specified, the default
selector (see Section \ref{default-selector}) is used.
-\newcommand{\selector}{\nterm{selector}}
+\newcommand{\toplevelselector}{\nterm{toplevel\_selector}}
\begin{tabular}{lcl}
-{\commandtac} & ::= & {\selector} {\tt :} {\tac} {\tt .}\\
+{\commandtac} & ::= & {\toplevelselector} {\tt :} {\tac} {\tt .}\\
& $|$ & {\tac} {\tt .}
\end{tabular}
-\subsection[\tt Set Default Goal Selector ``\selector''.]
- {\tt Set Default Goal Selector ``\selector''.
+\subsection[\tt Set Default Goal Selector ``\toplevelselector''.]
+ {\tt Set Default Goal Selector ``\toplevelselector''.
\optindex{Default Goal Selector}
\label{default-selector}}
After using this command, the default selector -- used when no selector
@@ -263,6 +263,16 @@ Defined.
This tactic behaves like {\tt refine}, but it does not shelve any
subgoal. It does not perform any beta-reduction either.
+\item {\tt notypeclasses refine \term}\tacindex{notypeclasses refine}
+
+ This tactic behaves like {\tt refine} except it performs typechecking
+ without resolution of typeclasses.
+
+\item {\tt simple notypeclasses refine \term}\tacindex{simple
+ notypeclasses refine}
+
+ This tactic behaves like {\tt simple refine} except it performs typechecking
+ without resolution of typeclasses.
\end{Variants}
\subsection{\tt apply \term}
@@ -1278,7 +1288,7 @@ in the list of subgoals remaining to prove.
In particular, \texttt{pose proof {\term} as {\ident}} behaves as
\texttt{assert ({\ident} := {\term})} and \texttt{pose proof {\term}
- as {\intropattern}\tacindex{pose proof}} is the same as applying
+ as {\intropattern}} is the same as applying
the {\intropattern} to {\term}.
\item \texttt{enough ({\ident} :\ {\form})}\tacindex{enough}
@@ -1491,10 +1501,10 @@ the local context.
\tacindex{contradiction}
This tactic applies to any goal. The {\tt contradiction} tactic
-attempts to find in the current context (after all {\tt intros}) one
-hypothesis that is equivalent to {\tt False}. It permits to prune
-irrelevant cases. This tactic is a macro for the tactics sequence
-{\tt intros; elimtype False; assumption}.
+attempts to find in the current context (after all {\tt intros}) an
+hypothesis that is equivalent to an empty inductive type (e.g. {\tt
+ False}), to the negation of a singleton inductive type (e.g. {\tt
+ True} or {\tt x=x}), or two contradictory hypotheses.
\begin{ErrMsgs}
\item \errindex{No such assumption}
@@ -2280,6 +2290,21 @@ hypothesis.
\end{Variants}
+\optindex{Structural Injection}
+
+It is possible to ensure that \texttt{injection {\term}} erases the
+original hypothesis and leaves the generated equalities in the context
+rather than putting them as antecedents of the current goal, as if
+giving \texttt{injection {\term} as} (with an empty list of names). To
+obtain this behavior, the option {\tt Set Structural Injection} must
+be activated. This option is off by default.
+
+By default, \texttt{injection} only creates new equalities between
+terms whose type is in sort \texttt{Type} or \texttt{Set}, thus
+implementing a special behavior for objects that are proofs
+of a statement in \texttt{Prop}. This behavior can be turned off
+by setting the option \texttt{Set Keep Proof Equalities}.
+\optindex{Keep Proof Equalities}
\subsection{\tt inversion \ident}
\tacindex{inversion}
@@ -2299,6 +2324,14 @@ latter is first introduced in the local context using
stock the lemmas whenever the same instance needs to be inverted
several times. See Section~\ref{Derive-Inversion}.
+\Rem Part of the behavior of the \texttt{inversion} tactic is to generate
+equalities between expressions that appeared in the hypothesis that is
+being processed. By default, no equalities are generated if they relate
+two proofs (i.e. equalities between terms whose type is in
+sort \texttt{Prop}). This behavior can be turned off by using the option
+\texttt{Set Keep Proof Equalities.}
+\optindex{Keep Proof Equalities}
+
\begin{Variants}
\item \texttt{inversion \num}
@@ -2872,6 +2905,9 @@ activated, {\tt subst} also deals with the following corner cases:
subst} would be necessary to replace {\ident$_2$} by $t$ or $t'$
respectively.
+\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}.
@@ -3030,8 +3066,10 @@ $\beta$ (reduction of functional application), $\delta$ (unfolding of
transparent constants, see \ref{Transparent}), $\iota$ (reduction of
pattern-matching over a constructed term, and unfolding of {\tt fix}
and {\tt cofix} expressions) and $\zeta$ (contraction of local
-definitions), the flag are either {\tt beta}, {\tt delta}, {\tt iota}
-or {\tt zeta}. The {\tt delta} flag itself can be refined into {\tt
+definitions), the flags are either {\tt beta}, {\tt delta},
+{\tt match}, {\tt fix}, {\tt cofix}, {\tt iota} or {\tt zeta}.
+The {\tt iota} flag is a shorthand for {\tt match}, {\tt fix} and {\tt cofix}.
+The {\tt delta} flag itself can be refined into {\tt
delta [\qualid$_1$\ldots\qualid$_k$]} or {\tt delta
-[\qualid$_1$\ldots\qualid$_k$]}, restricting in the first case the
constants to unfold to the constants listed, and restricting in the
@@ -3279,6 +3317,16 @@ reduced to \texttt{S t}.
\end{Variants}
+\begin{quote}
+\optindex{Refolding Reduction}
+{\tt Refolding Reduction}
+\end{quote}
+
+This option (off by default) controls the use of the refolding strategy
+of {\tt cbn} while doing reductions in unification, type inference and
+tactic applications. It can result in expensive unifications, as
+refolding currently uses a potentially exponential heuristic.
+
\subsection{\tt unfold \qualid}
\tacindex{unfold}
\label{unfold}
@@ -3451,12 +3499,11 @@ hints of the database named {\tt core}.
Uses the hint databases $\ident_1$ \dots\ $\ident_n$ in addition to
the database {\tt core}. See Section~\ref{Hints-databases} for the
list of pre-defined databases and the way to create or extend a
- database. This option can be combined with the previous one.
+ database.
\item {\tt auto with *}
- Uses all existing hint databases, minus the special database
- {\tt v62}. See Section~\ref{Hints-databases}
+ Uses all existing hint databases. See Section~\ref{Hints-databases}
\item \texttt{auto using} \nterm{lemma}$_1$ {\tt ,} {\ldots} {\tt ,} \nterm{lemma}$_n$
@@ -3465,9 +3512,17 @@ hints of the database named {\tt core}.
$lemma_i$ is an inductive type, it is the collection of its
constructors which is added as hints.
-\item \texttt{auto using} \nterm{lemma}$_1$ {\tt ,} {\ldots} {\tt ,} \nterm{lemma}$_n$ with \ident$_1$ {\ldots} \ident$_n$
+\item {\tt info\_auto}
- This combines the effects of the {\tt using} and {\tt with} options.
+ Behaves like {\tt auto} but shows the tactics it uses to solve the goal.
+ This variant is very useful for getting a better understanding of automation,
+ or to know what lemmas/assumptions were used.
+
+\item {\tt \zeroone{info\_}auto \zeroone{\num}} \zeroone{{\tt using} \nterm{lemma}$_1$
+ {\tt ,} {\ldots} {\tt ,} \nterm{lemma}$_n$} \zeroone{{\tt with}
+ \ident$_1$ {\ldots} \ident$_n$}
+
+ This is the most general form, combining the various options.
\item {\tt trivial}\tacindex{trivial}
@@ -3479,6 +3534,14 @@ hints of the database named {\tt core}.
\item \texttt{trivial with *}
+\item \texttt{trivial using} \nterm{lemma}$_1$ {\tt ,} {\ldots} {\tt ,} \nterm{lemma}$_n$
+
+\item {\tt info\_trivial}
+
+\item {\tt \zeroone{info\_}trivial} \zeroone{{\tt using} \nterm{lemma}$_1$
+ {\tt ,} {\ldots} {\tt ,} \nterm{lemma}$_n$} \zeroone{{\tt with}
+ \ident$_1$ {\ldots} \ident$_n$}
+
\end{Variants}
\Rem {\tt auto} either solves completely the goal or else leaves it
@@ -3492,8 +3555,8 @@ intact. \texttt{auto} and \texttt{trivial} never fail.
This tactic generalizes {\tt auto}. While {\tt auto} does not try
resolution hints which would leave existential variables in the goal,
-{\tt eauto} does try them (informally speaking, it uses {\tt eapply}
-where {\tt auto} uses {\tt apply}).
+{\tt eauto} does try them (informally speaking, it uses
+{\tt simple eapply} where {\tt auto} uses {\tt simple apply}).
As a consequence, {\tt eauto} can solve such a goal:
\begin{coq_eval}
@@ -3508,8 +3571,17 @@ eauto.
Abort.
\end{coq_eval}
-Note that {\tt ex\_intro} should be declared as an
-hint.
+Note that {\tt ex\_intro} should be declared as a hint.
+
+\begin{Variants}
+
+\item {\tt \zeroone{info\_}eauto \zeroone{\num}} \zeroone{{\tt using} \nterm{lemma}$_1$
+ {\tt ,} {\ldots} {\tt ,} \nterm{lemma}$_n$} \zeroone{{\tt with}
+ \ident$_1$ {\ldots} \ident$_n$}
+
+ The various options for eauto are the same as for auto.
+
+\end{Variants}
\SeeAlso Section~\ref{Hints-databases}
@@ -3655,19 +3727,22 @@ command to add a hint to some databases \ident$_1$, \dots, \ident$_n$ is
The {\hintdef} is one of the following expressions:
\begin{itemize}
-\item {\tt Resolve \term}
+\item {\tt Resolve \term {\zeroone{{\tt |} \zeroone{\num} \zeroone{\pattern}}}}
\comindex{Hint Resolve}
This command adds {\tt simple apply {\term}} to the hint list
with the head symbol of the type of \term. The cost of that hint is
- the number of subgoals generated by {\tt simple apply {\term}}.
+ the number of subgoals generated by {\tt simple apply {\term}} or \num
+ if specified. The associated pattern is inferred from the conclusion
+ of the type of \term or the given \pattern if specified.
%{\tt auto} actually uses a slightly modified variant of {\tt simple apply} with use_metas_eagerly_in_conv_on_closed_terms set to false
- % Is it really needed?
- %% In case the inferred type of \term\ does not start with a product
- %% the tactic added in the hint list is {\tt exact {\term}}. In case
- %% this type can however be reduced to a type starting with a product,
- %% the tactic {\tt apply {\term}} is also stored in the hints list.
+ In case the inferred type of \term\ does not start with a product
+ the tactic added in the hint list is {\tt exact {\term}}.
+% Actually, a slightly restricted version is used (no conversion on the head symbol)
+ In case
+ this type can however be reduced to a type starting with a product,
+ the tactic {\tt simple apply {\term}} is also stored in the hints list.
If the inferred type of \term\ contains a dependent quantification
on a variable which occurs only in the premisses of the type and not
@@ -3697,6 +3772,17 @@ The {\hintdef} is one of the following expressions:
Adds each \texttt{Resolve} {\term$_i$}.
+ \item {\tt Resolve -> \term}
+
+ Adds the left-to-right implication of an equivalence as a hint
+ (informally the hint will be used as {\tt apply <- \term},
+ although as mentionned before, the tactic actually used is
+ a restricted version of apply).
+
+ \item {\tt Resolve <- \term}
+
+ Adds the right-to-left implication of an equivalence as a hint.
+
\end{Variants}
\item \texttt{Immediate {\term}}
@@ -3832,7 +3918,7 @@ Abort.
\comindex{Hint Cut}
\textit{Warning:} these hints currently only apply to typeclass proof search and
- the \texttt{typeclasses eauto} tactic.
+ the \texttt{typeclasses eauto} tactic (\ref{typeclasseseauto}).
This command can be used to cut the proof-search tree according to a
regular expression matching paths to be cut. The grammar for regular
@@ -3924,8 +4010,8 @@ Several hint databases are defined in the \Coq\ standard library. The
actual content of a database is the collection of the hints declared
to belong to this database in each of the various modules currently
loaded. Especially, requiring new modules potentially extend a
-database. At {\Coq} startup, only the {\tt core} and {\tt v62}
-databases are non empty and can be used.
+database. At {\Coq} startup, only the {\tt core} database is non empty
+and can be used.
\begin{description}
@@ -3960,18 +4046,8 @@ databases are non empty and can be used.
from the \texttt{Classes} directory.
\end{description}
-There is also a special database called {\tt v62}. It collects all
-hints that were declared in the versions of {\Coq} prior to version
-6.2.4 when the databases {\tt core}, {\tt arith}, and so on were
-introduced. The purpose of the database {\tt v62} is to ensure
-compatibility with further versions of {\Coq} for developments done in
-versions prior to 6.2.4 ({\tt auto} being replaced by {\tt auto with v62}).
-The database {\tt v62} is intended not to be extended (!). It is not
-included in the hint databases list used in the {\tt auto with *} tactic.
-
-Furthermore, you are advised not to put your own hints in the
-{\tt core} database, but use one or several databases specific to your
-development.
+You are advised not to put your own hints in the {\tt core} database,
+but use one or several databases specific to your development.
\subsection{\tt Remove Hints \term$_1$ \mbox{\dots} \term$_n$ :~ \ident$_1$
\mbox{\dots} \ident$_m$}
@@ -4332,22 +4408,23 @@ vernacular command and printed using {\nobreak {\tt Print Firstorder
Tries to solve the goal with {\tac} when no logical rule may apply.
- \item {\tt firstorder with \ident$_1$ \dots\ \ident$_n$ }
- \tacindex{firstorder with}
-
- Adds lemmas \ident$_1$ \dots\ \ident$_n$ to the proof-search
- environment.
-
\item {\tt firstorder using {\qualid}$_1$ , \dots\ , {\qualid}$_n$ }
\tacindex{firstorder using}
- Adds lemmas in {\tt auto} hints bases {\qualid}$_1$ \dots\ {\qualid}$_n$
- to the proof-search environment. If {\qualid}$_i$ refers to an inductive
- type, it is the collection of its constructors which is added as hints.
+ Adds lemmas {\qualid}$_1$ \dots\ {\qualid}$_n$ to the proof-search
+ environment. If {\qualid}$_i$ refers to an inductive type, it is
+ the collection of its constructors which are added to the
+ proof-search environment.
+
+ \item {\tt firstorder with \ident$_1$ \dots\ \ident$_n$ }
+ \tacindex{firstorder with}
+
+ Adds lemmas from {\tt auto} hint bases \ident$_1$ \dots\ \ident$_n$
+ to the proof-search environment.
-\item \texttt{firstorder using {\qualid}$_1$ , \dots\ , {\qualid}$_n$ with \ident$_1$ \dots\ \ident$_n$}
+\item \texttt{firstorder {\tac} using {\qualid}$_1$ , \dots\ , {\qualid}$_n$ with \ident$_1$ \dots\ \ident$_n$}
- This combines the effects of the {\tt using} and {\tt with} options.
+ This combines the effects of the different variants of \texttt{firstorder}.
\end{Variants}
diff --git a/doc/refman/RefMan-uti.tex b/doc/refman/RefMan-uti.tex
index c282083b5c..9962ce9961 100644
--- a/doc/refman/RefMan-uti.tex
+++ b/doc/refman/RefMan-uti.tex
@@ -102,7 +102,7 @@ generator using for instance the command:
This command generates a file \texttt{Makefile} that can be used to
compile all the sources of the current project. It follows the
-syntax described by the output of \texttt{\% coq\_makefile ----help}.
+syntax described by the output of \texttt{\% coq\_makefile -{}-help}.
Once the \texttt{Makefile} file has been generated a first time, it
can be used by the \texttt{make} command to compile part or all of
the project. Note that once it has been generated once, as soon as
@@ -112,8 +112,8 @@ automatically regenerated by an invocation of \texttt{make}.
The following command generates a minimal example of
\texttt{\_CoqProject} file:
\begin{quotation}
-\texttt{\% \{ echo '-R .} \textit{MyFancyLib} \texttt{' ; find . -name
- '*.v' -print \} > \_CoqProject}
+\texttt{\% ( echo "-R .\ }\textit{MyFancyLib}\texttt{" ; find .\ -name
+ "*.v" -print ) > \_CoqProject}
\end{quotation}
when executed at the root of the directory containing the
project. Here the \texttt{\_CoqProject} lists all the \texttt{.v} files
@@ -251,7 +251,7 @@ to the \Coq\ toplevel or conversely from the \Coq\ toplevel to some
files.
{\ProofGeneral} is developed and distributed independently of the
-system \Coq. It is freely available at \verb!proofgeneral.inf.ed.ac.uk!.
+system \Coq. It is freely available at \verb!https://proofgeneral.github.io/!.
\section[Module specification]{Module specification\label{gallina}\ttindex{gallina}}
diff --git a/doc/refman/biblio.bib b/doc/refman/biblio.bib
index 70ee1f41f0..e69725838e 100644
--- a/doc/refman/biblio.bib
+++ b/doc/refman/biblio.bib
@@ -1199,7 +1199,7 @@ Decomposition}},
@Misc{ProofGeneral,
author = {David Aspinall},
title = {Proof General},
- note = {\url{http://proofgeneral.inf.ed.ac.uk/}}
+ note = {\url{https://proofgeneral.github.io/}}
}
@Book{CoqArt,
diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template
index fb45777e7f..9216c81fcd 100644
--- a/doc/stdlib/index-list.html.template
+++ b/doc/stdlib/index-list.html.template
@@ -616,5 +616,6 @@ through the <tt>Require Import</tt> command.</p>
theories/Compat/AdmitAxiom.v
theories/Compat/Coq84.v
theories/Compat/Coq85.v
+ theories/Compat/Coq86.v
</dd>
</dl>
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-02 05:01:39 +0000