Merge PR #6991: Sphinx doc chapter 12

5 files changed, 1325 insertions, 1433 deletions

diff --git a/Makefile.doc b/Makefile.doc
index 3ffea06e1..64b43f5ea 100644
--- a/Makefile.doc
+++ b/Makefile.doc
@@ -59,7 +59,6 @@ DOCCOMMON:=doc/common/version.tex doc/common/title.tex doc/common/macros.tex
 REFMANCOQTEXFILES:=$(addprefix doc/refman/, \
   RefMan-gal.v.tex \
   RefMan-lib.v.tex \
-  RefMan-syn.v.tex \
   RefMan-oth.v.tex RefMan-ltac.v.tex \
   RefMan-pro.v.tex RefMan-sch.v.tex \
   Cases.v.tex Coercion.v.tex CanonicalStructures.v.tex Extraction.v.tex \
diff --git a/doc/refman/RefMan-syn.tex b/doc/refman/RefMan-syn.tex
deleted file mode 100644
index 836753db1..000000000
--- a/doc/refman/RefMan-syn.tex
+++ /dev/null
@@ -1,1431 +0,0 @@
-\chapter[Syntax extensions and interpretation scopes]{Syntax extensions and interpretation scopes\label{Addoc-syntax}}
-%HEVEA\cutname{syntax-extensions.html}
-
-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 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 expression denoting some term
-or term pattern.
-
-A typical notation is the use of the infix symbol \verb=/\= to denote
-the logical conjunction (\texttt{and}). Such a notation is declared
-by
-
-\begin{coq_example*}
-Notation "A /\ B" := (and A B).
-\end{coq_example*}
-
-The expression \texttt{(and A B)} is the abbreviated term and the
-string \verb="A /\ B"= (called a {\em notation}) tells how it is 
-symbolically written.
-
-A notation is always surrounded by double quotes (except when 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
-denoted term. The other elements of the string (such as \verb=/\=) are
-the {\em symbols}.
-
-An identifier can be used as a symbol but it must be surrounded by
-simple quotes to avoid the confusion with a parameter. Similarly,
-every symbol of at least 3 characters and starting with a simple quote
-must be quoted (then it starts by two single quotes). Here is an example.
-
-\begin{coq_example*}
-Notation "'IF' c1 'then' c2 'else' c3" := (IF_then_else c1 c2 c3).
-\end{coq_example*}
-
-%TODO quote the identifier when not in front, not a keyword, as in "x 'U' y" ?
-
-A notation binds a syntactic expression to a term. Unless the parser
-and pretty-printer of {\Coq} already know how to deal with the
-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, 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.
-
-\subsection[Precedences and associativity]{Precedences and associativity\index{Precedences}
-\index{Associativity}}
-
-Mixing different symbolic notations in the same text may cause serious
-parsing ambiguity. To deal with the ambiguity of notations, {\Coq}
-uses precedence levels ranging from 0 to 100 (plus one extra level
-numbered 200) and associativity rules.
-
-Consider for example the new notation
-
-\begin{coq_example*}
-Notation "A \/ B" := (or A B).
-\end{coq_example*}
-
-Clearly, an expression such as {\tt forall A:Prop, True \verb=/\= A \verb=\/=
-A \verb=\/= False} is ambiguous. To tell the {\Coq} parser how to
-interpret the expression, a priority between the symbols \verb=/\= and
-\verb=\/= has to be given. Assume for instance that we want conjunction
-to bind more than disjunction. This is expressed by assigning a
-precedence level to each notation, knowing that a lower level binds
-more than a higher level.  Hence the level for disjunction must be
-higher than the level for conjunction.
-
-Since connectives are not tight articulation points of a text, it
-is reasonable to choose levels not so far from the highest level which
-is 100, for example 85 for disjunction and 80 for
-conjunction\footnote{which are the levels effectively chosen in the
-current implementation of {\Coq}}.
-
-Similarly, an associativity is needed to decide whether {\tt True \verb=/\=
-False \verb=/\= False} defaults to {\tt True \verb=/\= (False
-\verb=/\= False)} (right associativity) or to {\tt (True
-\verb=/\= False) \verb=/\= False} (left associativity). We may
-even consider that the expression is not well-formed and that
-parentheses are mandatory (this is a ``no associativity'')\footnote{
-{\Coq} accepts notations declared as no associative but the parser on
-which {\Coq} is built, namely {\camlpppp}, currently does not implement the
-no-associativity and replaces it by a left associativity; hence it is
-the same for {\Coq}: no-associativity is in fact left associativity}.
-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
-given between parentheses in a list of modifiers that the
-\texttt{Notation} command understands. Here is how the previous
-examples refine.
-
-\begin{coq_example*}
-Notation "A /\ B" := (and A B) (at level 80, right associativity).
-Notation "A \/ B" := (or A B)  (at level 85, right associativity).
-\end{coq_example*}
-
-By default, a notation is considered non associative, but the
-precedence level is mandatory (except for special cases whose level is
-canonical). The level is either a number or the phrase {\tt next
-level} whose meaning is obvious. The list of levels already assigned
-is on Figure~\ref{init-notations}.
-
-\subsection{Complex notations}
-
-Notations can be made from arbitrarily complex symbols. One can for
-instance define prefix notations.
-
-\begin{coq_example*}
-Notation "~ x" := (not x) (at level 75, right associativity).
-\end{coq_example*}
-
-One can also define notations for incomplete terms, with the hole
-expected to be inferred at typing time.
-
-\begin{coq_example*}
-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, and the default level for the notation itself is 0.
-
-\begin{coq_eval}
-Set Printing Depth 50.
-(********** The following is correct but produces **********)
-(**** an incompatibility with the reserved notation ********)
-\end{coq_eval}
-\begin{coq_example*}
-Notation "( x , y )" := (@pair _ _ x y).
-\end{coq_example*}
-
-One can also define notations for binders.
-
-\begin{coq_eval}
-Set Printing Depth 50.
-(********** The following is correct but produces **********)
-(**** an incompatibility with the reserved notation ********)
-\end{coq_eval}
-\begin{coq_example*}
-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. 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 the following.
-
-\begin{coq_example*}
-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
-%{\tt "{ A } + { B }"}. For the sake of factorization, {\tt A} must be
-%put at level 99 too, which gives
-%
-%\begin{coq_example*}
-%Notation "{ A } + { B }" := (sumbool A B) (at level 0, A at level 99).
-%\end{coq_example*}
-
-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 {\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 **********)
-(*** Error: Notation _ < _ < _ is already defined at level 70 ... ***)
-\end{coq_eval}
-\begin{coq_example*}
-Notation "x < y"     := (lt x y) (at level 70).
-Notation "x < y < z" := (x < y /\ y < z) (at level 70).
-\end{coq_example*}
-
-In order to factorize the left part of the rules, the subexpression
-referred by {\tt y} has to be at the same level in both rules. However
-the default behavior puts {\tt y} at the next level below 70
-in the first rule (no associativity is the default), and at the level
-200 in the second rule (level 200 is the default for inner expressions).
-To fix this, we need to force the parsing level of {\tt y},
-as follows.
-
-\begin{coq_example*}
-Notation "x < y"     := (lt x y) (at level 70).
-Notation "x < y < z" := (x < y /\ y < z) (at level 70, y at next level).
-\end{coq_example*}
-
-For the sake of factorization with {\Coq} predefined rules, simple
-rules have to be observed for notations starting with a symbol:
-e.g. rules starting with ``\{'' or ``('' should be put at level 0. The
-list of {\Coq} predefined notations can be found in Chapter~\ref{Theories}.
-
-The command to display the current state of the {\Coq} term parser is
-\comindex{Print Grammar constr}
-
-\begin{quote}
-\tt Print Grammar constr.
-\end{quote}
-
-\variant
-
-\comindex{Print Grammar pattern}
-{\tt Print Grammar pattern.}\\
-
-This displays the state of the subparser of patterns (the parser
-used in the grammar of the {\tt match} {\tt with} constructions).
-
-\subsection{Displaying symbolic notations}
-
-The command \texttt{Notation} has an effect both on the {\Coq} parser and
-on the {\Coq} printer. For example:
-
-\begin{coq_example}
-Check (and True True).
-\end{coq_example}
-
-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 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
-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
-to separate the components) is interpreted as a space to be inserted
-by the printer. Here is an example showing how to add spaces around
-the bar of the notation.
-
-\begin{coq_example}
-Notation "{{ x : A  |  P }}" := (sig (fun x : A => P))
-  (at level 0, x at level 99).
-Check (sig (fun x : nat => x=x)).
-\end{coq_example}
-
-The second, more powerful control on printing is by using the {\tt
-format} modifier. Here is an example
-
-\begin{small}
-\begin{coq_example}
-Notation "'If' c1 'then' c2 'else' c3" := (IF_then_else c1 c2 c3)
-(at level 200, right associativity, format
-"'[v   ' 'If'  c1 '/' '[' 'then'  c2  ']' '/' '[' 'else'  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:
-
-\begin{itemize}
-\item extra spaces are translated into simple spaces
-\item tokens of the form \verb='/  '= are translated into breaking point,
-  in case a line break occurs, an indentation of the number of spaces
-  after the ``\verb=/='' is applied (2 spaces in the given example)
-\item token of the form \verb='//'= force writing on a new line
-\item well-bracketed pairs of tokens of the form \verb='[    '= and \verb=']'=
-  are translated into printing boxes; in case a line break occurs,
-  an extra indentation of the number of spaces given after the ``\verb=[=''
-  is applied (4 spaces in the example)
-\item well-bracketed pairs of tokens of the form \verb='[hv   '= and \verb=']'=
-  are translated into horizontal-orelse-vertical printing boxes; 
-  if the content of the box does not fit on a single line, then every breaking
-  point forces a newline and an extra  indentation of the number of spaces
-  given after the ``\verb=[='' is applied at the beginning of each newline
-  (3 spaces in the example)
-\item well-bracketed pairs of tokens of the form \verb='[v '= and
-  \verb=']'= are translated into vertical printing boxes; every
-  breaking point forces a newline, even if the line is large enough to
-  display the whole content of the box, and an extra indentation of the
-  number of spaces given after the ``\verb=[='' is applied at the beginning
-  of each newline
-\end{itemize}
-
-%Thus, for the previous example, we get
-%\footnote{The ``@'' is here to shunt
-%the notation "'IF' A 'then' B 'else' C" which is defined in {\Coq}
-%initial state}:
-
-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.
-
-\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 {\tt only parsing} is allowed in the list of modifiers of
-\texttt{Notation}.
-
-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.
-
-\subsection{The \texttt{Infix} command
-\comindex{Infix}}
-
-The \texttt{Infix} command is a shortening for declaring notations of
-infix symbols. Its syntax is 
-
-\begin{quote}
-\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" := ({\term} x y)  (} \nelist{\em modifier}{,} {\tt )}.
-\end{quote}
-
-where {\tt x} and {\tt y} are fresh names. Here is an example.
-
-\begin{coq_example*}
-Infix "/\" := and (at level 80, right associativity).
-\end{coq_example*}
-
-\subsection{Reserving notations
-\label{ReservedNotation}
-\comindex{Reserved Notation}}
-
-A given notation may be used in different contexts. {\Coq} expects all
-uses of the notation to be defined at the same precedence and with the
-same associativity. To avoid giving the precedence and associativity
-every time, it is possible to declare a parsing rule in advance
-without giving its interpretation. Here is an example from the initial
-state of {\Coq}.
-
-\begin{coq_example}
-Reserved Notation "x = y" (at level 70, no associativity).
-\end{coq_example}
-
-Reserving a notation is also useful for simultaneously defining an
-inductive type or a recursive constant and a notation for it.
-
-\Rem The notations mentioned on Figure~\ref{init-notations} are
-reserved. Hence their precedence and associativity cannot be changed.
-
-\subsection{Simultaneous definition of terms and notations
-\comindex{Fixpoint {\ldots} where {\ldots}}
-\comindex{CoFixpoint {\ldots} where {\ldots}}
-\comindex{Inductive {\ldots} where {\ldots}}}
-
-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.
-(********** The following is correct but produces an error **********)
-(********** because the symbol /\ is already bound **********)
-(**** Error: The conclusion of A -> B -> A /\ B is not valid *****)
-\end{coq_eval}
-
-\begin{coq_example*}
-Inductive and (A B:Prop) : Prop := conj : A -> B -> A /\ B 
-where "A /\ B" := (and A B).
-\end{coq_example*}
-
-\begin{coq_eval}
-Set Printing Depth 50.
-(********** The following is correct but produces an error **********)
-(********** because the symbol + is already bound **********)
-(**** Error: no recursive definition *****)
-\end{coq_eval}
-
-\begin{coq_example*}
-Fixpoint plus (n m:nat) {struct n} : nat :=
-  match n with
-  | O => m
-  | S p => S (p+m)
-  end
-where "n + m" := (plus n m).
-\end{coq_example*}
-
-\subsection{Displaying informations about notations
-\optindex{Printing Notations}}
-
-To deactivate the printing of all notations, use the command
-\begin{quote}
-\tt Unset Printing Notations.
-\end{quote}
-To reactivate it, use the command
-\begin{quote}
-\tt Set Printing Notations.
-\end{quote}
-The default is to use notations for printing terms wherever possible.
-
-\SeeAlso {\tt Set Printing All} in Section~\ref{SetPrintingAll}.
-
-\subsection{Locating notations
-\comindex{Locate}
-\label{LocateSymbol}}
-
-To know to which notations a given symbol belongs to, use the command
-\begin{quote}
-\tt Locate {\symbolentry}
-\end{quote}
-where symbol is any (composite) symbol surrounded by double quotes. To locate
-a particular notation, use a string where the variables of the
-notation are replaced by ``\_'' and where possible single quotes
-inserted around identifiers or tokens starting with a single quote are
-dropped.
-
-\Example
-\begin{coq_example}
-Locate "exists".
-Locate "exists _ .. _ , _".
-\end{coq_example}
-
-\SeeAlso Section \ref{Locate}.
-
-\begin{figure}
-\begin{small}
-\begin{centerframe}
-\begin{tabular}{lcl}
-{\sentence} & ::= & 
-   \zeroone{\tt Local} \texttt{Notation} {\str} \texttt{:=} {\term} 
-   \zeroone{\modifiers} \zeroone{:{\scope}} .\\
-  & $|$ & 
-   \zeroone{\tt Local} \texttt{Infix} {\str} \texttt{:=} {\qualid} 
-   \zeroone{\modifiers} \zeroone{:{\scope}} .\\
-  & $|$ & 
-   \zeroone{\tt Local} \texttt{Reserved Notation} {\str}
-   \zeroone{\modifiers} .\\
-  & $|$ & {\tt Inductive}
-   \nelist{{\inductivebody} \zeroone{\declnotation}}{with}{\tt .}\\
-  & $|$ & {\tt CoInductive}
-   \nelist{{\inductivebody} \zeroone{\declnotation}}{with}{\tt .}\\
-  & $|$ & {\tt Fixpoint}
-   \nelist{{\fixpointbody} \zeroone{\declnotation}}{with} {\tt .} \\
-  & $|$ & {\tt CoFixpoint}
-   \nelist{{\cofixpointbody} \zeroone{\declnotation}}{with} {\tt .} \\
-\\
-{\declnotation} & ::= & 
-  \zeroone{{\tt where} \nelist{{\str} {\tt :=} {\term} \zeroone{:{\scope}}}{\tt and}}.
-\\
-\\
-{\modifiers}
-  & ::= & {\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 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} \\
-\\
-\\
-{\binderinterp}
-  & ::= & {\tt as ident} \\
-  & $|$ & {\tt as pattern} \\
-  & $|$ & {\tt as strict pattern} \\
-\end{tabular}
-\end{centerframe}
-\end{small}
-\caption{Syntax of the variants of {\tt Notation}}
-\label{notation-syntax}
-\end{figure}
-
-\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}
-
-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.
-(********** The following is correct but produces **********)
-(**** an incompatibility with the reserved notation ********)
-\end{coq_eval}
-\begin{coq_example*}
-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*}
-
-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}
-
-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).
-\end{coq_example*}
-the next command fails because {\tt p} does not bind in 
-the instance of {\tt n}.
-\begin{coq_eval}
-Set Printing Depth 50.
-\end{coq_eval}
-% (********** The following produces **********)
-% (**** The reference p was not found in the current environment ********)
-\begin{coq_example}
-Fail Check (exists_different p).
-\end{coq_example}
-
-\subsection{Notations with recursive patterns}
-\label{RecursiveNotations}
-
-A mechanism is provided for declaring elementary notations with
-recursive patterns. The basic example is:
-
-\begin{coq_example*}
-Notation "[ x ; .. ; y ]" := (cons x .. (cons y nil) ..).
-\end{coq_example*}
-
-On the right-hand side, an extra construction of the form {\tt ..} $t$
-{\tt ..} can be used. Notice that {\tt ..} is part of the {\Coq}
-syntax and it must not be confused with the three-dots notation
-$\ldots$ used in this manual to denote a sequence of arbitrary size.
-
-On the left-hand side, the part ``$x$ $s$ {\tt ..} $s$ $y$'' of the
-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 ;}'').
-
-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
-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
-  $[~]_E$ $[~]_I$} and the terminating expression is {\tt nil}. Here are
-other examples:
-\begin{coq_example*}
-Notation "( x , y , .. , z )" := (pair .. (pair x y) .. z) (at level 0).
-Notation "[| t * ( x , y , .. , z ) ; ( a , b , .. , c )  * u |]" :=
-  (pair (pair .. (pair (pair t x) (pair t y)) .. (pair t z))
-        (pair .. (pair (pair a u) (pair b u)) .. (pair 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}).
-
-\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)) ..))
-  (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 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. 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.
-
-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 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 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:
-
-\begin{coq_example*}
-Notation "'mylet' f x .. y :=  t 'in' u":=
-  (let f := fun x => .. (fun y => t) .. in u)
-  (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*}
-
-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}
-
-The different syntactic variants of the command \texttt{Notation} are
-given on Figure~\ref{notation-syntax}. The optional {\tt :{\scope}} is
-described in the Section~\ref{scopes}.
-
-\Rem No typing of the denoted expression is performed at definition
-time. Type-checking is done only at the time of use of the notation.
-
-\Rem Many examples of {\tt Notation} may be found in the files
-composing the initial state of {\Coq} (see directory {\tt
-\$COQLIB/theories/Init}).
-
-\Rem The notation \verb="{ x }"= has a special status in such a way
-that complex notations of the form \verb="x + { y }"= or
-\verb="x * { y }"= can be nested with correct precedences. Especially,
-every notation involving a pattern of the form \verb="{ x }"= is
-parsed as a notation where the pattern \verb="{ x }"= has been simply
-replaced by \verb="x"= and the curly brackets are parsed separately.
-E.g. \verb="y + { z }"= is not parsed as a term of the given form but
-as a term of the form \verb="y + z"= where \verb=z= has been parsed
-using the rule parsing \verb="{ x }"=. Especially, level and
-precedences for a rule including patterns of the form \verb="{ x }"=
-are relative not to the textual notation but to the notation where the
-curly brackets have been removed (e.g. the level and the associativity
-given to some notation, say \verb="{ y } & { z }"= in fact applies to
-the underlying \verb="{ x }"=-free rule which is \verb="y & z"=).
-
-\paragraph{Persistence of notations}
-
-Notations do not survive the end of sections. They survive modules
-unless the command {\tt Local Notation} is used instead of {\tt
-Notation}.
-
-\section[Interpretation scopes]{Interpretation scopes\index{Interpretation scopes}
-\label{scopes}}
-% Introduction
-
-An {\em interpretation scope} is a set of notations for terms with
-their interpretation. Interpretation scopes provide a weak,
-purely syntactical form of notation overloading: the same notation, for
-instance the infix symbol \verb=+=, can be used to denote distinct
-definitions of the additive operator. Depending on which interpretation
-scope is currently open, the interpretation is different.
-Interpretation scopes can include an interpretation for
-numerals and strings. However, this is only made possible at the
-{\ocaml} level.
-
-See Figure \ref{notation-syntax} for the syntax of notations including
-the possibility to declare them in a given scope.  Here is a typical
-example which declares the notation for conjunction in the scope {\tt
-type\_scope}.
-
-\begin{verbatim}
-Notation "A /\ B" := (and A B) : type_scope.
-\end{verbatim}
-
-\Rem A notation not defined in a scope is called a {\em lonely} notation.
-
-\subsection{Global interpretation rules for notations}
-
-At any time, the interpretation of a notation for term is done within
-a {\em stack} of interpretation scopes and lonely notations. In case a
-notation has several interpretations, the actual interpretation is the
-one defined by (or in) the more recently declared (or open) lonely
-notation (or interpretation scope) which defines this notation.
-Typically if a given notation is defined in some scope {\scope} but
-has also an interpretation not assigned to a scope, then, if {\scope}
-is open before the lonely interpretation is declared, then the lonely
-interpretation is used (and this is the case even if the
-interpretation of the notation in {\scope} is given after the lonely
-interpretation: otherwise said, only the order of lonely
-interpretations and opening of scopes matters, and not the declaration
-of interpretations within a scope).
-
-The initial state of {\Coq} declares three interpretation scopes and
-no lonely notations. These scopes, in opening order, are {\tt
-core\_scope}, {\tt type\_scope} and {\tt nat\_scope}.
-
-The command to add a scope to the interpretation scope stack is
-\comindex{Open Scope}
-\comindex{Close Scope}
-\begin{quote}
-{\tt Open Scope} {\scope}.
-\end{quote}
-It is also possible to remove a scope from the interpretation scope
-stack by using the command
-\begin{quote}
-{\tt Close Scope} {\scope}.
-\end{quote}
-Notice that this command does not only cancel the last {\tt Open Scope
-{\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
-exported to the modules that import the module where they occur.
-
-\begin{Variants}
-
-\item {\tt Local Open Scope} {\scope}.
-
-\item {\tt Local Close Scope} {\scope}.
-
-These variants are not exported to the modules that import the module
-where they occur, even if outside a section.
-
-\item {\tt Global Open Scope} {\scope}.
-
-\item {\tt Global Close Scope} {\scope}.
-
-These variants survive sections. They behave as if {\tt Global} were
-absent when not inside a section.
-
-\end{Variants}
-
-\subsection{Local interpretation rules for notations}
-
-In addition to the global rules of interpretation of notations, some
-ways to change the interpretation of subterms are available.
-
-\subsubsection{Local opening of an interpretation scope 
-\label{scopechange}
-\index{\%}
-\comindex{Delimit Scope}
-\comindex{Undelimit Scope}}
-
-It is possible to locally extend the interpretation scope stack using
-the syntax ({\term})\%{\delimkey} (or simply {\term}\%{\delimkey}
-for atomic terms), where {\delimkey} is a special identifier called
-{\em delimiting key} and bound to a given scope.
-
-In such a situation, the term {\term}, and all its subterms, are
-interpreted in the scope stack extended with the scope bound to
-{\delimkey}.
-
-To bind a delimiting key to a scope, use the command
-
-\begin{quote}
-\texttt{Delimit Scope} {\scope} \texttt{with} {\ident} 
-\end{quote}
-
-To remove a delimiting key of a scope, use the command
-
-\begin{quote}
-\texttt{Undelimit Scope} {\scope}
-\end{quote}
-
-\subsubsection{Binding arguments of a constant to an interpretation scope
-\comindex{Arguments}}
-
-It is possible to set in advance that some arguments of a given
-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 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.
-\end{coq_example*}
-
-The {\tt Arguments} command accepts scopes decoration to all grouping
-parentheses. In the following example arguments {\tt A} and {\tt B} 
-are marked as maximally inserted implicit arguments and are
-put into the {\tt type\_scope} scope.
-
-\begin{coq_example*}
-Arguments respectful {A B}%type (R R')%signature _ _.
-\end{coq_example*}
-
-When interpreting a term, if some of the arguments of {\qualid} are
-built from a notation, then this notation is interpreted in the scope
-stack extended by the scope bound (if any) to this argument. The
-effect of the scope is limited to the argument itself. It does not propagate 
-to subterms but the subterms that, after interpretation of the
-notation, turn to be themselves arguments of a reference are
-interpreted accordingly to the arguments scopes bound to this reference.
-
-Arguments scopes can be cleared with the following command:
-
-\begin{quote}
-{\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}{}
-
-This behaves like {\tt Arguments} {\qualid} \nelist{\name {\tt \%}\scope}{}
-but survives when a section is closed instead
-of stopping working at section closing. Without the {\tt Global} modifier,
-the effect of the command stops when the section it belongs to ends.
-
-\item {\tt Local Arguments} {\qualid} \nelist{\name {\tt \%}\scope}{}
-
-This behaves like {\tt Arguments} {\qualid} \nelist{\name {\tt \%}\scope}{}
-but does not survive modules and files.
-Without the {\tt Local} modifier, the effect of the command is
-visible from within other modules or files.
-
-\end{Variants}
-
-\SeeAlso The command to show the scopes bound to the arguments of a
-function is described in Section~\ref{About}.
-
-\subsubsection{Binding types of arguments to an interpretation scope}
-
-When an interpretation scope is naturally associated to a type
-(e.g. the scope of operations on the natural numbers), it may be
-convenient to bind it to this type. When a scope {\scope} is bound to
-a type {\type}, any new function defined later on gets its arguments
-of type {\type} interpreted by default in scope {\scope} (this default
-behavior can however be overwritten by explicitly using the command
-{\tt Arguments}).
-
-Whether the argument of a function has some type {\type} is determined
-statically. For instance, if {\tt f} is a polymorphic function of type
-{\tt forall X:Type, X -> X} and type {\tt t} is bound to a scope
-{\scope}, then {\tt a} of type {\tt t} in {\tt f~t~a} is not
-recognized as an argument to be interpreted in scope {\scope}.
-
-\comindex{Bind Scope}
-\label{bindscope}
-More generally, any coercion {\class} (see Chapter~\ref{Coercions-full}) can be
-bound to an interpretation scope. The command to do it is
-\begin{quote}
-{\tt Bind Scope} {\scope} \texttt{with} {\class}
-\end{quote}
-
-\Example
-\begin{coq_example}
-Parameter U : Set.
-Bind Scope U_scope with U.
-Parameter Uplus : U -> U -> U.
-Parameter P : forall T:Set, T -> U -> Prop.
-Parameter f : forall T:Set, T -> U.
-Infix "+" := Uplus : U_scope.
-Unset Printing Notations.
-Open Scope nat_scope. (* Define + on the nat as the default for + *)
-Check (fun x y1 y2 z t => P _ (x + t) ((f _ (y1 + y2) + z))).
-\end{coq_example}
-
-\Rem The scopes {\tt type\_scope} and {\tt function\_scope} also have a local effect on
-interpretation. See the next section.
-
-\SeeAlso The command to show the scopes bound to the arguments of a
-function is described in Section~\ref{About}.
-
-\Rem In notations, the subterms matching the identifiers of the
-notations are interpreted in the scope in which the identifiers
-occurred at the time of the declaration of the notation. Here is an
-example:
-
-\begin{coq_example}
-Parameter g : bool -> bool.
-Notation "@@" := true (only parsing) : bool_scope.
-Notation "@@" := false (only parsing): mybool_scope.
-
-(* Defining a notation while the argument of g is bound to bool_scope *)
-Bind Scope bool_scope with bool.
-Notation "# x #" := (g x) (at level 40).
-Check # @@ #.
-(* Rebinding the argument of g to mybool_scope has no effect on the notation *)
-Arguments g _%mybool_scope.
-Check # @@ #.
-(* But we can force the scope *)
-Delimit Scope mybool_scope with mybool.
-Check # @@%mybool #.
-\end{coq_example}
-
-\subsection[The {\tt type\_scope} interpretation scope]{The {\tt type\_scope} interpretation scope\index{type\_scope@\texttt{type\_scope}}}
-
-The scope {\tt type\_scope} has a special status. It is a primitive
-interpretation scope which is temporarily activated each time a
-subterm of an expression is expected to be a type.  It is delimited by
-the key {\tt type}, and bound to the coercion class {\tt Sortclass}. It is also
-used in certain situations where an expression is statically known to
-be a type, including the conclusion and the type of hypotheses within
-an {\tt Ltac} goal match (see Section~\ref{ltac-match-goal})
-the statement of a theorem, the type of
-a definition, the type of a binder, the domain and codomain of
-implication, the codomain of products, and more generally any type
-argument of a declared or defined constant.
-
-\subsection[The {\tt function\_scope} interpretation scope]{The {\tt function\_scope} interpretation scope\index{function\_scope@\texttt{function\_scope}}}
-
-The scope {\tt function\_scope} also has a special status. 
-It is temporarily activated each time the argument of a global reference is
-recognized to be a {\tt Funclass instance}, i.e., of type {\tt forall x:A, B} or {\tt A -> B}.
-
-\subsection{Interpretation scopes used in the standard library of {\Coq}}
-
-We give an overview of the scopes used in the standard library of
-{\Coq}. For a complete list of notations in each scope, use the
-commands {\tt Print Scopes} or {\tt Print Scope {\scope}}.
-
-\subsubsection{\tt type\_scope}
-
-This scope includes infix {\tt *} for product types and infix {\tt +} for
-sum types. It is delimited by key {\tt type}, and bound to the coercion class 
-{\tt Sortclass}, as described at \ref{bindscope}.
-
-\subsubsection{\tt nat\_scope}
-
-This scope includes the standard arithmetical operators and relations on
-type {\tt nat}. Positive numerals in this scope are mapped to their
-canonical representent built from {\tt O} and {\tt S}. The scope is
-delimited by key {\tt nat}, and bound to the type {\tt nat} (see \ref{bindscope}).
-
-\subsubsection{\tt N\_scope}
-
-This scope includes the standard arithmetical operators and relations on
-type {\tt N} (binary natural numbers). It is delimited by key {\tt N}
-and comes with an interpretation for numerals as closed term of type {\tt N}.
-
-\subsubsection{\tt Z\_scope}
-
-This scope includes the standard arithmetical operators and relations on
-type {\tt Z} (binary integer numbers). It is delimited by key {\tt Z} 
-and comes with an interpretation for numerals as closed term of type {\tt Z}.
-
-\subsubsection{\tt positive\_scope}
-
-This scope includes the standard arithmetical operators and relations on
-type {\tt positive} (binary strictly positive numbers). It is
-delimited by key {\tt positive} and comes with an interpretation for
-numerals as closed term of type {\tt positive}.
-
-\subsubsection{\tt Q\_scope}
-
-This scope includes the standard arithmetical operators and relations on
-type {\tt Q} (rational numbers defined as fractions of an integer and
-a strictly positive integer modulo the equality of the
-numerator-denominator cross-product). As for numerals, only $0$ and
-$1$ have an interpretation in scope {\tt Q\_scope} (their
-interpretations are $\frac{0}{1}$ and $\frac{1}{1}$ respectively).
-
-\subsubsection{\tt Qc\_scope}
-
-This scope includes the standard arithmetical operators and relations on the
-type {\tt Qc} of rational numbers defined as the type of irreducible
-fractions of an integer and a strictly positive integer.
-
-\subsubsection{\tt real\_scope}
-
-This scope includes the standard arithmetical operators and relations on
-type {\tt R} (axiomatic real numbers). It is delimited by key {\tt R}
-and comes with an interpretation for numerals using the {\tt IZR}
-morphism from binary integer numbers to {\tt R}.
-
-\subsubsection{\tt bool\_scope}
-
-This scope includes notations for the boolean operators. It is
-delimited by key {\tt bool}, and bound to the type {\tt bool} (see \ref{bindscope}).
-
-\subsubsection{\tt list\_scope}
-
-This scope includes notations for the list operators. It is
-delimited by key {\tt list}, and bound to the type {\tt list} (see \ref{bindscope}).
-
-\subsubsection{\tt function\_scope}
-
-This scope is delimited by the key {\tt function}, and bound to the coercion class {\tt Funclass}, 
-as described at \ref{bindscope}.
-
-\subsubsection{\tt core\_scope}
-
-This scope includes the notation for pairs. It is delimited by key {\tt core}.
-
-\subsubsection{\tt string\_scope}
-
-This scope includes notation for strings as elements of the type {\tt
-string}.  Special characters and escaping follow {\Coq} conventions
-on strings (see Section~\ref{strings}). Especially, there is no
-convention to visualize non printable characters of a string.  The
-file {\tt String.v} shows an example that contains quotes, a newline
-and a beep (i.e. the ASCII character of code 7).
-
-\subsubsection{\tt char\_scope}
-
-This scope includes interpretation for all strings of the form
-\verb!"!$c$\verb!"! where $c$ is an ASCII character, or of the form
-\verb!"!$nnn$\verb!"! where $nnn$ is a three-digits number (possibly
-with leading 0's), or of the form \verb!""""!. Their respective
-denotations are the ASCII code of $c$, the decimal ASCII code $nnn$,
-or the ASCII code of the character \verb!"! (i.e. the ASCII code
-34), all of them being represented in the type {\tt ascii}.
-
-\subsection{Displaying informations about scopes}
-
-\subsubsection{\tt Print Visibility\comindex{Print Visibility}}
-
-This displays the current stack of notations in scopes and lonely
-notations that is used to interpret a notation. The top of the stack
-is displayed last. Notations in scopes whose interpretation is hidden
-by the same notation in a more recently open scope are not
-displayed. Hence each notation is displayed only once.
-
-\variant
-
-{\tt Print Visibility {\scope}}\\
-
-This displays the current stack of notations in scopes and lonely
-notations assuming that {\scope} is pushed on top of the stack.  This
-is useful to know how a subterm locally occurring in the scope of
-{\scope} is interpreted.
-
-\subsubsection{\tt Print Scope {\scope}\comindex{Print Scope}}
-
-This displays all the notations defined in interpretation scope
-{\scope}.  It also displays the delimiting key if any and the class to
-which the scope is bound, if any.
-
-\subsubsection{\tt Print Scopes\comindex{Print Scopes}}
-
-This displays all the notations, delimiting keys and corresponding
-class of all the existing interpretation scopes.
-It also displays the lonely notations.
-
-\section[Abbreviations]{Abbreviations\index{Abbreviations}
-\label{Abbreviations}
-\comindex{Notation}}
-
-An {\em abbreviation} is a name, possibly applied to arguments, that
-denotes a (presumably) more complex expression. Here are examples:
-
-\begin{coq_eval}
-Require Import List.
-Require Import Relations.
-Set Printing Notations.
-\end{coq_eval}
-\begin{coq_example}
-Notation Nlist := (list nat).
-Check 1 :: 2 :: 3 :: nil.
-Notation reflexive R := (forall x, R x x).
-Check forall A:Prop, A <-> A.
-Check reflexive iff.
-\end{coq_example}
-
-An abbreviation expects no precedence nor associativity, since it
-is parsed as usual application. Abbreviations are used as
-much as possible by the {\Coq} printers unless the modifier
-\verb=(only parsing)= is given.
-
-Abbreviations are bound to an absolute name as an ordinary
-definition is, and they can be referred by qualified names too.
-
-Abbreviations are syntactic in the sense that they are bound to
-expressions which are not typed at the time of the definition of the
-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}{} \texttt{:=} {\term}
- \zeroone{{\tt (only parsing)}}~\verb=.=
-\end{quote}
-
-\Example
-\begin{coq_eval}
-Set Strict Implicit.
-Reset Initial.
-\end{coq_eval}
-\begin{coq_example}
-Definition explicit_id (A:Set) (a:A) := a.
-Notation id := (explicit_id _).
-Check (id 0).
-\end{coq_example}
-
-Abbreviations 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 abbreviation.
-
-%\Rem \index{Syntactic Definition} %
-%Abbreviations are similar to the {\em syntactic
-%definitions} available in versions of {\Coq} prior to version 8.0,
-%except that abbreviations are used for printing (unless the modifier
-%\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:
-\medskip
-
-\noindent
-\begin{tabular}{lcl}
-{\sentence} & ::= & \zeroone{\tt Local} \texttt{Tactic Notation} \zeroone{\taclevel} \sequence{\proditem}{} \\
-& & \texttt{:= {\tac} .}\\
-{\proditem} & ::= & {\str} $|$ {\tacargtype}{\tt ({\ident})} \\ 
-{\taclevel} & ::= & {\tt (at level} {\naturalnumber}{\tt )} \\
-{\tacargtype}\!\! & ::= &
-%{\tt preident} $|$
-{\tt ident} $|$
-{\tt simple\_intropattern} $|$
-{\tt reference} \\ & $|$ &
-{\tt hyp} $|$
-{\tt hyp\_list} $|$
-{\tt ne\_hyp\_list} \\ & $|$ &
-% {\tt quantified\_hypothesis} \\ & $|$ &
-{\tt constr} $|$ {\tt uconstr} $|$
-{\tt constr\_list} $|$
-{\tt ne\_constr\_list} \\ & $|$ &
-%{\tt castedopenconstr} $|$
-{\tt integer} $|$
-{\tt integer\_list} $|$
-{\tt ne\_integer\_list} \\ & $|$ &
-{\tt int\_or\_var} $|$
-{\tt int\_or\_var\_list} $|$
-{\tt ne\_int\_or\_var\_list} \\ & $|$ &
-{\tt tactic} $|$ {\tt tactic$n$} \qquad\mbox{(for $0\leq n\leq 5$)}
-
-\end{tabular}
-\medskip
-
-A tactic notation {\tt Tactic Notation {\taclevel}
-{\sequence{\proditem}{}} := {\tac}} extends the parser and
-pretty-printer of tactics with a new rule made of the list of
-production items. It then evaluates into the tactic expression
-{\tac}. For simple tactics, it is recommended to use a terminal
-symbol, i.e. a {\str}, for the first production item.  The tactic
-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
-\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
-following table. The last command gives examples of tactics which
-use the corresponding kind of argument.
-
-\medskip
-\noindent
-\begin{tabular}{l|l|l|l}
-Tactic argument type & parsed as & interpreted as & as in tactic \\
-\hline & & & \\
-{\tt\small ident} & identifier & a user-given name & {\tt intro} \\
-{\tt\small simple\_intropattern} & intro\_pattern & an intro\_pattern & {\tt intros}\\
-{\tt\small hyp} & identifier & an hypothesis defined in context & {\tt clear}\\
-%% quantified_hypothesis actually not supported
-%%{\tt\small quantified\_hypothesis} & identifier or integer & a named or non dep. hyp. of the goal & {\tt intros until}\\
-{\tt\small reference} & qualified identifier & a global reference of term & {\tt unfold}\\
-{\tt\small constr} & term & a term & {\tt exact} \\
-{\tt\small uconstr} & term & an untyped term & {\tt refine} \\
-%% castedopenconstr actually not supported
-%%{\tt\small castedopenconstr} & term & a term with its sign. of exist. var. & {\tt refine}\\
-{\tt\small integer} & integer & an integer &  \\
-{\tt\small int\_or\_var} & identifier or integer & an integer & {\tt do} \\
-{\tt\small tactic} & tactic at level 5 & a tactic &  \\
-{\tt\small tactic$n$} & tactic at level $n$ & a tactic & \\
-{\tt\small {\nterm{entry}}\_list} & list of {\nterm{entry}} & a list of how {\nterm{entry}} is interpreted & \\
-{\tt\small ne\_{\nterm{entry}}\_list} & non-empty list of {\nterm{entry}} & a list of how {\nterm{entry}} is interpreted& \\
-\end{tabular}
-
-\Rem In order to be bound in tactic definitions, each syntactic entry
-for argument type must include the case of simple {\ltac} identifier
-as part of what it parses. This is naturally the case for {\tt ident},
-{\tt simple\_intropattern}, {\tt reference}, {\tt constr}, ... but not
-for {\tt integer}. This is the reason for introducing a special entry
-{\tt int\_or\_var} which evaluates to integers only but which
-syntactically includes identifiers in order to be usable in tactic
-definitions.
-
-\Rem The {\tt {\nterm{entry}}\_list} and {\tt ne\_{\nterm{entry}}\_list}
-entries can be used in primitive tactics or in other notations at
-places where a list of the underlying entry can be used: {\nterm{entry}} is
-either {\tt\small constr}, {\tt\small hyp}, {\tt\small integer} or
-{\tt\small int\_or\_var}.
-
-Tactic notations do not survive the end of sections. They survive
-modules unless the command {\tt Local Tactic Notation} is used instead
-of {\tt Tactic Notation}.
-
-%%% Local Variables: 
-%%% mode: latex
-%%% TeX-master: "Reference-Manual"
-%%% End: 
diff --git a/doc/refman/Reference-Manual.tex b/doc/refman/Reference-Manual.tex
index e63e6731e..9545a47c9 100644
--- a/doc/refman/Reference-Manual.tex
+++ b/doc/refman/Reference-Manual.tex
@@ -109,7 +109,6 @@ Options A and B of the licence are {\em not} elected.}
 \include{RefMan-ssr}
 
 \part{User extensions}
-\include{RefMan-syn.v}% The Syntax and the Grammar commands
 %%SUPPRIME \include{RefMan-tus.v}% Writing tactics
 \include{RefMan-sch.v}% The Scheme commands
 
diff --git a/doc/sphinx/index.rst b/doc/sphinx/index.rst
index c76d0c73b..f3b852d45 100644
--- a/doc/sphinx/index.rst
+++ b/doc/sphinx/index.rst
@@ -29,6 +29,8 @@ Table of contents
 .. toctree::
    :caption: User extensions
 
+   user-extensions/syntax-extensions
+
 .. toctree::
    :caption: Practical tools
 
diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst
new file mode 100644
index 000000000..6e6d66447
--- /dev/null
+++ b/doc/sphinx/user-extensions/syntax-extensions.rst
@@ -0,0 +1,1323 @@
+.. include:: ../replaces.rst
+
+.. _syntaxextensionsandinterpretationscopes:
+
+Syntax extensions and interpretation scopes
+========================================================
+
+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 to provide custom symbolic notations for terms are
+``Notation`` and ``Infix``. They are described in section 12.1. There is also a
+variant of ``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 ``Tactic Notation``.
+It is described in Section :ref:`TacticNotation`.
+
+.. coqtop:: none
+
+   Set Printing Depth 50.
+
+Notations
+---------
+
+Basic notations
+~~~~~~~~~~~~~~~
+
+A *notation* is a symbolic expression denoting some term or term
+pattern.
+
+A typical notation is the use of the infix symbol ``/\`` to denote the
+logical conjunction (and). Such a notation is declared by
+
+.. coqtop:: in
+
+   Notation "A /\ B" := (and A B).
+
+The expression :g:`(and A B)` is the abbreviated term and the string ``"A /\ B"``
+(called a *notation*) tells how it is symbolically written.
+
+A notation is always surrounded by double quotes (except when the
+abbreviation has the form of an ordinary applicative expression;
+see :ref:`Abbreviations`). The notation is composed of *tokens* separated by
+spaces. Identifiers in the string (such as ``A`` and ``B``) are the *parameters*
+of the notation. They must occur at least once each in the denoted term. The
+other elements of the string (such as ``/\``) are the *symbols*.
+
+An identifier can be used as a symbol but it must be surrounded by
+simple quotes to avoid the confusion with a parameter. Similarly,
+every symbol of at least 3 characters and starting with a simple quote
+must be quoted (then it starts by two single quotes). Here is an
+example.
+
+.. coqtop:: in
+
+   Notation "'IF' c1 'then' c2 'else' c3" := (IF_then_else c1 c2 c3).
+
+A notation binds a syntactic expression to a term. Unless the parser
+and pretty-printer of Coq already know how to deal with the syntactic
+expression (see 12.1.7), explicit precedences and associativity rules
+have to be given.
+
+.. note::
+
+   The right-hand side of a notation is interpreted at the time the notation is
+   given. In particular, disambiguiation of constants, implicit arguments (see
+   Section :ref:`ImplicitArguments`), coercions (see Section :ref:`Coercions`),
+   etc. are resolved at the time of the declaration of the notation.
+
+Precedences and associativity
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+Mixing different symbolic notations in the same text may cause serious
+parsing ambiguity. To deal with the ambiguity of notations, Coq uses
+precedence levels ranging from 0 to 100 (plus one extra level numbered
+200) and associativity rules.
+
+Consider for example the new notation
+
+.. coqtop:: in
+
+   Notation "A \/ B" := (or A B).
+
+Clearly, an expression such as :g:`forall A:Prop, True /\ A \/ A \/ False`
+is ambiguous. To tell the Coq parser how to interpret the
+expression, a priority between the symbols ``/\`` and ``\/`` has to be
+given. Assume for instance that we want conjunction to bind more than
+disjunction. This is expressed by assigning a precedence level to each
+notation, knowing that a lower level binds more than a higher level.
+Hence the level for disjunction must be higher than the level for
+conjunction.
+
+Since connectives are not tight articulation points of a text, it
+is reasonable to choose levels not so far from the highest level which
+is 100, for example 85 for disjunction and 80 for conjunction [#and_or_levels]_.
+
+Similarly, an associativity is needed to decide whether :g:`True /\ False /\ False`
+defaults to :g:`True /\ (False /\ False)` (right associativity) or to
+:g:`(True /\ False) /\ False` (left associativity). We may even consider that the
+expression is not well- formed and that parentheses are mandatory (this is a “no
+associativity”) [#no_associativity]_. 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
+given between parentheses in a list of modifiers that the ``Notation``
+command understands. Here is how the previous examples refine.
+
+.. coqtop:: in
+
+   Notation "A /\ B" := (and A B) (at level 80, right associativity).
+   Notation "A \/ B" := (or A B) (at level 85, right associativity).
+
+By default, a notation is considered non associative, but the
+precedence level is mandatory (except for special cases whose level is
+canonical). The level is either a number or the phrase `next level`
+whose meaning is obvious. The list of levels already assigned is on
+Figure 3.1.
+
+.. TODO I don't find it obvious -- CPC
+
+Complex notations
+~~~~~~~~~~~~~~~~~
+
+Notations can be made from arbitrarily complex symbols. One can for
+instance define prefix notations.
+
+.. coqtop:: in
+
+   Notation "~ x" := (not x) (at level 75, right associativity).
+
+One can also define notations for incomplete terms, with the hole
+expected to be inferred at typing time.
+
+.. coqtop:: in
+
+   Notation "x = y" := (@eq _ x y) (at level 70, no associativity).
+
+One can define *closed* notations whose both sides are symbols. In this case,
+the default precedence level for the inner subexpression is 200, and the default
+level for the notation itself is 0.
+
+.. coqtop:: in
+
+   Notation "( x , y )" := (@pair _ _ x y).
+
+One can also define notations for binders.
+
+.. coqtop:: in
+
+   Notation "{ x : A | P }" := (sig A (fun x => P)).
+
+In the last case though, there is a conflict with the notation for
+type casts. The notation for types casts, as shown by the command :cmd:`Print
+Grammar constr` is at level 100. To avoid ``x : A`` being parsed as a type cast,
+it is necessary to put x at a level below 100, typically 99. Hence, a correct
+definition is the following:
+
+.. coqtop:: all
+
+   Notation "{ x : A | P }" := (sig A (fun x => P)) (x at level 99).
+
+More generally, it is required that notations are explicitly factorized on the
+left. See the next section for more about factorization.
+
+Simple factorization rules
+~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+Coq extensible parsing is performed by *Camlp5* 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.
+
+.. coqtop:: all
+
+   Notation "x < y" := (lt x y) (at level 70).
+   Notation "x < y < z" := (x < y /\ y < z) (at level 70).
+
+In order to factorize the left part of the rules, the subexpression
+referred by y has to be at the same level in both rules. However the
+default behavior puts y at the next level below 70 in the first rule
+(no associativity is the default), and at the level 200 in the second
+rule (level 200 is the default for inner expressions). To fix this, we
+need to force the parsing level of y, as follows.
+
+.. coqtop:: all
+
+   Notation "x < y" := (lt x y) (at level 70).
+   Notation "x < y < z" := (x < y /\ y < z) (at level 70, y at next level).
+
+For the sake of factorization with Coq predefined rules, simple rules
+have to be observed for notations starting with a symbol: e.g. rules
+starting with “{” or “(” should be put at level 0. The list of Coq
+predefined notations can be found in Chapter 3.
+
+.. cmd:: Print Grammar constr.
+
+   This command displays the current state of the Coq term parser.
+
+.. cmd:: Print Grammar pattern.
+
+   This displays the state of the subparser of patterns (the parser used in the
+   grammar of the match with constructions).
+
+
+Displaying symbolic notations
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+The command ``Notation`` has an effect both on the Coq parser and on the
+Coq printer. For example:
+
+.. coqtop:: all
+
+   Check (and True True).
+
+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 *formatting boxes*.
+
+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
+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 to
+separate the components) is interpreted as a space to be inserted by
+the printer. Here is an example showing how to add spaces around the
+bar of the notation.
+
+.. coqtop:: in
+
+   Notation "{{ x : A | P }}" := (sig (fun x : A => P)) (at level 0, x at level 99).
+
+.. coqtop:: all
+
+   Check (sig (fun x : nat => x=x)).
+
+The second, more powerful control on printing is by using the format
+modifier. Here is an example
+
+.. coqtop:: all
+
+   Notation "'If' c1 'then' c2 'else' c3" := (IF_then_else c1 c2 c3)
+   (at level 200, right associativity, format
+   "'[v   ' 'If'  c1 '/' '[' 'then'  c2  ']' '/' '[' 'else'  c3 ']' ']'").
+
+.. coqtop:: all
+
+   Check
+     (IF_then_else (IF_then_else True False True)
+       (IF_then_else True False True)
+       (IF_then_else True False True)).
+
+A *format* is an extension of the string denoting the notation with
+the possible following elements delimited by single quotes:
+
+- extra spaces are translated into simple spaces
+
+- tokens of the form ``'/ '`` are translated into breaking point, in
+  case a line break occurs, an indentation of the number of spaces after
+  the “ ``/``” is applied (2 spaces in the given example)
+
+- token of the form ``'//'`` force writing on a new line
+
+- well-bracketed pairs of tokens of the form ``'[ '`` and ``']'`` are
+  translated into printing boxes; in case a line break occurs, an extra
+  indentation of the number of spaces given after the “ ``[``” is applied
+  (4 spaces in the example)
+
+- well-bracketed pairs of tokens of the form ``'[hv '`` and ``']'`` are
+  translated into horizontal-orelse-vertical printing boxes; if the
+  content of the box does not fit on a single line, then every breaking
+  point forces a newline and an extra indentation of the number of
+  spaces given after the “ ``[``” is applied at the beginning of each
+  newline (3 spaces in the example)
+
+- well-bracketed pairs of tokens of the form ``'[v '`` and ``']'`` are
+  translated into vertical printing boxes; every breaking point forces a
+  newline, even if the line is large enough to display the whole content
+  of the box, and an extra indentation of the number of spaces given
+  after the “``[``” is applied at the beginning of each newline
+
+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.
+
+.. note:: Sometimes, a notation is expected only for the parser. To do
+          so, the option ``only parsing`` is allowed in the list of modifiers
+          of ``Notation``. Conversely, the ``only printing`` modifier 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.
+
+The Infix command
+~~~~~~~~~~~~~~~~~~
+
+The ``Infix`` command is a shortening for declaring notations of infix
+symbols.
+
+.. cmd:: Infix "@symbol" := @term ({+, @modifier}).
+
+   This command is equivalent to
+
+       :n:`Notation "x @symbol y" := (@term x y) ({+, @modifier}).`
+
+   where ``x`` and ``y`` are fresh names. Here is an example.
+
+   .. coqtop:: in
+
+      Infix "/\" := and (at level 80, right associativity).
+
+Reserving notations
+~~~~~~~~~~~~~~~~~~~
+
+A given notation may be used in different contexts. Coq expects all
+uses of the notation to be defined at the same precedence and with the
+same associativity. To avoid giving the precedence and associativity
+every time, it is possible to declare a parsing rule in advance
+without giving its interpretation. Here is an example from the initial
+state of Coq.
+
+.. coqtop:: in
+
+   Reserved Notation "x = y" (at level 70, no associativity).
+
+Reserving a notation is also useful for simultaneously defining an
+inductive type or a recursive constant and a notation for it.
+
+.. note:: The notations mentioned on Figure 3.1 are reserved. Hence
+          their precedence and associativity cannot be changed.
+
+Simultaneous definition of terms and notations
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+Thanks to reserved notations, the inductive, co-inductive, record, recursive
+and corecursive definitions can benefit of customized notations. To do
+this, insert a ``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 12.1 for inductive, co-inductive, recursive and corecursive
+definitions and on Figure :ref:`record-syntax` for records. Here are examples:
+
+.. coqtop:: in
+
+   Inductive and (A B:Prop) : Prop := conj : A -> B -> A /\ B
+   where "A /\ B" := (and A B).
+
+   Fixpoint plus (n m:nat) {struct n} : nat :=
+     match n with
+     | O => m
+     | S p => S (p+m)
+     end
+   where "n + m" := (plus n m).
+
+Displaying informations about notations
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+.. opt:: Printing Notations
+
+   To deactivate the printing of all notations, use the command
+   ``Unset Printing Notations``. To reactivate it, use the command
+   ``Set Printing Notations``.
+
+   The default is to use notations for printing terms wherever possible.
+
+.. seealso::
+
+   :opt:`Printing All`
+      To disable other elements in addition to notations.
+
+Locating notations
+~~~~~~~~~~~~~~~~~~
+
+.. cmd:: Locate @symbol
+
+   To know to which notations a given symbol belongs to, use the command
+   ``Locate symbol``, where symbol is any (composite) symbol surrounded by double
+   quotes. To locate a particular notation, use a string where the variables of the
+   notation are replaced by “_” and where possible single quotes inserted around
+   identifiers or tokens starting with a single quote are dropped.
+
+   .. coqtop:: all
+
+      Locate "exists".
+      Locate "exists _ .. _ , _".
+
+   .. todo:: See also: Section 6.3.10.
+
+Notations and binders
+~~~~~~~~~~~~~~~~~~~~~
+
+Notations can include binders. This section lists
+different ways to deal with binders. For further examples, see also
+Section :ref:`RecursiveNotationsWithBinders`.
+
+Binders bound in the notation and parsed as identifiers
++++++++++++++++++++++++++++++++++++++++++++++++++++++++
+
+Here is the basic example of a notation using a binder:
+
+.. coqtop:: in
+
+   Notation "'sigma' x : A , B" := (sigT (fun x : A => B))
+     (at level 200, x ident, A at level 200, right associativity).
+
+The binding variables in the right-hand side that occur as a parameter
+of the notation (here :g:`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 :g:`B` can
+refer to the variable name bound to :g:`x` as shown in the following
+application of the notation:
+
+.. coqtop:: all
+
+   Check sigma z : nat, z = 0.
+
+Notice the modifier ``x ident`` in the declaration of the
+notation. It tells to parse :g:`x` as a single identifier.
+
+Binders bound in the notation and parsed as patterns
+++++++++++++++++++++++++++++++++++++++++++++++++++++
+
+In the same way as patterns can be used as binders, as in
+:g:`fun '(x,y) => x+y` or :g:`fun '(existT _ x _) => x`, notations can be
+defined so that any pattern (in the sense of the entry :n:`@pattern` of
+Figure :ref:`term-syntax-aux`) can be used in place of the
+binder. Here is an example:
+
+.. coqtop:: in reset
+
+   Notation "'subset' ' p , P " := (sig (fun p => P))
+     (at level 200, p pattern, format "'subset'  ' p ,  P").
+
+.. coqtop:: all
+
+   Check subset '(x,y), x+y=0.
+
+The modifier ``p pattern`` in the declaration of the notation tells to parse
+:g:`p` as a pattern. Note that a single variable is both an identifier and a
+pattern, so, e.g., the following also works:
+
+.. coqtop:: all
+
+   Check subset 'x, x=0.
+
+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 ``p strict pattern``. For parsing, however, a
+``strict pattern`` will continue to include the case of a
+variable. Here is an example showing the difference:
+
+.. coqtop:: in
+
+   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).
+
+.. coqtop:: all
+
+   Check subset_bis 'x, x=0.
+
+The default level for a ``pattern`` is 0. One can use a different level by
+using ``pattern at level`` :math:`n` where the scale is the same as the one for
+terms (Figure :ref:`init-notations`).
+
+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:
+
+.. coqtop:: in
+
+   Notation "{ x : A | P }" := (sig (fun x : A => P))
+       (at level 0, x at level 99 as ident).
+
+This is so because the grammar also contains rules starting with :g:`{}` and
+followed by a term, such as the rule for the notation :g:`{ A } + { B }` for the
+constant :g:`sumbool` (see Section :ref:`sumbool`).
+
+Then, in the rule, ``x ident`` is replaced by ``x at level 99 as ident`` meaning
+that ``x`` is parsed as a term at level 99 (as done in the notation for
+:g:`sumbool`), but that this term has actually to be an identifier.
+
+The notation :g:`{ x | P }` is already defined in the standard
+library with the ``as ident`` modifier. We cannot redefine it but
+one can define an alternative notation, say :g:`{ p such that P }`,
+using instead ``as pattern``.
+
+.. coqtop:: in
+
+   Notation "{ p 'such' 'that' P }" := (sig (fun p => P))
+     (at level 0, p at level 99 as pattern).
+
+Then, the following works:
+
+.. coqtop:: all
+
+   Check {(x,y) such that x+y=0}.
+
+To enforce that the pattern should not be used for printing when it
+is just an identifier, one could have said
+``p at level 99 as strict pattern``.
+
+Note also that in the absence of a ``as ident``, ``as strict pattern`` or
+``as pattern`` modifiers, the default is to consider subexpressions occurring
+in binding position and parsed as terms to be ``as ident``.
+
+.. _NotationsWithBinders:
+
+Binders not bound in 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
+
+.. coqtop:: in
+
+   Notation "'exists_different' n" := (exists p:nat, p<>n) (at level 200).
+
+the next command fails because p does not bind in the instance of n.
+
+.. coqtop:: all
+
+   Fail Check (exists_different p).
+
+.. coqtop:: in
+
+   Notation "[> a , .. , b <]" :=
+     (cons a .. (cons b nil) .., cons b .. (cons a nil) ..).
+
+.. _RecursiveNotationsWithBinders:
+
+Notations with recursive patterns
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+A mechanism is provided for declaring elementary notations with
+recursive patterns. The basic example is:
+
+.. coqtop:: all
+
+   Notation "[ x ; .. ; y ]" := (cons x .. (cons y nil) ..).
+
+On the right-hand side, an extra construction of the form ``.. t ..`` can
+be used. Notice that ``..`` is part of the Coq syntax and it must not be
+confused with the three-dots notation “``…``” used in this manual to denote
+a sequence of arbitrary size.
+
+On the left-hand side, the part “``x s .. s y``” of the 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 “``;``”).
+
+The right-hand side must contain a subterm of the form either
+``φ(x, .. φ(y,t) ..)`` or ``φ(y, .. φ(x,t) ..)`` where :math:`φ([~]_E , [~]_I)`,
+called the *iterator* of the recursive notation is an arbitrary expression with
+distinguished placeholders and where :math:`t` is called the *terminating
+expression* of the recursive notation. In the example, we choose the names
+:math:`x` and :math:`y` but in practice they can of course be chosen
+arbitrarily. Not atht the placeholder :math:`[~]_I` has to occur only once but
+:math:`[~]_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
+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 :math:`φ([~]_E , [~]_I)` is :math:`cons [~]_E [~]_I`
+and the terminating expression is ``nil``. Here are other examples:
+
+.. coqtop:: in
+
+   Notation "( x , y , .. , z )" := (pair .. (pair x y) .. z) (at level 0).
+
+   Notation "[| t * ( x , y , .. , z ) ; ( a , b , .. , c )  * u |]" :=
+     (pair (pair .. (pair (pair t x) (pair t y)) .. (pair t z))
+           (pair .. (pair (pair a u) (pair b u)) .. (pair c u)))
+     (t at level 39).
+
+Notations with recursive patterns can be reserved like standard
+notations, they can also be declared within interpretation scopes (see
+section 12.2).
+
+
+Notations with recursive patterns involving binders
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+Recursive notations can also be used with binders. The basic example
+is:
+
+.. coqtop:: all
+
+   Notation "'exists' x .. y , p" :=
+     (ex (fun x => .. (ex (fun y => p)) ..))
+     (at level 200, x binder, y binder, right associativity).
+
+The principle is the same as in Section 12.1.12 except that in the iterator
+:math:`φ([~]_E , [~]_I)`, the placeholder :math:`[~]_E` can also occur in
+position of the binding variable of a ``fun`` or a ``forall``.
+
+To specify that the part “``x .. y``” of the notation parses a sequence of
+binders, ``x`` and ``y`` must be marked as ``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 ``'`` (see Section 2.7.19) is used in the binding list,
+the added binders are taken into account too.
+
+Binders parsing exist in two flavors. If ``x`` and ``y`` are marked as binder,
+then a sequence such as :g:`a b c : T` will be accepted and interpreted as
+the sequence of binders :g:`(a:T) (b:T) (c:T)`. For instance, in the
+notation above, the syntax :g:`exists a b : nat, a = b` is valid.
+
+The variables ``x`` and ``y`` can also be marked as closed binder in which
+case only well-bracketed binders of the form :g:`(a b c:T)` or :g:`{a b c:T}`
+etc. are accepted.
+
+With closed binders, the recursive sequence in the left-hand side can
+be of the more general form ``x s .. 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:
+
+.. coqtop:: in
+
+   Notation "'mylet' f x .. y :=  t 'in' u":=
+     (let f := fun x => .. (fun y => t) .. in u)
+     (at level 200, x closed binder, y closed binder, right associativity).
+
+A recursive pattern for binders can be used in position of a recursive
+pattern for terms. Here is an example:
+
+.. coqtop:: in 
+
+   Notation "'FUNAPP' x .. y , f" :=
+     (fun x => .. (fun y => (.. (f x) ..) y ) ..)
+     (at level 200, x binder, y binder, right associativity).
+
+If an occurrence of the :math:`[~]_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:
+
+.. coqtop:: in
+
+   Notation "'exists_non_null' x .. y  , P" :=
+     (ex (fun x => x <> 0 /\ .. (ex (fun y => y <> 0 /\ P)) ..))
+     (at level 200, x binder).
+
+Predefined entries
+~~~~~~~~~~~~~~~~~~
+
+By default, sub-expressions are parsed as terms and the corresponding
+grammar entry is called :n:`@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 :g:`x`:
+
+.. coqtop:: in
+
+   Notation "'apply' f a1 .. an" := (.. (f a1) .. an)
+     (at level 10, f global, a1, an at level 9).
+
+In addition to ``global``, one can restrict the syntax of a
+sub-expression by using the entry names ``ident`` or ``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.:
+
+.. coqtop:: in
+
+   Notation "'apply_id' f a1 .. an" := (.. (f a1) .. an)
+     (at level 10, f ident, a1, an at level 9).
+
+Summary
+~~~~~~~
+
+Syntax of notations
+~~~~~~~~~~~~~~~~~~~
+
+The different syntactic variants of the command Notation are given on the
+following figure. The optional :token:`scope` is described in the Section 12.2.
+
+.. productionlist:: coq
+   notation      : [Local] Notation `string` := `term` [`modifiers`] [: `scope`].
+                 : | [Local] Infix `string` := `qualid` [`modifiers`] [: `scope`].
+                 : | [Local] Reserved Notation `string` [`modifiers`] .
+                 : | Inductive `ind_body` [`decl_notation`] with … with `ind_body` [`decl_notation`].
+                 : | CoInductive `ind_body` [`decl_notation`] with … with `ind_body` [`decl_notation`].
+                 : | Fixpoint `fix_body` [`decl_notation`] with … with `fix_body` [`decl_notation`].
+                 : | CoFixpoint `cofix_body` [`decl_notation`] with … with `cofix_body` [`decl_notation`].
+   decl_notation : [where `string` := `term` [: `scope`] and … and `string` := `term` [: `scope`]].
+   modifiers     : at level `natural`
+                 : | `ident` , … , `ident` at level `natural` [`binderinterp`]
+                 : | `ident` , … , `ident` at next level [`binderinterp`]
+                 : | `ident` ident
+                 : | `ident` global
+                 : | `ident` bigint
+                 : | `ident` [strict] pattern [at level `natural`]
+                 : | `ident` binder
+                 : | `ident` closed binder
+                 : | left associativity
+                 : | right associativity
+                 : | no associativity
+                 : | only parsing
+                 : | only printing
+                 : | format `string`
+   binderinterp  : as ident
+                 : | as pattern
+                 : | as strict pattern
+
+.. note:: No typing of the denoted expression is performed at definition
+          time. Type-checking is done only at the time of use of the notation.
+
+.. note:: Many examples of Notation may be found in the files composing
+          the initial state of Coq (see directory :file:`$COQLIB/theories/Init`).
+
+.. note:: The notation ``"{ x }"`` has a special status in such a way that
+          complex notations of the form ``"x + { y }"`` or ``"x * { y }"`` can be
+          nested with correct precedences. Especially, every notation involving
+          a pattern of the form ``"{ x }"`` is parsed as a notation where the
+          pattern ``"{ x }"`` has been simply replaced by ``"x"`` and the curly
+          brackets are parsed separately. E.g. ``"y + { z }"`` is not parsed as a
+          term of the given form but as a term of the form ``"y + z"`` where ``z``
+          has been parsed using the rule parsing ``"{ x }"``. Especially, level
+          and precedences for a rule including patterns of the form ``"{ x }"``
+          are relative not to the textual notation but to the notation where the
+          curly brackets have been removed (e.g. the level and the associativity
+          given to some notation, say ``"{ y } & { z }"`` in fact applies to the
+          underlying ``"{ x }"``\-free rule which is ``"y & z"``).
+
+Persistence of notations
+~~~~~~~~~~~~~~~~~~~~~~~~
+
+Notations do not survive the end of sections.
+
+.. cmd:: Local Notation @notation
+
+   Notations survive modules unless the command ``Local Notation`` is used instead
+   of ``Notation``.
+
+Interpretation scopes
+----------------------
+
+An *interpretation scope* is a set of notations for terms with their
+interpretation. Interpretation scopes provide a weak, purely
+syntactical form of notations overloading: the same notation, for
+instance the infix symbol ``+`` can be used to denote distinct
+definitions of the additive operator. Depending on which interpretation
+scopes is currently open, the interpretation is different.
+Interpretation scopes can include an interpretation for numerals and
+strings. However, this is only made possible at the Objective Caml
+level.
+
+See Figure 12.1 for the syntax of notations including the possibility
+to declare them in a given scope. Here is a typical example which
+declares the notation for conjunction in the scope ``type_scope``.
+
+.. coqdoc::
+
+   Notation "A /\ B" := (and A B) : type_scope.
+
+.. note:: A notation not defined in a scope is called a *lonely*
+          notation.
+
+Global interpretation rules for notations
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+At any time, the interpretation of a notation for term is done within
+a *stack* of interpretation scopes and lonely notations. In case a
+notation has several interpretations, the actual interpretation is the
+one defined by (or in) the more recently declared (or open) lonely
+notation (or interpretation scope) which defines this notation.
+Typically if a given notation is defined in some scope ``scope`` but has
+also an interpretation not assigned to a scope, then, if ``scope`` is open
+before the lonely interpretation is declared, then the lonely
+interpretation is used (and this is the case even if the
+interpretation of the notation in scope is given after the lonely
+interpretation: otherwise said, only the order of lonely
+interpretations and opening of scopes matters, and not the declaration
+of interpretations within a scope).
+
+The initial state of Coq declares three interpretation scopes and no
+lonely notations. These scopes, in opening order, are ``core_scope``,
+``type_scope`` and ``nat_scope``.
+
+.. cmd:: Open Scope @scope
+
+   The command to add a scope to the interpretation scope stack is
+   :n:`Open Scope @scope`.
+
+.. cmd:: Close Scope @scope
+
+   It is also possible to remove a scope from the interpretation scope
+   stack by using the command :n:`Close Scope @scope`.
+
+   Notice that this command does not only cancel the last :n:`Open Scope @scope`
+   but all the invocations of it.
+
+.. note:: ``Open Scope`` and ``Close Scope`` do not survive the end of sections
+          where they occur. When defined outside of a section, they are exported
+          to the modules that import the module where they occur.
+
+.. cmd:: Local Open Scope @scope.
+         Local Close Scope @scope.
+
+   These variants are not exported to the modules that import the module where
+   they occur, even if outside a section.
+
+.. cmd:: Global Open Scope @scope.
+         Global Close Scope @scope.
+
+   These variants survive sections. They behave as if Global were absent when
+   not inside a section.
+
+Local interpretation rules for notations
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+In addition to the global rules of interpretation of notations, some
+ways to change the interpretation of subterms are available.
+
+Local opening of an interpretation scope
++++++++++++++++++++++++++++++++++++++++++
+
+It is possible to locally extend the interpretation scope stack using the syntax
+:g:`(term)%key` (or simply :g:`term%key` for atomic terms), where key is a
+special identifier called *delimiting key* and bound to a given scope.
+
+In such a situation, the term term, and all its subterms, are
+interpreted in the scope stack extended with the scope bound tokey.
+
+.. cmd:: Delimit Scope @scope with @ident
+
+   To bind a delimiting key to a scope, use the command
+   :n:`Delimit Scope @scope with @ident`
+
+.. cmd:: Undelimit Scope @scope
+
+   To remove a delimiting key of a scope, use the command
+   :n:`Undelimit Scope @scope`
+
+Binding arguments of a constant to an interpretation scope
++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
+
+.. cmd:: Arguments @qualid {+ @name%@scope}
+
+   It is possible to set in advance that some arguments of a given constant have
+   to be interpreted in a given scope. The command is
+   :n:`Arguments @qualid {+ @name%@scope}` where the list is a prefix 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 :g:`plus_fct`
+   in the scope delimited by the key ``F`` (``Rfun_scope``) and the last
+   argument in the scope delimited by the key ``R`` (``R_scope``).
+
+   .. coqtop:: in
+
+      Arguments plus_fct (f1 f2)%F x%R.
+
+   The ``Arguments`` command accepts scopes decoration to all grouping
+   parentheses. In the following example arguments A and B are marked as
+   maximally inserted implicit arguments and are put into the type_scope scope.
+
+   .. coqtop:: in
+
+      Arguments respectful {A B}%type (R R')%signature _ _.
+
+   When interpreting a term, if some of the arguments of qualid are built
+   from a notation, then this notation is interpreted in the scope stack
+   extended by the scope bound (if any) to this argument. The effect of
+   the scope is limited to the argument itself. It does not propagate to
+   subterms but the subterms that, after interpretation of the notation,
+   turn to be themselves arguments of a reference are interpreted
+   accordingly to the arguments scopes bound to this reference.
+
+.. cmdv:: Arguments @qualid : clear scopes
+
+   Arguments scopes can be cleared with :n:`Arguments @qualid : clear scopes`.
+
+.. cmdv:: Arguments @qualid {+ @name%scope} : extra scopes
+
+   Defines extra argument scopes, to be used in case of coercion to Funclass
+   (see Chapter :ref:`Coercions-full`) or with a computed type.
+
+.. cmdv:: Global Arguments @qualid {+ @name%@scope}
+
+   This behaves like :n:`Arguments qualid {+ @name%@scope}` but survives when a
+   section is closed instead of stopping working at section closing. Without the
+   ``Global`` modifier, the effect of the command stops when the section it belongs
+   to ends.
+
+.. cmdv:: Local Arguments @qualid {+ @name%@scope}
+
+   This behaves like :n:`Arguments @qualid {+ @name%@scope}` but does not
+   survive modules and files. Without the ``Local`` modifier, the effect of the
+   command is visible from within other modules or files.
+
+.. seealso::
+
+   :cmd:`About @qualid`
+     The command to show the scopes bound to the arguments of a
+     function is described in Section 2.
+
+.. note::
+
+   In notations, the subterms matching the identifiers of the
+   notations are interpreted in the scope in which the identifiers
+   occurred at the time of the declaration of the notation. Here is an
+   example:
+
+   .. coqtop:: all
+
+      Parameter g : bool -> bool.
+      Notation "@@" := true (only parsing) : bool_scope.
+      Notation "@@" := false (only parsing): mybool_scope.
+
+      Bind Scope bool_scope with bool.
+      Notation "# x #" := (g x) (at level 40).
+      Check # @@ #.
+      Arguments g _%mybool_scope.
+      Check # @@ #.
+      Delimit Scope mybool_scope with mybool.
+      Check # @@%mybool #.
+
+Binding types of arguments to an interpretation scope
++++++++++++++++++++++++++++++++++++++++++++++++++++++
+
+.. cmd:: Bind Scope @scope with @qualid
+
+   When an interpretation scope is naturally associated to a type (e.g.  the
+   scope of operations on the natural numbers), it may be convenient to bind it
+   to this type. When a scope ``scope`` is bound to a type type, any new function
+   defined later on gets its arguments of type type interpreted by default in
+   scope scope (this default behavior can however be overwritten by explicitly
+   using the command ``Arguments``).
+
+   Whether the argument of a function has some type ``type`` is determined
+   statically. For instance, if f is a polymorphic function of type :g:`forall
+   X:Type, X -> X` and type :g:`t` is bound to a scope ``scope``, then :g:`a` of
+   type :g:`t` in :g:`f t a` is not recognized as an argument to be interpreted
+   in scope ``scope``.
+
+   More generally, any coercion :n:`@class` (see Chapter :ref:`Coercions-full`)
+   can be bound to an interpretation scope. The command to do it is
+   :n:`Bind Scope @scope with @class`
+
+   .. coqtop:: in
+
+      Parameter U : Set.
+      Bind Scope U_scope with U.
+      Parameter Uplus : U -> U -> U.
+      Parameter P : forall T:Set, T -> U -> Prop.
+      Parameter f : forall T:Set, T -> U.
+      Infix "+" := Uplus : U_scope.
+      Unset Printing Notations.
+      Open Scope nat_scope.
+
+   .. coqtop:: all
+
+      Check (fun x y1 y2 z t => P _ (x + t) ((f _ (y1 + y2) + z))).
+
+   .. note:: The scopes ``type_scope`` and ``function_scope`` also have a local
+             effect on interpretation. See the next section.
+
+.. seealso::
+
+   :cmd:`About`
+     The command to show the scopes bound to the arguments of a
+     function is described in Section 2.
+
+The ``type_scope`` interpretation scope
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+.. index:: type_scope
+
+The scope ``type_scope`` has a special status. It is a primitive interpretation
+scope which is temporarily activated each time a subterm of an expression is
+expected to be a type. It is delimited by the key ``type``, and bound to the
+coercion class ``Sortclass``. It is also used in certain situations where an
+expression is statically known to be a type, including the conclusion and the
+type of hypotheses within an Ltac goal match (see Section
+:ref:`ltac-match-goal`), the statement of a theorem, the type of a definition,
+the type of a binder, the domain and codomain of implication, the codomain of
+products, and more generally any type argument of a declared or defined
+constant.
+
+The ``function_scope`` interpretation scope
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+.. index:: function_scope
+
+The scope ``function_scope`` also has a special status. 
+It is temporarily activated each time the argument of a global reference is
+recognized to be a ``Funclass`` istance, i.e., of type :g:`forall x:A, B` or
+:g:`A -> B`.
+
+
+Interpretation scopes used in the standard library of Coq
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+We give an overview of the scopes used in the standard library of Coq.
+For a complete list of notations in each scope, use the commands Print
+Scopes or Print Scope scope.
+
+``type_scope``
+  This scope includes infix * for product types and infix + for sum types. It
+  is delimited by key ``type``, and bound to the coercion class 
+  ``Sortclass``, as described above.
+
+``function_scope``
+  This scope is delimited by key ``function``, and bound to the coercion class 
+  ``Funclass``, as described above.
+
+``nat_scope``
+  This scope includes the standard arithmetical operators and relations on type
+  nat. Positive numerals in this scope are mapped to their canonical
+  representent built from :g:`O` and :g:`S`. The scope is delimited by key
+  ``nat``, and bound to the type :g:`nat` (see above).
+
+``N_scope``
+  This scope includes the standard arithmetical operators and relations on
+  type :g:`N` (binary natural numbers). It is delimited by key ``N`` and comes
+  with an interpretation for numerals as closed terms of type :g:`N`.
+
+``Z_scope``
+  This scope includes the standard arithmetical operators and relations on
+  type :g:`Z` (binary integer numbers). It is delimited by key ``Z`` and comes
+  with an interpretation for numerals as closed term of type :g:`Z`.
+
+``positive_scope``
+  This scope includes the standard arithmetical operators and relations on
+  type :g:`positive` (binary strictly positive numbers). It is delimited by
+  key ``positive`` and comes with an interpretation for numerals as closed
+  term of type :g:`positive`.
+
+``Q_scope``
+  This scope includes the standard arithmetical operators and relations on
+  type :g:`Q` (rational numbers defined as fractions of an integer and a
+  strictly positive integer modulo the equality of the numerator-
+  denominator cross-product). As for numerals, only 0 and 1 have an
+  interpretation in scope ``Q_scope`` (their interpretations are 0/1 and 1/1
+  respectively).
+
+``Qc_scope``
+  This scope includes the standard arithmetical operators and relations on the
+  type :g:`Qc` of rational numbers defined as the type of irreducible
+  fractions of an integer and a strictly positive integer.
+
+``real_scope``
+  This scope includes the standard arithmetical operators and relations on
+  type :g:`R` (axiomatic real numbers). It is delimited by key ``R`` and comes
+  with an interpretation for numerals using the :g:`IZR` morphism from binary
+  integer numbers to :g:`R`.
+
+``bool_scope``
+  This scope includes notations for the boolean operators. It is delimited by
+  key ``bool``, and bound to the type :g:`bool` (see above).
+
+``list_scope``
+  This scope includes notations for the list operators. It is delimited by key
+  ``list``, and bound to the type :g:`list` (see above).
+
+``core_scope``
+  This scope includes the notation for pairs. It is delimited by key ``core``.
+
+``string_scope``
+  This scope includes notation for strings as elements of the type string.
+  Special characters and escaping follow Coq conventions on strings (see
+  Section 1.1). Especially, there is no convention to visualize non
+  printable characters of a string. The file :file:`String.v` shows an example
+  that contains quotes, a newline and a beep (i.e. the ASCII character
+  of code 7).
+
+``char_scope``
+  This scope includes interpretation for all strings of the form ``"c"``
+  where :g:`c` is an ASCII character, or of the form ``"nnn"`` where nnn is
+  a three-digits number (possibly with leading 0's), or of the form
+  ``""""``. Their respective denotations are the ASCII code of c, the
+  decimal ASCII code nnn, or the ascii code of the character ``"`` (i.e.
+  the ASCII code 34), all of them being represented in the type :g:`ascii`.
+
+
+Displaying informations about scopes
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+.. cmd:: Print Visibility
+
+   This displays the current stack of notations in scopes and lonely
+   notations that is used to interpret a notation. The top of the stack
+   is displayed last. Notations in scopes whose interpretation is hidden
+   by the same notation in a more recently open scope are not displayed.
+   Hence each notation is displayed only once.
+
+.. cmdv:: Print Visibility scope
+
+   This displays the current stack of notations in scopes and lonely
+   notations assuming that scope is pushed on top of the stack. This is
+   useful to know how a subterm locally occurring in the scope ofscope is
+   interpreted.
+
+.. cmdv:: Print Scope scope
+
+   This displays all the notations defined in interpretation scopescope.
+   It also displays the delimiting key if any and the class to which the
+   scope is bound, if any.
+
+.. cmdv:: Print Scopes
+
+   This displays all the notations, delimiting keys and corresponding
+   class of all the existing interpretation scopes. It also displays the
+   lonely notations.
+
+Abbreviations
+--------------
+
+.. cmd:: {? Local} Notation @ident {+ @ident} := @term {? (only parsing)}.
+
+   An *abbreviation* is a name, possibly applied to arguments, that
+   denotes a (presumably) more complex expression. Here are examples:
+
+   .. coqtop:: none
+
+      Require Import List.
+      Require Import Relations.
+      Set Printing Notations.
+
+   .. coqtop:: in
+
+      Notation Nlist := (list nat).
+
+   .. coqtop:: all
+
+      Check 1 :: 2 :: 3 :: nil.
+
+   .. coqtop:: in
+
+      Notation reflexive R := (forall x, R x x).
+
+   .. coqtop:: all
+
+      Check forall A:Prop, A <-> A.
+      Check reflexive iff.
+
+   An abbreviation expects no precedence nor associativity, since it
+   is parsed as an usual application. Abbreviations are used as
+   much as possible by the Coq printers unless the modifier ``(only
+   parsing)`` is given.
+
+   Abbreviations are bound to an absolute name as an ordinary definition
+   is, and they can be referred by qualified names too.
+
+   Abbreviations are syntactic in the sense that they are bound to
+   expressions which are not typed at the time of the definition of the
+   abbreviation but at the time it is used. Especially, abbreviations can
+   be bound to terms with holes (i.e. with “``_``”). For example:
+
+   .. coqtop:: none reset
+
+      Set Strict Implicit.
+      Set Printing Depth 50.
+
+   .. coqtop:: in
+
+      Definition explicit_id (A:Set) (a:A) := a.
+      Notation id := (explicit_id _).
+
+   .. coqtop:: all
+
+      Check (id 0).
+
+   Abbreviations 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 abbreviation.
+
+Tactic Notations
+-----------------
+
+Tactic notations allow to customize the syntax of the tactics of the
+tactic language. Tactic notations obey the following syntax:
+
+.. productionlist:: coq
+   tacn                 : [Local] Tactic Notation [`tactic_level`] [`prod_item` … `prod_item`] := `tactic`.
+   prod_item            : `string` | `tactic_argument_type`(`ident`)
+   tactic_level         : (at level `natural`)
+   tactic_argument_type : ident | simple_intropattern | reference
+                        : | hyp | hyp_list | ne_hyp_list
+                        : | constr | uconstr | constr_list | ne_constr_list
+                        : | integer | integer_list | ne_integer_list
+                        : | int_or_var | int_or_var_list | ne_int_or_var_list
+                        : | tactic | tactic0 | tactic1 | tactic2 | tactic3
+                        : | tactic4 | tactic5
+
+.. cmd:: {? Local} Tactic Notation {? (at level @level)} {+ @prod_item} := @tactic.
+
+   A tactic notation extends the parser and pretty-printer of tactics with a new
+   rule made of the list of production items. It then evaluates into the
+   tactic expression ``tactic``. For simple tactics, it is recommended to use
+   a terminal symbol, i.e. a string, for the first production item. The
+   tactic 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).
+
+   .. cmd:: Print Grammar tactic
+
+      To know the parsing precedences of the existing tacticals, use the command
+      ``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
+   following table. The last command gives examples of tactics which use
+   the corresponding kind of argument.
+
+   .. list-table::
+      :header-rows: 1
+
+      * - Tactic argument type
+        - parsed as
+        - interpreted as
+        - as in tactic
+
+      * - ``ident``
+        - identifier
+        - a user-given name
+        - intro
+
+      * - ``simple_intropattern``
+        - intro_pattern
+        - an intro_pattern
+        - intros
+
+      * - ``hyp``
+        - identifier
+        - an hypothesis defined in context
+        - clear
+
+      * - ``reference``
+        - qualified identifier
+        - a global reference of term
+        - unfold
+
+      * - ``constr``
+        - term
+        - a term
+        - exact
+
+      * - ``uconstr``
+        - term
+        - an untyped term
+        - refine
+
+      * - ``integer``
+        - integer
+        - an integer
+        -
+
+      * - ``int_or_var``
+        - identifier or integer
+        - an integer
+        - do
+
+      * - ``tactic``
+        - tactic at level 5
+        - a tactic
+        -
+
+      * - ``tacticn``
+        - tactic at level n
+        - a tactic
+        -
+
+      * - *entry*\ ``_list``
+        - list of *entry*
+        - a list of how *entry* is interpreted
+        -
+
+      * - ``ne_``\ *entry*\ ``_list``
+        - non-empty list of *entry*
+        - a list of how *entry* is interpreted
+        -
+
+   .. note:: In order to be bound in tactic definitions, each syntactic
+             entry for argument type must include the case of simple L tac
+             identifier as part of what it parses. This is naturally the case for
+             ``ident``, ``simple_intropattern``, ``reference``, ``constr``, ... but not for ``integer``.
+             This is the reason for introducing a special entry ``int_or_var`` which
+             evaluates to integers only but which syntactically includes
+             identifiers in order to be usable in tactic definitions.
+
+   .. note:: The *entry*\ ``_list`` and ``ne_``\ *entry*\ ``_list`` entries can be used in
+             primitive tactics or in other notations at places where a list of the
+             underlying entry can be used: entry is either ``constr``, ``hyp``, ``integer``
+             or ``int_or_var``.
+
+.. cmdv:: Local Tactic Notation
+
+   Tactic notations do not survive the end of sections. They survive
+   modules unless the command Local Tactic Notation is used instead of
+   Tactic Notation.
+
+.. rubric:: Footnotes
+
+.. [#and_or_levels] which are the levels effectively chosen in the current
+   implementation of Coq
+
+.. [#no_associativity] Coq accepts notations declared as no associative but the parser on
+   which Coq is built, namely Camlp4, 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