aboutsummaryrefslogtreecommitdiff
path: root/doc
diff options
context:
space:
mode:
Diffstat (limited to 'doc')
-rw-r--r--doc/LICENSE10
-rw-r--r--doc/common/macros.tex1
-rw-r--r--doc/refman/Classes.tex27
-rw-r--r--doc/refman/RefMan-com.tex14
-rw-r--r--doc/refman/RefMan-lib.tex1
-rw-r--r--doc/refman/RefMan-ltac.tex10
-rw-r--r--doc/refman/RefMan-oth.tex5
-rw-r--r--doc/refman/RefMan-pro.tex8
-rw-r--r--doc/refman/RefMan-sch.tex2
-rw-r--r--doc/refman/RefMan-syn.tex406
-rw-r--r--doc/refman/RefMan-tac.tex16
-rw-r--r--doc/stdlib/index-list.html.template8
12 files changed, 329 insertions, 179 deletions
diff --git a/doc/LICENSE b/doc/LICENSE
index ada22e6690..0aa0d629e8 100644
--- a/doc/LICENSE
+++ b/doc/LICENSE
@@ -25,16 +25,6 @@ the PostScript, PDF and html outputs) are copyright (c) INRIA
distributed under the terms of the Lesser General Public License
version 2.1 or later.
-The FAQ (Coq for the Clueless) is a work by Pierre Castéran, Hugo
-Herbelin, Florent Kirchner, Benjamin Monate, and Julien Narboux. All
-documents (the LaTeX source and the PostScript, PDF and html outputs)
-are copyright (c) INRIA 2004-2006. The material connected to the FAQ
-(Coq for the Clueless) may be distributed only subject to the terms
-and conditions set forth in the Open Publication License, v1.0 or
-later (the latest version is presently available at
-http://www.opencontent.org/openpub/). Options A and B are *not*
-elected.
-
The Tutorial on [Co-]Inductive Types in Coq is a work by Pierre
Castéran and Eduardo Gimenez. All related documents (the LaTeX and
BibTeX sources and the PostScript, PDF and html outputs) are copyright
diff --git a/doc/common/macros.tex b/doc/common/macros.tex
index 81def1674c..6a28c5b3d1 100644
--- a/doc/common/macros.tex
+++ b/doc/common/macros.tex
@@ -182,6 +182,7 @@
\newcommand{\declnotation}{\nterm{decl\_notation}}
\newcommand{\symbolentry}{\nterm{symbol}}
\newcommand{\modifiers}{\nterm{modifiers}}
+\newcommand{\binderinterp}{\nterm{binder\_interp}}
\newcommand{\localdef}{\nterm{local\_def}}
\newcommand{\localdecls}{\nterm{local\_decls}}
\newcommand{\ident}{\nterm{ident}}
diff --git a/doc/refman/Classes.tex b/doc/refman/Classes.tex
index 6e76d04e77..da798a238e 100644
--- a/doc/refman/Classes.tex
+++ b/doc/refman/Classes.tex
@@ -492,26 +492,6 @@ 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}
-\emph{Deprecated since 8.7}
-
-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}
-\emph{Deprecated since 8.7}
-
-This option allows eta-conversion for functions and records during
-unification of type-classes. This option is unsupported since 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}
@@ -525,13 +505,6 @@ 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{Typeclass 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{Typeclass Resolution For Conversion}
diff --git a/doc/refman/RefMan-com.tex b/doc/refman/RefMan-com.tex
index 04a8a25c12..5b73ac00a6 100644
--- a/doc/refman/RefMan-com.tex
+++ b/doc/refman/RefMan-com.tex
@@ -241,6 +241,20 @@ The following command-line options are recognized by the commands {\tt
Collapse the universe hierarchy of {\Coq}. Warning: this makes the
logic inconsistent.
+\item[{\tt -mangle-names} {\em ident}]\ %
+
+ Experimental: Do not depend on this option.
+
+ Replace Coq's auto-generated name scheme with names of the form
+ {\tt ident0}, {\tt ident1}, \ldots etc.
+ The command {\tt Set Mangle Names}\optindex{Mangle Names} turns
+ the behavior on in a document, and {\tt Set Mangle Names Prefix "ident"}
+ \optindex{Mangle Names Prefix} changes the used prefix.
+
+ This feature is intended to be used as a linter for developments that want
+ to be robust to changes in the auto-generated name scheme. The options are
+ provided to facilitate tracking down problems.
+
\item[{\tt -compat} {\em version}]\ %
Attempt to maintain some backward-compatibility with a previous version.
diff --git a/doc/refman/RefMan-lib.tex b/doc/refman/RefMan-lib.tex
index c8e8443026..89f5be8438 100644
--- a/doc/refman/RefMan-lib.tex
+++ b/doc/refman/RefMan-lib.tex
@@ -55,6 +55,7 @@ Figure~\ref{init-notations}.
\hline
Notation & Precedence & Associativity \\
\hline
+\verb!_ -> _! & 99 & right \\
\verb!_ <-> _! & 95 & no \\
\verb!_ \/ _! & 85 & right \\
\verb!_ /\ _! & 80 & right \\
diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex
index c4c0435c5f..0a4d0ef9aa 100644
--- a/doc/refman/RefMan-ltac.tex
+++ b/doc/refman/RefMan-ltac.tex
@@ -1156,16 +1156,6 @@ without having to cut manually the proof in smaller lemmas.
It may be useful to generate lemmas minimal w.r.t. the assumptions they depend
on. This can be obtained thanks to the option below.
-\begin{quote}
-\optindex{Shrink Abstract}
-{\tt Set Shrink Abstract}
-\end{quote}
-\emph{Deprecated since 8.7}
-
-When set (default), all lemmas generated through \texttt{abstract {\tacexpr}}
-and \texttt{transparent\_abstract {\tacexpr}} are quantified only over the
-variables that appear in the term constructed by \texttt{\tacexpr}.
-
\begin{Variants}
\item \texttt{abstract {\tacexpr} using {\ident}}.\\
Give explicitly the name of the auxiliary lemma.
diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex
index 1cd23c9297..bef31d3fa5 100644
--- a/doc/refman/RefMan-oth.tex
+++ b/doc/refman/RefMan-oth.tex
@@ -513,6 +513,9 @@ This command loads the file named {\ident}{\tt .v}, searching
successively in each of the directories specified in the {\em
loadpath}. (see Section~\ref{loadpath})
+Files loaded this way cannot leave proofs open, and neither the {\tt
+ Load} command can be use inside a proof.
+
\begin{Variants}
\item {\tt Load {\str}.}\label{Load-str}\\
Loads the file denoted by the string {\str}, where {\str} is any
@@ -530,6 +533,8 @@ successively in each of the directories specified in the {\em
\begin{ErrMsgs}
\item \errindex{Can't find file {\ident} on loadpath}
+\item \errindex{Load is not supported inside proofs}
+\item \errindex{Files processed by Load cannot leave open proofs}
\end{ErrMsgs}
\section[Compiled files]{Compiled files\label{compiled}\index{Compiled files}}
diff --git a/doc/refman/RefMan-pro.tex b/doc/refman/RefMan-pro.tex
index 6b24fdde79..bd74a40d7c 100644
--- a/doc/refman/RefMan-pro.tex
+++ b/doc/refman/RefMan-pro.tex
@@ -298,15 +298,19 @@ subgoals which clutter your screen.
\begin{Variant}
\item {\tt Focus {\num}.}\\
This focuses the attention on the $\num^{th}$ subgoal to prove.
-
\end{Variant}
+\emph{This command is deprecated since 8.8: prefer the use of bullets or
+ focusing brackets instead, including {\tt {\num}: \{}}.
+
\subsection[\tt Unfocus.]{\tt Unfocus.\comindex{Unfocus}}
This command restores to focus the goal that were suspended by the
last {\tt Focus} command.
+\emph{This command is deprecated since 8.8.}
+
\subsection[\tt Unfocused.]{\tt Unfocused.\comindex{Unfocused}}
-Succeeds in the proof is fully unfocused, fails is there are some
+Succeeds in the proof if fully unfocused, fails if there are some
goals out of focus.
\subsection[\tt \{ \textrm{and} \}]{\tt \{ \textrm{and} \}\comindex{\{}\comindex{\}}}\label{curlybacket}
diff --git a/doc/refman/RefMan-sch.tex b/doc/refman/RefMan-sch.tex
index 30724759d2..6004711235 100644
--- a/doc/refman/RefMan-sch.tex
+++ b/doc/refman/RefMan-sch.tex
@@ -127,7 +127,6 @@ conclusion is {\tt (n:nat)(even n)->(Q n)}.
\optindex{Boolean Equality Schemes}
\optindex{Elimination Schemes}
\optindex{Nonrecursive Elimination Schemes}
-\optindex{Record Elimination Schemes}
\optindex{Case Analysis Schemes}
\optindex{Decidable Equality Schemes}
\optindex{Rewriting Schemes}
@@ -144,7 +143,6 @@ and {\tt Record} (see~\ref{Record}) do not have an automatic
declaration of the induction principles. It can be activated with the
command {\tt Set Nonrecursive Elimination Schemes}. It can be
deactivated again with {\tt Unset Nonrecursive Elimination Schemes}.
-{\tt Record Elimination Schemes} is a deprecated alias of {\tt Nonrecursive Elimination Schemes}.
In addition, the {\tt Case Analysis Schemes} flag governs the generation of
case analysis lemmas for inductive types, i.e. corresponding to the
diff --git a/doc/refman/RefMan-syn.tex b/doc/refman/RefMan-syn.tex
index eecb5ac7c0..836753db16 100644
--- a/doc/refman/RefMan-syn.tex
+++ b/doc/refman/RefMan-syn.tex
@@ -3,25 +3,32 @@
In this chapter, we introduce advanced commands to modify the way
{\Coq} parses and prints objects, i.e. the translations between the
-concrete and internal representations of terms and commands. The main
-commands are {\tt Notation} and {\tt Infix} which are described in
-section \ref{Notation}. It also happens that the same symbolic
-notation is expected in different contexts. To achieve this form of
-overloading, {\Coq} offers a notion of interpretation scope. This is
-described in Section~\ref{scopes}.
-
-\Rem The commands {\tt Grammar}, {\tt Syntax} and {\tt Distfix} which
-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}.
+concrete and internal representations of terms and commands.
+
+The main commands to provide custom symbolic notations for terms are
+{\tt Notation} and {\tt Infix}. They are described in Section
+\ref{Notation}. There is also a variant of {\tt Notation} which does
+not modify the parser. This provides with a form of abbreviation and
+it is described in Section~\ref{Abbreviations}. It is sometimes
+expected that the same symbolic notation has different meanings in
+different contexts. To achieve this form of overloading, {\Coq} offers
+a notion of interpretation scope. This is described in
+Section~\ref{scopes}.
+
+The main command to provide custom notations for tactics is {\tt
+ Tactic Notation}. It is described in Section~\ref{Tactic-Notation}.
+
+% No need any more to remind this
+%% \Rem The commands {\tt Grammar}, {\tt Syntax} and {\tt Distfix} which
+%% 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.
\section[Notations]{Notations\label{Notation}
\comindex{Notation}}
\subsection{Basic notations}
-A {\em notation} is a symbolic abbreviation denoting some term
+A {\em notation} is a symbolic expression denoting some term
or term pattern.
A typical notation is the use of the infix symbol \verb=/\= to denote
@@ -37,7 +44,7 @@ string \verb="A /\ B"= (called a {\em notation}) tells how it is
symbolically written.
A notation is always surrounded by double quotes (except when the
-abbreviation is a single identifier; see \ref{Abbreviations}). The
+abbreviation has the form of an ordinary applicative expression; 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
@@ -61,7 +68,7 @@ syntactic expression (see \ref{ReservedNotation}), explicit precedences and
associativity rules have to be given.
\Rem The right-hand side of a notation is interpreted at the time the
-notation is given. In particular, implicit arguments (see
+notation is given. In particular, disambiguation of constants, implicit arguments (see
Section~\ref{Implicit Arguments}), coercions (see
Section~\ref{Coercions}), etc. are resolved at the time of the
declaration of the notation.
@@ -105,8 +112,8 @@ parentheses are mandatory (this is a ``no associativity'')\footnote{
which {\Coq} is built, namely {\camlpppp}, currently does not implement the
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, so let's apply for instance a right
+We do not know of a special convention of the associativity of
+disjunction and conjunction, so let us apply for instance a right
associativity (which is the choice of {\Coq}).
Precedence levels and associativity rules of notations have to be
@@ -142,7 +149,8 @@ Notation "x = y" := (@eq _ x y) (at level 70, no associativity).
\end{coq_example*}
One can define {\em closed} notations whose both sides are symbols. In
-this case, the default precedence level for inner subexpression is 200.
+this case, the default precedence level for inner subexpression is
+200, and the default level for the notation itself is 0.
\begin{coq_eval}
Set Printing Depth 50.
@@ -150,7 +158,7 @@ Set Printing Depth 50.
(**** an incompatibility with the reserved notation ********)
\end{coq_eval}
\begin{coq_example*}
-Notation "( x , y )" := (@pair _ _ x y) (at level 0).
+Notation "( x , y )" := (@pair _ _ x y).
\end{coq_example*}
One can also define notations for binders.
@@ -161,17 +169,17 @@ Set Printing Depth 50.
(**** an incompatibility with the reserved notation ********)
\end{coq_eval}
\begin{coq_example*}
-Notation "{ x : A | P }" := (sig A (fun x => P)) (at level 0).
+Notation "{ x : A | P }" := (sig A (fun x => P)).
\end{coq_example*}
In the last case though, there is a conflict with the notation for
-type casts. This last notation, as shown by the command {\tt Print Grammar
+type casts. The notation for type casts, as shown by the command {\tt Print Grammar
constr} is at level 100. To avoid \verb=x : A= being parsed as a type cast,
it is necessary to put {\tt x} at a level below 100, typically 99. Hence, a
-correct definition is
+correct definition is the following.
\begin{coq_example*}
-Notation "{ x : A | P }" := (sig A (fun x => P)) (at level 0, x at level 99).
+Notation "{ x : A | P }" := (sig A (fun x => P)) (x at level 99).
\end{coq_example*}
%This change has retrospectively an effect on the notation for notation
@@ -182,14 +190,17 @@ Notation "{ x : A | P }" := (sig A (fun x => P)) (at level 0, x at level 99).
%Notation "{ A } + { B }" := (sumbool A B) (at level 0, A at level 99).
%\end{coq_example*}
-See the next section for more about factorization.
+More generally, it is required that notations are explicitly
+factorized on the left. See the next section for more about
+factorization.
\subsection{Simple factorization rules}
-{\Coq} extensible parsing is performed by Camlp5 which is essentially a
-LL1 parser. Hence, some care has to be taken not to hide already
-existing rules by new rules. Some simple left factorization work has
-to be done. Here is an example.
+{\Coq} extensible parsing is performed by {\camlpppp} which is
+essentially a LL1 parser: it decides which notation to parse by
+looking tokens from left to right. Hence, some care has to be taken
+not to hide already existing rules by new rules. Some simple left
+factorization work has to be done. Here is an example.
\begin{coq_eval}
(********** The next rule for notation _ < _ < _ produces **********)
@@ -242,17 +253,19 @@ on the {\Coq} printer. For example:
Check (and True True).
\end{coq_example}
-However, printing, especially pretty-printing, requires
-more care than parsing. We may want specific indentations,
-line breaks, alignment if on several lines, etc.
+However, printing, especially pretty-printing, also requires some
+care. We may want specific indentations, line breaks, alignment if on
+several lines, etc. For pretty-printing, {\Coq} relies on {\ocaml}
+formatting library, which provides indentation and automatic line
+breaks depending on page width by means of {\em formatting boxes}.
-The default printing of notations is very rudimentary. For printing a
-notation, a {\em formatting box} is opened in such a way that if the
+The default printing of notations is rudimentary. For printing a
+notation, a formatting box is opened in such a way that if the
notation and its arguments cannot fit on a single line, a line break
is inserted before the symbols of the notation and the arguments on
the next lines are aligned with the argument on the first line.
-A first, simple control that a user can have on the printing of a
+A first simple control that a user can have on the printing of a
notation is the insertion of spaces at some places of the
notation. This is performed by adding extra spaces between the symbols
and parameters: each extra space (other than the single space needed
@@ -277,6 +290,13 @@ Notation "'If' c1 'then' c2 'else' c3" := (IF_then_else c1 c2 c3)
\end{coq_example}
\end{small}
+\begin{coq_example}
+Check
+ (IF_then_else (IF_then_else True False True)
+ (IF_then_else True False True)
+ (IF_then_else True False True)).
+\end{coq_example}
+
A {\em format} is an extension of the string denoting the notation with
the possible following elements delimited by single quotes:
@@ -313,22 +333,15 @@ Notations do not survive the end of sections. No typing of the denoted
expression is performed at definition time. Type-checking is done only
at the time of use of the notation.
-\begin{coq_example}
-Check
- (IF_then_else (IF_then_else True False True)
- (IF_then_else True False True)
- (IF_then_else True False True)).
-\end{coq_example}
-
\Rem
Sometimes, a notation is expected only for the parser.
%(e.g. because
%the underlying parser of {\Coq}, namely {\camlpppp}, is LL1 and some extra
%rules are needed to circumvent the absence of factorization).
-To do so, the option {\em only parsing} is allowed in the list of modifiers of
+To do so, the option {\tt only parsing} is allowed in the list of modifiers of
\texttt{Notation}.
-Conversely, the {\em only printing} can be used to declare
+Conversely, the {\tt 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.
@@ -339,16 +352,16 @@ The \texttt{Infix} command is a shortening for declaring notations of
infix symbols. Its syntax is
\begin{quote}
-\noindent\texttt{Infix "{\symbolentry}" :=} {\qualid} {\tt (} \nelist{\em modifier}{,} {\tt )}.
+\noindent\texttt{Infix "{\symbolentry}" :=} {\term} {\tt (} \nelist{\em modifier}{,} {\tt )}.
\end{quote}
and it is equivalent to
\begin{quote}
-\noindent\texttt{Notation "x {\symbolentry} y" := ({\qualid} x y) (} \nelist{\em modifier}{,} {\tt )}.
+\noindent\texttt{Notation "x {\symbolentry} y" := ({\term} x y) (} \nelist{\em modifier}{,} {\tt )}.
\end{quote}
-where {\tt x} and {\tt y} are fresh names distinct from {\qualid}. Here is an example.
+where {\tt x} and {\tt y} are fresh names. Here is an example.
\begin{coq_example*}
Infix "/\" := and (at level 80, right associativity).
@@ -380,12 +393,14 @@ reserved. Hence their precedence and associativity cannot be changed.
\comindex{CoFixpoint {\ldots} where {\ldots}}
\comindex{Inductive {\ldots} where {\ldots}}}
-Thanks to reserved notations, the inductive, co-inductive, recursive
-and corecursive definitions can benefit of customized notations. To do
-this, insert a {\tt where} notation clause after the definition of the
-(co)inductive type or (co)recursive term (or after the definition of
-each of them in case of mutual definitions). The exact syntax is given
-on Figure~\ref{notation-syntax}. Here are examples:
+Thanks to reserved notations, the inductive, co-inductive, record,
+recursive and corecursive definitions can benefit of customized
+notations. To do this, insert a {\tt where} notation clause after the
+definition of the (co)inductive type or (co)recursive term (or after
+the definition of each of them in case of mutual definitions). The
+exact syntax is given on Figure~\ref{notation-syntax} for inductive,
+co-inductive, recursive and corecursive definitions and on
+Figure~\ref{record-syntax} for records. Here are examples:
\begin{coq_eval}
Set Printing Depth 50.
@@ -479,20 +494,28 @@ Locate "exists _ .. _ , _".
\\
\\
{\modifiers}
- & ::= & \nelist{\ident}{,} {\tt at level} {\naturalnumber} \\
- & $|$ & \nelist{\ident}{,} {\tt at next level} \\
- & $|$ & {\tt at level} {\naturalnumber} \\
- & $|$ & {\tt left associativity} \\
- & $|$ & {\tt right associativity} \\
- & $|$ & {\tt no associativity} \\
+ & ::= & {\tt at level} {\naturalnumber} \\
+ & $|$ & \nelist{\ident}{,} {\tt at level} {\naturalnumber} \zeroone{\binderinterp}\\
+ & $|$ & \nelist{\ident}{,} {\tt at next level} \zeroone{\binderinterp}\\
+ & $|$ & {\ident} {\binderinterp} \\
& $|$ & {\ident} {\tt ident} \\
- & $|$ & {\ident} {\tt binder} \\
- & $|$ & {\ident} {\tt closed binder} \\
& $|$ & {\ident} {\tt global} \\
& $|$ & {\ident} {\tt bigint} \\
+ & $|$ & {\ident} \zeroone{{\tt strict}} {\tt pattern} \zeroone{{\tt at level} {\naturalnumber}}\\
+ & $|$ & {\ident} {\tt binder} \\
+ & $|$ & {\ident} {\tt closed binder} \\
+ & $|$ & {\tt left associativity} \\
+ & $|$ & {\tt right associativity} \\
+ & $|$ & {\tt no associativity} \\
& $|$ & {\tt only parsing} \\
& $|$ & {\tt only printing} \\
- & $|$ & {\tt format} {\str}
+ & $|$ & {\tt format} {\str} \\
+\\
+\\
+{\binderinterp}
+ & ::= & {\tt as ident} \\
+ & $|$ & {\tt as pattern} \\
+ & $|$ & {\tt as strict pattern} \\
\end{tabular}
\end{centerframe}
\end{small}
@@ -500,9 +523,93 @@ Locate "exists _ .. _ , _".
\label{notation-syntax}
\end{figure}
-\subsection{Notations and simple binders}
+\subsection{Notations and binders}
+
+Notations can include binders. This section lists
+different ways to deal with binders. For further examples, see also
+Section~\ref{RecursiveNotationsWithBinders}.
+
+\subsubsection{Binders bound in the notation and parsed as identifiers}
-Notations can be defined for binders as in the example:
+Here is the basic example of a notation using a binder:
+
+\begin{coq_example*}
+Notation "'sigma' x : A , B" := (sigT (fun x : A => B))
+ (at level 200, x ident, A at level 200, right associativity).
+\end{coq_example*}
+
+The binding variables in the right-hand side that occur as a parameter
+of the notation (here {\tt x}) dynamically bind all the occurrences
+in their respective binding scope after instantiation of the
+parameters of the notation. This means that the term bound to {\tt B} can
+refer to the variable name bound to {\tt x} as shown in the following
+application of the notation:
+
+\begin{coq_example}
+Check sigma z : nat, z = 0.
+\end{coq_example}
+
+Notice the modifier {\tt x ident} in the declaration of the
+notation. It tells to parse {\tt x} as a single identifier.
+
+\subsubsection{Binders bound in the notation and parsed as patterns}
+
+In the same way as patterns can be used as binders, as in {\tt fun
+ '(x,y) => x+y} or {\tt fun '(existT \_ x \_) => x}, notations can be
+defined so that any pattern (in the sense of the entry {\pattern} of
+Figure~\ref{term-syntax-aux}) can be used in place of the
+binder. Here is an example:
+
+\begin{coq_eval}
+Reset Initial.
+\end{coq_eval}
+
+\begin{coq_example*}
+Notation "'subset' ' p , P " := (sig (fun p => P))
+ (at level 200, p pattern, format "'subset' ' p , P").
+\end{coq_example*}
+
+\begin{coq_example}
+Check subset '(x,y), x+y=0.
+\end{coq_example}
+
+The modifier {\tt p pattern} in the declaration of the notation
+tells to parse $p$ as a pattern. Note that a single
+variable is both an identifier and a pattern, so, e.g., the following
+also works:
+
+% Note: we rely on the notation of the standard library which does not
+% print the expected output, so we hide the output.
+\begin{coq_example}
+Check subset 'x, x=0.
+\end{coq_example}
+
+If one wants to prevent such a notation to be used for printing when the
+pattern is reduced to a single identifier, one has to use instead
+the modifier {\tt p strict pattern}. For parsing, however, a {\tt
+ strict pattern} will continue to include the case of a
+variable. Here is an example showing the difference:
+
+\begin{coq_example*}
+Notation "'subset_bis' ' p , P" := (sig (fun p => P))
+ (at level 200, p strict pattern).
+Notation "'subset_bis' p , P " := (sig (fun p => P))
+ (at level 200, p ident).
+\end{coq_example*}
+
+\begin{coq_example}
+Check subset_bis 'x, x=0.
+\end{coq_example}
+
+The default level for a {\tt pattern} is 0. One can use a different level by
+using {\tt pattern at level} $n$ where the scale is the same as the one for
+terms (Figure~\ref{init-notations}).
+
+\subsubsection{Binders bound in the notation and parsed as terms}
+
+Sometimes, for the sake of factorization of rules, a binder has to be
+parsed as a term. This is typically the case for a notation such as
+the following:
\begin{coq_eval}
Set Printing Depth 50.
@@ -510,18 +617,53 @@ Set Printing Depth 50.
(**** an incompatibility with the reserved notation ********)
\end{coq_eval}
\begin{coq_example*}
-Notation "{ x : A | P }" := (sig (fun x : A => P)) (at level 0).
+Notation "{ x : A | P }" := (sig (fun x : A => P))
+ (at level 0, x at level 99 as ident).
+\end{coq_example*}
+
+This is so because the grammar also contains rules starting with
+{\tt \{} and followed by a term, such as the rule for the notation
+ {\tt \{ A \} + \{ B \}} for the constant {\tt
+ sumbool}~(see Section~\ref{sumbool}).
+
+Then, in the rule, {\tt x ident} is replaced by {\tt x at level 99 as
+ ident} meaning that {\tt x} is parsed as a term at level 99 (as done
+in the notation for {\tt sumbool}), but that this term has actually to
+be an identifier.
+
+The notation {\tt \{ x | P \}} is already defined in the standard
+library with the {\tt as ident} modifier. We cannot redefine it but
+one can define an alternative notation, say {\tt \{ p such that P }\},
+using instead {\tt as pattern}.
+
+% Note, this conflicts with the default rule in the standard library, so
+% we don't show the
+\begin{coq_example*}
+Notation "{ p 'such' 'that' P }" := (sig (fun p => P))
+ (at level 0, p at level 99 as pattern).
\end{coq_example*}
-The binding variables in the left-hand-side that occur as a parameter
-of the notation naturally bind all their occurrences appearing in
-their respective scope after instantiation of the parameters of the
-notation.
+Then, the following works:
+\begin{coq_example}
+Check {(x,y) such that x+y=0}.
+\end{coq_example}
+
+To enforce that the pattern should not be used for printing when it
+is just an identifier, one could have said {\tt p at level
+ 99 as strict pattern}.
+
+Note also that in the absence of a {\tt as ident}, {\tt as strict
+ pattern} or {\tt as pattern} modifiers, the default is to consider
+subexpressions occurring in binding position and parsed as terms to be
+{\tt as ident}.
+
+\subsubsection{Binders not bound in the notation}
+\label{NotationsWithBinders}
-Contrastingly, the binding variables that are not a parameter of the
-notation do not capture the variables of same name that
-could appear in their scope after instantiation of the
-notation. E.g., for the notation
+We can also have binders in the right-hand side of a notation which
+are not themselves bound in the notation. In this case, the binders
+are considered up to renaming of the internal binder. E.g., for the
+notation
\begin{coq_example*}
Notation "'exists_different' n" := (exists p:nat, p<>n) (at level 200).
@@ -537,14 +679,6 @@ Set Printing Depth 50.
Fail Check (exists_different p).
\end{coq_example}
-\Rem Binding variables must not necessarily be parsed using the
-{\tt ident} entry. For factorization purposes, they can be said to be
-parsed at another level (e.g. {\tt x} in \verb="{ x : A | P }"= must be
-parsed at level 99 to be factorized with the notation
-\verb="{ A } + { B }"= for which {\tt A} can be any term).
-However, even if parsed as a term, this term must at the end be effectively
-a single identifier.
-
\subsection{Notations with recursive patterns}
\label{RecursiveNotations}
@@ -565,24 +699,22 @@ notation parses any number of time (but at least one time) a sequence
of expressions separated by the sequence of tokens $s$ (in the
example, $s$ is just ``{\tt ;}'').
-In the right-hand side, the term enclosed within {\tt ..} must be a
-pattern with two holes of the form $\phi([~]_E,[~]_I)$ where the first
-hole is occupied either by $x$ or by $y$ and the second hole is
-occupied by an arbitrary term $t$ called the {\it terminating}
-expression of the recursive notation. The subterm {\tt ..} $\phi(x,t)$
-{\tt ..} (or {\tt ..} $\phi(y,t)$ {\tt ..}) must itself occur at
-second position of the same pattern where the first hole is occupied
-by the other variable, $y$ or $x$. Otherwise said, the right-hand side
-must contain a subterm of the form either $\phi(x,${\tt ..}
-$\phi(y,t)$ {\tt ..}$)$ or $\phi(y,${\tt ..} $\phi(x,t)$ {\tt ..}$)$.
-The pattern $\phi$ is the {\em iterator} of the recursive notation
-and, of course, the name $x$ and $y$ can be chosen arbitrarily.
-
-The parsing phase produces a list of expressions which are used to
-fill in order the first hole of the iterating pattern which is
+The right-hand side must contain a subterm of the form either
+$\phi(x,${\tt ..} $\phi(y,t)$ {\tt ..}$)$ or $\phi(y,${\tt ..}
+$\phi(x,t)$ {\tt ..}$)$ where $\phi([~]_E,[~]_I)$, called the {\em
+ iterator} of the recursive notation is an arbitrary expression with
+distinguished placeholders and
+where $t$ is called the {\tt terminating expression} of the recursive
+notation. In the example, we choose the name s$x$ and $y$ but in
+practice they can of course be chosen arbitrarily. Note that the
+placeholder $[~]_I$ has to occur only once but the $[~]_E$ can occur
+several times.
+
+Parsing the notation produces a list of expressions which are used to
+fill the first placeholder of the iterating pattern which itself is
repeatedly nested as many times as the length of the list, the second
-hole being the nesting point. In the innermost occurrence of the
-nested iterating pattern, the second hole is finally filled with the
+placeholder being the nesting point. In the innermost occurrence of the
+nested iterating pattern, the second placeholder is finally filled with the
terminating expression.
In the example above, the iterator $\phi([~]_E,[~]_I)$ is {\tt cons
@@ -609,24 +741,26 @@ notations, they can also be declared within interpretation scopes (see
section \ref{scopes}).
\subsection{Notations with recursive patterns involving binders}
+\label{RecursiveNotationsWithBinders}
Recursive notations can also be used with binders. The basic example is:
\begin{coq_example*}
-Notation "'exists' x .. y , p" := (ex (fun x => .. (ex (fun y => p)) ..))
+Notation "'exists' x .. y , p" :=
+ (ex (fun x => .. (ex (fun y => p)) ..))
(at level 200, x binder, y binder, right associativity).
\end{coq_example*}
The principle is the same as in Section~\ref{RecursiveNotations}
-except that in the iterator $\phi([~]_E,[~]_I)$, the first hole is a
-placeholder occurring at the position of the binding variable of a {\tt
+except that in the iterator $\phi([~]_E,[~]_I)$, the placeholder $[~]_E$ can
+also occur in position of the binding variable of a {\tt
fun} or a {\tt forall}.
To specify that the part ``$x$ {\tt ..} $y$'' of the notation
parses a sequence of binders, $x$ and $y$ must be marked as {\tt
- binder} in the list of modifiers of the notation. Then, the list of
-binders produced at the parsing phase are used to fill in the first
-hole of the iterating pattern which is repeatedly nested as many times
+ binder} in the list of modifiers of the notation. The
+binders of the parsed sequence are used to fill the occurrences of the first
+placeholder of the iterating pattern which is repeatedly nested as many times
as the number of binders generated. If ever the generalization
operator {\tt `} (see Section~\ref{implicit-generalization}) is used
in the binding list, the added binders are taken into account too.
@@ -635,14 +769,14 @@ Binders parsing exist in two flavors. If $x$ and $y$ are marked as
{\tt binder}, then a sequence such as {\tt a b c : T} will be accepted
and interpreted as the sequence of binders {\tt (a:T) (b:T)
(c:T)}. For instance, in the notation above, the syntax {\tt exists
- a b : nat, a = b} is provided.
+ a b : nat, a = b} is valid.
The variables $x$ and $y$ can also be marked as {\tt closed binder} in
which case only well-bracketed binders of the form {\tt (a b c:T)} or
{\tt \{a b c:T\}} etc. are accepted.
With closed binders, the recursive sequence in the left-hand side can
-be of the general form $x$ $s$ {\tt ..} $s$ $y$ where $s$ is an
+be of the more general form $x$ $s$ {\tt ..} $s$ $y$ where $s$ is an
arbitrary sequence of tokens. With open binders though, $s$ has to be
empty. Here is an example of recursive notation with closed binders:
@@ -661,6 +795,40 @@ Notation "'FUNAPP' x .. y , f" :=
(at level 200, x binder, y binder, right associativity).
\end{coq_example*}
+If an occurrence of the $[~]_E$ is not in position of a binding
+variable but of a term, it is the name used in the binding which is
+used. Here is an example:
+
+\begin{coq_example*}
+Notation "'exists_non_null' x .. y , P" :=
+ (ex (fun x => x <> 0 /\ .. (ex (fun y => y <> 0 /\ P)) ..))
+ (at level 200, x binder).
+\end{coq_example*}
+
+\subsection{Predefined entries}
+
+By default, sub-expressions are parsed as terms and the corresponding
+grammar entry is called {\tt constr}. However, one may sometimes want
+to restrict the syntax of terms in a notation. For instance, the
+following notation will accept to parse only global reference in
+position of {\tt x}:
+
+\begin{coq_example*}
+Notation "'apply' f a1 .. an" := (.. (f a1) .. an)
+ (at level 10, f global, a1, an at level 9).
+\end{coq_example*}
+
+In addition to {\tt global}, one can restrict the syntax of a
+sub-expression by using the entry names {\tt ident} or {\tt pattern}
+already seen in Section~\ref{NotationsWithBinders}, even when the
+corresponding expression is not used as a binder in the right-hand
+side. E.g.:
+
+\begin{coq_example*}
+Notation "'apply_id' f a1 .. an" := (.. (f a1) .. an)
+ (at level 10, f ident, a1, an at level 9).
+\end{coq_example*}
+
\subsection{Summary}
\paragraph{Syntax of notations}
@@ -754,7 +922,7 @@ stack by using the command
{\tt Close Scope} {\scope}.
\end{quote}
Notice that this command does not only cancel the last {\tt Open Scope
-{\scope}} but all the invocation of it.
+{\scope}} but all the invocations of it.
\Rem {\tt Open Scope} and {\tt Close Scope} do not survive the end of
sections where they occur. When defined outside of a section, they are
@@ -853,6 +1021,14 @@ Arguments scopes can be cleared with the following command:
{\tt Arguments {\qualid} : clear scopes}
\end{quote}
+Extra argument scopes, to be used in case of coercion to Funclass
+(see Chapter~\ref{Coercions-full}) or with a computed type,
+can be given with
+
+\begin{quote}
+{\tt Arguments} {\qualid} \nelist{\textunderscore {\tt \%} \scope}{} {\tt : extra scopes.}
+\end{quote}
+
\begin{Variants}
\item {\tt Global Arguments} {\qualid} \nelist{\name {\tt \%}\scope}{}
@@ -1108,7 +1284,7 @@ Check reflexive iff.
\end{coq_example}
An abbreviation expects no precedence nor associativity, since it
-follows the usual syntax of application. Abbreviations are used as
+is parsed as usual application. Abbreviations are used as
much as possible by the {\Coq} printers unless the modifier
\verb=(only parsing)= is given.
@@ -1121,7 +1297,7 @@ abbreviation but at the time it is used. Especially, abbreviations can
be bound to terms with holes (i.e. with ``\_''). The general syntax
for abbreviations is
\begin{quote}
-\zeroone{{\tt Local}} \texttt{Notation} {\ident} \sequence{\ident} {\ident} \texttt{:=} {\term}
+\zeroone{{\tt Local}} \texttt{Notation} {\ident} \sequence{\ident}{} \texttt{:=} {\term}
\zeroone{{\tt (only parsing)}}~\verb=.=
\end{quote}
@@ -1147,13 +1323,15 @@ at the time of use of the abbreviation.
%\verb=(only parsing)= is given) while syntactic definitions were not.
\section{Tactic Notations
+\label{Tactic-Notation}
\comindex{Tactic Notation}}
Tactic notations allow to customize the syntax of the tactics of the
-tactic language\footnote{Tactic notations are just a simplification of
-the {\tt Grammar tactic simple\_tactic} command that existed in
-versions prior to version 8.0.}. Tactic notations obey the following
-syntax
+tactic language.
+%% \footnote{Tactic notations are just a simplification of
+%% the {\tt Grammar tactic simple\_tactic} command that existed in
+%% versions prior to version 8.0.}
+Tactic notations obey the following syntax:
\medskip
\noindent
@@ -1196,7 +1374,9 @@ level indicates the parsing precedence of the tactic notation. This
information is particularly relevant for notations of tacticals.
Levels 0 to 5 are available (default is 0).
To know the parsing precedences of the
-existing tacticals, use the command {\tt Print Grammar tactic.}
+existing tacticals, use the command
+\comindex{Print Grammar tactic}
+ {\tt Print Grammar tactic.}
Each type of tactic argument has a specific semantic regarding how it
is parsed and how it is interpreted. The semantic is described in the
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 66a5f107a5..40ba43b6cd 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -2904,7 +2904,7 @@ This happens if \term$_1$ does not occur in the goal.
rewrite H in H2 at - 2}. In particular a failure will happen if any of
these three simpler tactics fails.
\item \texttt{rewrite H in * |- } will do \texttt{rewrite H in
- H$_i$} for all hypothesis \texttt{H$_i$ <> H}. A success will happen
+ H$_i$} for all hypotheses \texttt{H$_i$} different from \texttt{H}. A success will happen
as soon as at least one of these simpler tactics succeeds.
\item \texttt{rewrite H in *} is a combination of \texttt{rewrite H}
and \texttt{rewrite H in * |-} that succeeds if at
@@ -3611,7 +3611,7 @@ $\beta$-expansion (the inverse of $\bt$-reduction) of the current goal
\item applying the abstracted goal to {\term}
\end{enumerate}
-For instance, if the current goal $T$ is expressible has $\phi(t)$
+For instance, if the current goal $T$ is expressible as $\phi(t)$
where the notation captures all the instances of $t$ in $\phi(t)$,
then {\tt pattern $t$} transforms it into {\tt (fun x:$A$ => $\phi(${\tt
x}$)$) $t$}. This command can be used, for instance, when the tactic
@@ -4589,7 +4589,6 @@ incompatibilities.
\end{Variants}
\optindex{Intuition Negation Unfolding}
-\optindex{Intuition Iff Unfolding}
Some aspects of the tactic {\tt intuition} can be
controlled using options. To avoid that inner negations which do not
@@ -4609,17 +4608,6 @@ To do that all negations of the goal are unfolded even inner ones
To avoid that inner occurrence of {\tt iff} which do not need to be
unfolded are unfolded (this is the default), use:
-\begin{quote}
-{\tt Unset Intuition Iff Unfolding}
-\end{quote}
-
-To do that all negations of the goal are unfolded even inner ones
-(this is the default), use:
-
-\begin{quote}
-{\tt Set Intuition Iff Unfolding}
-\end{quote}
-
% En attente d'un moyen de valoriser les fichiers de demos
%\SeeAlso file \texttt{contrib/Rocq/DEMOS/Demo\_tauto.v}
diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template
index 48048b7a0f..a2739e457e 100644
--- a/doc/stdlib/index-list.html.template
+++ b/doc/stdlib/index-list.html.template
@@ -18,6 +18,7 @@ through the <tt>Require Import</tt> command.</p>
theories/Init/Logic.v
theories/Init/Logic_Type.v
theories/Init/Nat.v
+ theories/Init/Decimal.v
theories/Init/Peano.v
theories/Init/Specif.v
theories/Init/Tactics.v
@@ -225,6 +226,12 @@ through the <tt>Require Import</tt> command.</p>
theories/Numbers/BinNums.v
theories/Numbers/NumPrelude.v
theories/Numbers/NaryFunctions.v
+ theories/Numbers/DecimalFacts.v
+ theories/Numbers/DecimalNat.v
+ theories/Numbers/DecimalPos.v
+ theories/Numbers/DecimalN.v
+ theories/Numbers/DecimalZ.v
+ theories/Numbers/DecimalString.v
</dd>
<dt> <b>&nbsp;&nbsp;NatInt</b>:
@@ -589,7 +596,6 @@ through the <tt>Require Import</tt> command.</p>
</dt>
<dd>
theories/Compat/AdmitAxiom.v
- theories/Compat/Coq85.v
theories/Compat/Coq86.v
theories/Compat/Coq87.v
</dd>
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-05 00:55:21 +0000