18 files changed, 444 insertions, 237 deletions
diff --git a/doc/LICENSE b/doc/LICENSE
index ada22e6690..0aa0d629e8 100644
--- a/doc/LICENSE
+++ b/doc/LICENSE
@@ -25,16 +25,6 @@ the PostScript, PDF and html outputs) are copyright (c) INRIA
 distributed under the terms of the Lesser General Public License
 version 2.1 or later. 
 
-The FAQ (Coq for the Clueless) is a work by Pierre Castéran, Hugo
-Herbelin, Florent Kirchner, Benjamin Monate, and Julien Narboux. All
-documents (the LaTeX source and the PostScript, PDF and html outputs)
-are copyright (c) INRIA 2004-2006. The material connected to the FAQ
-(Coq for the Clueless) may be distributed only subject to the terms
-and conditions set forth in the Open Publication License, v1.0 or
-later (the latest version is presently available at
-http://www.opencontent.org/openpub/). Options A and B are *not*
-elected.
-
 The Tutorial on [Co-]Inductive Types in Coq is a work by Pierre
 Castéran and Eduardo Gimenez. All related documents (the LaTeX and
 BibTeX sources and the PostScript, PDF and html outputs) are copyright
diff --git a/doc/common/macros.tex b/doc/common/macros.tex
index 81def1674c..6a28c5b3d1 100644
--- a/doc/common/macros.tex
+++ b/doc/common/macros.tex
@@ -182,6 +182,7 @@
 \newcommand{\declnotation}{\nterm{decl\_notation}} 
 \newcommand{\symbolentry}{\nterm{symbol}}
 \newcommand{\modifiers}{\nterm{modifiers}}
+\newcommand{\binderinterp}{\nterm{binder\_interp}}
 \newcommand{\localdef}{\nterm{local\_def}}
 \newcommand{\localdecls}{\nterm{local\_decls}}
 \newcommand{\ident}{\nterm{ident}}
diff --git a/doc/refman/AsyncProofs.tex b/doc/refman/AsyncProofs.tex
index 30039d4898..8f9d876cb8 100644
--- a/doc/refman/AsyncProofs.tex
+++ b/doc/refman/AsyncProofs.tex
@@ -1,4 +1,4 @@
-\achapter{Asynchronous and Parallel Proof Processing}
+\achapter{Asynchronous and Parallel Proof Processing\label{Asyncprocessing}}
 %HEVEA\cutname{async-proofs.html}
 \aauthor{Enrico Tassi}
 
diff --git a/doc/refman/Classes.tex b/doc/refman/Classes.tex
index 6e76d04e77..da798a238e 100644
--- a/doc/refman/Classes.tex
+++ b/doc/refman/Classes.tex
@@ -492,26 +492,6 @@ control on the triggering of instances.  For example, forcing a constant
 to explicitely appear in the pattern will make it never apply on a goal
 where there is a hole in that place.
 
-\subsection{\tt Set Typeclasses Legacy Resolution}
-\optindex{Typeclasses Legacy Resolution}
-\emph{Deprecated since 8.7}
-
-This option (off by default) uses the 8.5 implementation of resolution.
-Use for compatibility purposes only (porting and debugging).
-
-\subsection{\tt Set Typeclasses Module Eta}
-\optindex{Typeclasses Modulo Eta}
-\emph{Deprecated since 8.7}
-
-This option allows eta-conversion for functions and records during
-unification of type-classes. This option is unsupported since 8.6 with
-{\tt Typeclasses Filtered Unification} set, but still affects the
-default unification strategy, and the one used in {\tt Legacy
-  Resolution} mode. It is \emph{unset} by default. If {\tt Typeclasses
-  Filtered Unification} is set, this has no effect and unification will
-find solutions up-to eta conversion. Note however that syntactic
-pattern-matching is not up-to eta.
-
 \subsection{\tt Set Typeclasses Limit Intros}
 \optindex{Typeclasses Limit Intros}
 
@@ -525,13 +505,6 @@ invertibility status of the product introduction rule, resulting in
 potentially more expensive proof-search (i.e. more useless
 backtracking).
 
-\subsection{\tt Set Typeclass Resolution After Apply}
-\optindex{Typeclass Resolution After Apply}
-\emph{Deprecated since 8.6}
-
-This option (off by default in Coq 8.6 and 8.5) controls the resolution
-of typeclass subgoals generated by the {\tt apply} tactic.
-
 \subsection{\tt Set Typeclass Resolution For Conversion}
 \optindex{Typeclass Resolution For Conversion}
 
diff --git a/doc/refman/RefMan-com.tex b/doc/refman/RefMan-com.tex
index 04a8a25c12..5b73ac00a6 100644
--- a/doc/refman/RefMan-com.tex
+++ b/doc/refman/RefMan-com.tex
@@ -241,6 +241,20 @@ The following command-line options are recognized by the commands {\tt
   Collapse the universe hierarchy of {\Coq}. Warning: this makes the
   logic inconsistent.
 
+\item[{\tt -mangle-names} {\em ident}]\ %
+
+  Experimental: Do not depend on this option.
+
+  Replace Coq's auto-generated name scheme with names of the form
+  {\tt ident0}, {\tt ident1}, \ldots etc.
+  The command {\tt Set Mangle Names}\optindex{Mangle Names} turns
+  the behavior on in a document, and {\tt Set Mangle Names Prefix "ident"}
+  \optindex{Mangle Names Prefix} changes the used prefix.
+
+  This feature is intended to be used as a linter for developments that want
+  to be robust to changes in the auto-generated name scheme. The options are
+  provided to facilitate tracking down problems.
+
 \item[{\tt -compat} {\em version}]\ %
 
   Attempt to maintain some backward-compatibility with a previous version.
diff --git a/doc/refman/RefMan-ide.tex b/doc/refman/RefMan-ide.tex
index 436099e74d..2d98534307 100644
--- a/doc/refman/RefMan-ide.tex
+++ b/doc/refman/RefMan-ide.tex
@@ -44,9 +44,10 @@ bottom is the status bar.
 In the script window, you may open arbitrarily many buffers to
 edit. The \emph{File} menu allows you to open files or create some,
 save them, print or export them into various formats. Among all these
-buffers, there is always one which is the current \emph{running
-  buffer}, whose name is displayed on a green background, which is the
-one where Coq commands are currently executed. 
+buffers, there is always one which is the current
+\emph{running buffer}, whose name is displayed on a background in the
+\emph{processed} color (green by default), which is the one where Coq commands
+are currently executed.
 
 Buffers may be edited as in any text editor, and classical basic
 editing commands (Copy/Paste, \ldots) are available in the \emph{Edit}
@@ -58,12 +59,13 @@ menu.
 \section{Interactive navigation into \Coq{} scripts}
 
 The running buffer is the one where navigation takes place. The
-toolbar proposes five basic commands for this. The first one,
+toolbar offers five basic navigation commands. The first one,
 represented by a down arrow icon, is for going forward executing one
 command. If that command is successful, the part of the script that
-has been executed is displayed on a green background. If that command
-fails, the error message is displayed in the message window, and the
-location of the error is emphasized by a red underline.
+has been executed is displayed on a background with the
+processed color. If that command fails, the error message is
+displayed in the message window, and the location of the error is
+emphasized by an underline in the error foreground color (red by default).
 
 On Figure~\ref{fig:coqide}, the running buffer is \verb|Fermat.v|, all
 commands until the \verb|Theorem| have been already executed, and the
@@ -71,23 +73,41 @@ user tried to go forward executing \verb|Induction n|. That command
 failed because no such tactic exist (tactics are now in
 lowercase\ldots), and the wrong word is underlined. 
 
-Notice that the green part of the running buffer is not editable. If
+Notice that the processed part of the running buffer is not editable. If
 you ever want to modify something you have to go backward using the up
 arrow tool, or even better, put the cursor where you want to go back
 and use the \textsf{goto} button. Unlike with \verb|coqtop|, you
 should never use \verb|Undo| to go backward.
 
-Two additional tool buttons exist, one to go directly to the end and
-one to go back to the beginning. If you try to go to the end, or in
-general to run several commands using the \textsf{goto} button, the
-  execution will stop whenever an error is found.
+There are two additional buttons for navigation within the running buffer.
+The ``down'' button with a line goes directly to the end; the ``up'' button
+with a line goes back to the beginning. The handling of errors when using the
+go-to-the-end button depends on whether \Coq{} is running in asynchronous mode or not
+(see Chapter~\ref{Asyncprocessing}). If it is not running in that mode, execution stops
+as soon as an error is found. Otherwise, execution continues, and the
+error is marked with an underline in the error foreground color, with a background in
+the error background color (pink by default). The same characterization of
+error-handling applies when running several commands using the \textsf{goto} button.
 
 If you ever try to execute a command which happens to run during a
 long time, and would like to abort it before its
 termination, you may use the interrupt button (the white cross on a red circle).
  
-Finally, notice that these navigation buttons are also available in
-the menu, where their keyboard shortcuts are given.
+There are other buttons on the \CoqIDE{} toolbar: a button to save the running
+buffer; a button to close the current buffer (an ``X''); buttons to switch among
+buffers (left and right arrows); an ``information'' button; and a ``gears'' button.
+
+The ``information'' button is described in Section~\ref{sec:trytactics}.
+
+The ``gears'' button submits proof terms to the \Coq{} kernel for type-checking.
+When \Coq{} uses asynchronous processing (see Chapter~\ref{Asyncprocessing}), proofs may
+have been completed without kernel-checking of generated proof terms. The presence of
+unchecked proof terms is indicated by \texttt{Qed} statements
+that have a subdued \emph{being-processed} color (light blue by default),
+rather than the processed color, though their preceding proofs have the processed color.
+
+Notice that for all these buttons, except for the ``gears'' button, their operations
+are also available in the menu, where their keyboard shortcuts are given.
 
 \section[Try tactics automatically]{Try tactics automatically\label{sec:trytactics}}
 
@@ -96,8 +116,8 @@ trying to solve the current goal using simple tactics. If such a
 tactic succeeds in solving the goal, then its text is automatically
 inserted into the script. There is finally a combination of these
 tactics, called the \emph{proof wizard} which will try each of them in
-turn. This wizard is also available as a tool button (the light
-bulb).  The set of tactics tried by the wizard is customizable in
+turn. This wizard is also available as a tool button (the ``information''
+button).  The set of tactics tried by the wizard is customizable in
 the preferences.
 
 These tactics are general ones, in particular they do not refer to
@@ -132,7 +152,7 @@ arguments.
 
 \begin{figure}[t]
 \begin{center}
-%HEVEA\imgsrc[alt="coqide query window"]{coqide-queries.png}
+%HEVEA\imgsrc[alt="coqide query"]{coqide-queries.png}
 %BEGIN LATEX
 \ifpdf  % si on est en pdflatex
 \includegraphics[width=1.0\textwidth]{coqide-queries.png}
@@ -141,27 +161,21 @@ arguments.
 \fi
 %END LATEX
 \end{center}
-\caption{\CoqIDE{}: the query window}
-\label{fig:querywindow}
+\caption{\CoqIDE{}: a Print query on a selected phrase}
+\label{fig:queryselected}
 \end{figure}
 
-
-We call \emph{query} any vernacular command that do not change the
-current state, such as \verb|Check|, \verb|Search|, etc. Those
-commands are of course useless during compilation of a file, hence
-should not be included in scripts. To run such commands without
-writing them in the script, \CoqIDE{} offers another input window
-called the \emph{query window}. This window can be displayed on
-demand, either by using the \texttt{Window} menu, or directly using
-shortcuts given in the \texttt{Queries} menu. Indeed, with \CoqIDE{}
-the simplest way to perform a \texttt{Search} on some identifier
-is to select it using the mouse, and pressing \verb|F2|. This will
-both make appear the query window and run the \texttt{Search} in
-it, displaying the result. Shortcuts \verb|F3| and \verb|F4| are for
-\verb|Check| and \verb|Print| respectively.
-Figure~\ref{fig:querywindow} displays the query window after selection
-of the word ``mult'' in the script windows, and pressing \verb|F4| to
-print its definition.
+We call \emph{query} any vernacular command that does not change the
+current state, such as \verb|Check|, \verb|Search|, etc.
+To run such commands interactively, without writing them in scripts,
+\CoqIDE{} offers a \emph{query pane}.
+The query pane can be displayed on demand by using the \texttt{View} menu,
+or using the shortcut \verb|F1|. Queries can also be performed by
+selecting a particular phrase, then choosing an item from the
+\texttt{Queries} menu. The response then appears in the message window.
+Figure~\ref{fig:queryselected} shows the result after selecting
+of the phrase \verb|Nat.mul| in the script window, and choosing \verb|Print|
+from the \texttt{Queries} menu.
 
 \section{Compilation}
 
diff --git a/doc/refman/RefMan-lib.tex b/doc/refman/RefMan-lib.tex
index c8e8443026..89f5be8438 100644
--- a/doc/refman/RefMan-lib.tex
+++ b/doc/refman/RefMan-lib.tex
@@ -55,6 +55,7 @@ Figure~\ref{init-notations}.
 \hline
 Notation & Precedence & Associativity \\
 \hline
+\verb!_ -> _! & 99 & right \\
 \verb!_ <-> _! & 95 & no \\
 \verb!_ \/ _!  & 85 & right \\
 \verb!_ /\ _!  & 80 & right \\
diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex
index ef0f4af8f6..0a4d0ef9aa 100644
--- a/doc/refman/RefMan-ltac.tex
+++ b/doc/refman/RefMan-ltac.tex
@@ -1156,16 +1156,6 @@ without having to cut manually the proof in smaller lemmas.
 It may be useful to generate lemmas minimal w.r.t. the assumptions they depend
 on. This can be obtained thanks to the option below.
 
-\begin{quote}
-\optindex{Shrink Abstract}
-{\tt Set Shrink Abstract}
-\end{quote}
-\emph{Deprecated since 8.7}
-
-When set (default), all lemmas generated through \texttt{abstract {\tacexpr}}
-and \texttt{transparent\_abstract {\tacexpr}} are quantified only over the
-variables that appear in the term constructed by \texttt{\tacexpr}.
-
 \begin{Variants}
 \item \texttt{abstract {\tacexpr} using {\ident}}.\\
   Give explicitly the name of the auxiliary lemma.
@@ -1426,6 +1416,16 @@ You can also pass the {\tt -profile-ltac} command line option to {\tt coqc}, whi
 
 Note that the profiler currently does not handle backtracking into multi-success tactics, and issues a warning to this effect in many cases when such backtracking occurs.
 
+\subsection[Run-time optimization tactic]{Run-time optimization tactic\label{tactic-optimizeheap}}.
+
+The following tactic behaves like {\tt idtac}, and running it compacts the heap in the
+OCaml run-time system. It is analogous to the Vernacular command {\tt Optimize Heap} (see~\ref{vernac-optimizeheap}).
+
+\tacindex{optimize\_heap}
+\begin{quote}
+{\tt optimize\_heap}.
+\end{quote}
+
 \endinput
 
 \subsection{Permutation on closed lists}
diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex
index 3ebeba178a..bef31d3fa5 100644
--- a/doc/refman/RefMan-oth.tex
+++ b/doc/refman/RefMan-oth.tex
@@ -513,6 +513,9 @@ This command loads the file named {\ident}{\tt .v}, searching
 successively in each of the directories specified in the {\em
   loadpath}. (see Section~\ref{loadpath})
 
+Files loaded this way cannot leave proofs open, and neither the {\tt
+  Load} command can be use inside a proof.
+
 \begin{Variants}
 \item {\tt Load {\str}.}\label{Load-str}\\
   Loads the file denoted by the string {\str}, where {\str} is any
@@ -530,6 +533,8 @@ successively in each of the directories specified in the {\em
 
 \begin{ErrMsgs}
 \item \errindex{Can't find file {\ident} on loadpath}
+\item \errindex{Load is not supported inside proofs}
+\item \errindex{Files processed by Load cannot leave open proofs}
 \end{ErrMsgs}
 
 \section[Compiled files]{Compiled files\label{compiled}\index{Compiled files}}
@@ -912,6 +917,15 @@ This command turns off the use of a default timeout.
 
 This command displays whether some default timeout has be set or not.
 
+\subsection[\tt Fail \textrm{\textsl{command-or-tactic}}.]{\tt Fail \textrm{\textsl{command-or-tactic}}.\comindex{Fail}\label{Fail}}
+
+For debugging {\Coq} scripts, sometimes it is desirable to know
+whether a command or a tactic fails. If the given command or tactic
+fails, the {\tt Fail} statement succeeds, without changing the proof
+state, and in interactive mode, {\Coq} prints a message confirming the failure.
+If the command or tactic succeeds, the statement is an error, and
+{\Coq} prints a message indicating that the failure did not occur.
+
 \section{Controlling display}
 
 \subsection[\tt Set Silent.]{\tt Set Silent.\optindex{Silent}
diff --git a/doc/refman/RefMan-pre.tex b/doc/refman/RefMan-pre.tex
index 991c9745e9..05775bfbe5 100644
--- a/doc/refman/RefMan-pre.tex
+++ b/doc/refman/RefMan-pre.tex
@@ -499,7 +499,7 @@ Claude Marché coordinated the edition of the Reference Manual for
 Pierre Letouzey and Jacek Chrz\k{a}szcz respectively maintained the
 extraction tool and module system of {\Coq}.
 
-Jean-Christophe Filliâtre, Pierre Letouzey, Hugo Herbelin ando
+Jean-Christophe Filliâtre, Pierre Letouzey, Hugo Herbelin and other
 contributors from Sophia-Antipolis and Nijmegen participated to the
 extension of the library.
 
@@ -659,7 +659,7 @@ Matthieu Sozeau extended the \textsc{Russell} language, ending in an
 convenient way to write programs of given specifications, Pierre
 Corbineau extended the Mathematical Proof Language and the
 automatization tools that accompany it, Pierre Letouzey supervised and
-extended various parts the standard library, Stéphane Glondu
+extended various parts of the standard library, Stéphane Glondu
 contributed a few tactics and improvements, Jean-Marc Notin provided
 help in debugging, general maintenance and {\tt coqdoc} support,
 Vincent Siles contributed extensions of the {\tt Scheme} command and
@@ -680,7 +680,7 @@ Nicolas Tabareau made the adaptation of the interface of the old
 the interaction between Coq and its external interfaces. With Samuel
 Mimram, he also helped making Coq compatible with recent software
 tools.  Russell O'Connor, Cezary Kaliscyk, Milad Niqui contributed to
-improved the libraries of integers, rational, and real numbers. We
+improve the libraries of integers, rational, and real numbers. We
 also thank many users and partners for suggestions and feedback, in
 particular Pierre Castéran and Arthur Charguéraud, the INRIA Marelle
 team, Georges Gonthier and the INRIA-Microsoft Mathematical Components team, 
@@ -714,7 +714,7 @@ implementation of $\mathbb{N}$, $\mathbb{Z}$ or
 $\mathbb{Z}/n\mathbb{Z}$. 
 
 The main other evolutions of the library are due to Hugo Herbelin who
-made a revision of the sorting library (includingh a certified
+made a revision of the sorting library (including a certified
 merge-sort) and to Guillaume Melquiond who slightly revised and
 cleaned up the library of reals.
 
@@ -723,7 +723,7 @@ some efficiency issues and a more flexible construction of module
 types, Élie Soubiran brought a new model of name equivalence, the
 $\Delta$-equivalence, which respects as much as possible the names
 given by the users. He also designed with Pierre Letouzey a new
-convenient operator \verb!<+! for nesting functor application, what
+convenient operator \verb!<+! for nesting functor application, that
 provides a light notation for inheriting the properties of cascading
 modules.
 
diff --git a/doc/refman/RefMan-pro.tex b/doc/refman/RefMan-pro.tex
index 1d3311edc2..bd74a40d7c 100644
--- a/doc/refman/RefMan-pro.tex
+++ b/doc/refman/RefMan-pro.tex
@@ -298,15 +298,19 @@ subgoals which clutter your screen.
 \begin{Variant}
 \item {\tt Focus {\num}.}\\ 
 This focuses the attention on the $\num^{th}$ subgoal to prove.
-
 \end{Variant}
 
+\emph{This command is deprecated since 8.8: prefer the use of bullets or
+  focusing brackets instead, including {\tt {\num}: \{}}.
+
 \subsection[\tt Unfocus.]{\tt Unfocus.\comindex{Unfocus}}
 This command restores to focus the goal that were suspended by the
 last {\tt Focus} command.
 
+\emph{This command is deprecated since 8.8.}
+
 \subsection[\tt Unfocused.]{\tt Unfocused.\comindex{Unfocused}}
-Succeeds in the proof is fully unfocused, fails is there are some
+Succeeds in the proof if fully unfocused, fails if there are some
 goals out of focus.
 
 \subsection[\tt \{ \textrm{and} \}]{\tt \{ \textrm{and} \}\comindex{\{}\comindex{\}}}\label{curlybacket}
@@ -320,10 +324,19 @@ Note that when a focused goal is proved a message is displayed
 together with a suggestion about the right bullet or {\tt \}} to
 unfocus it or focus the next one.
 
+\begin{Variants}
+
+\item {\tt {\num}: \{}\\
+This focuses on the $\num^{th}$ subgoal to prove.
+
+\end{Variants}
+
 \begin{ErrMsgs}
 \item \errindex{This proof is focused, but cannot be unfocused
     this way} You are trying to use {\tt \}} but the current subproof
   has not been fully solved.
+\item \errindex{No such goal}
+\item \errindex{Brackets only support the single numbered goal selector}
 \item see also error message about bullets below.
 \end{ErrMsgs}
 
@@ -555,12 +568,12 @@ used to force Coq to optimize some of its internal data structures.
 This command forces Coq to shrink the data structure used to represent
 the ongoing proof.
 
-\subsection[\tt Optimize Heap.]{\tt Optimize Heap.}
+\subsection[\tt Optimize Heap.]{\tt Optimize Heap.\label{vernac-optimizeheap}}
 
 This command forces the OCaml runtime to perform a heap compaction.
-This is in general an expensive operation.  See:
-  \url{http://caml.inria.fr/pub/docs/manual-ocaml/libref/Gc.html#VALcompact}
-
+This is in general an expensive operation.  See: \\
+\ \url{http://caml.inria.fr/pub/docs/manual-ocaml/libref/Gc.html#VALcompact} \\
+There is also an analogous tactic {\tt optimize\_heap} (see~\ref{tactic-optimizeheap}).
 
 %%% Local Variables: 
 %%% mode: latex
diff --git a/doc/refman/RefMan-sch.tex b/doc/refman/RefMan-sch.tex
index 30724759d2..6004711235 100644
--- a/doc/refman/RefMan-sch.tex
+++ b/doc/refman/RefMan-sch.tex
@@ -127,7 +127,6 @@ conclusion is {\tt (n:nat)(even n)->(Q n)}.
 \optindex{Boolean Equality Schemes}
 \optindex{Elimination Schemes}
 \optindex{Nonrecursive Elimination Schemes}
-\optindex{Record Elimination Schemes}
 \optindex{Case Analysis Schemes}
 \optindex{Decidable Equality Schemes}
 \optindex{Rewriting Schemes}
@@ -144,7 +143,6 @@ and {\tt Record} (see~\ref{Record}) do not have an automatic
 declaration of the induction principles. It can be activated with the
 command {\tt Set Nonrecursive Elimination Schemes}. It can be
 deactivated again with {\tt Unset Nonrecursive Elimination Schemes}.
-{\tt Record Elimination Schemes} is a deprecated alias of {\tt Nonrecursive Elimination Schemes}.
 
 In addition, the {\tt Case Analysis Schemes} flag governs the generation of
 case analysis lemmas for inductive types, i.e. corresponding to the
diff --git a/doc/refman/RefMan-syn.tex b/doc/refman/RefMan-syn.tex
index eecb5ac7c0..836753db16 100644
--- a/doc/refman/RefMan-syn.tex
+++ b/doc/refman/RefMan-syn.tex
@@ -3,25 +3,32 @@
 
 In this chapter, we introduce advanced commands to modify the way
 {\Coq} parses and prints objects, i.e. the translations between the
-concrete and internal representations of terms and commands. The main
-commands are {\tt Notation} and {\tt Infix} which are described in
-section \ref{Notation}.  It also happens that the same symbolic
-notation is expected in different contexts. To achieve this form of
-overloading, {\Coq} offers a notion of interpretation scope. This is
-described in Section~\ref{scopes}.
-
-\Rem The commands {\tt Grammar}, {\tt Syntax} and {\tt Distfix} which
-were present for a while in {\Coq} are no longer available from {\Coq}
-version 8.0. The underlying AST structure is also no longer available.
-The functionalities of the command {\tt Syntactic Definition} are
-still available; see Section~\ref{Abbreviations}.
+concrete and internal representations of terms and commands.
+
+The main commands to provide custom symbolic notations for terms are
+{\tt Notation} and {\tt Infix}. They are described in Section
+\ref{Notation}. There is also a variant of {\tt Notation} which does
+not modify the parser. This provides with a form of abbreviation and
+it is described in Section~\ref{Abbreviations}. It is sometimes
+expected that the same symbolic notation has different meanings in
+different contexts. To achieve this form of overloading, {\Coq} offers
+a notion of interpretation scope. This is described in
+Section~\ref{scopes}.
+
+The main command to provide custom notations for tactics is {\tt
+  Tactic Notation}. It is described in Section~\ref{Tactic-Notation}.
+
+% No need any more to remind this
+%% \Rem The commands {\tt Grammar}, {\tt Syntax} and {\tt Distfix} which
+%% were present for a while in {\Coq} are no longer available from {\Coq}
+%% version 8.0. The underlying AST structure is also no longer available.
 
 \section[Notations]{Notations\label{Notation}
 \comindex{Notation}}
 
 \subsection{Basic notations}
 
-A {\em notation} is a symbolic abbreviation denoting some term
+A {\em notation} is a symbolic expression denoting some term
 or term pattern.
 
 A typical notation is the use of the infix symbol \verb=/\= to denote
@@ -37,7 +44,7 @@ string \verb="A /\ B"= (called a {\em notation}) tells how it is
 symbolically written.
 
 A notation is always surrounded by double quotes (except when the
-abbreviation is a single identifier; see \ref{Abbreviations}). The
+abbreviation has the form of an ordinary applicative expression; see \ref{Abbreviations}). The
 notation is composed of {\em tokens} separated by spaces.  Identifiers
 in the string (such as \texttt{A} and \texttt{B}) are the {\em
 parameters} of the notation. They must occur at least once each in the
@@ -61,7 +68,7 @@ syntactic expression (see \ref{ReservedNotation}), explicit precedences and
 associativity rules have to be given.
 
 \Rem The right-hand side of a notation is interpreted at the time the
-notation is given. In particular, implicit arguments (see
+notation is given. In particular, disambiguation of constants, implicit arguments (see
 Section~\ref{Implicit Arguments}), coercions (see
 Section~\ref{Coercions}), etc. are resolved at the time of the
 declaration of the notation.
@@ -105,8 +112,8 @@ parentheses are mandatory (this is a ``no associativity'')\footnote{
 which {\Coq} is built, namely {\camlpppp}, currently does not implement the
 no-associativity and replaces it by a left associativity; hence it is
 the same for {\Coq}: no-associativity is in fact left associativity}.
-We don't know of a special convention of the associativity of
-disjunction and conjunction, so let's apply for instance a right
+We do not know of a special convention of the associativity of
+disjunction and conjunction, so let us apply for instance a right
 associativity (which is the choice of {\Coq}).
 
 Precedence levels and associativity rules of notations have to be
@@ -142,7 +149,8 @@ Notation "x = y" := (@eq _ x y) (at level 70, no associativity).
 \end{coq_example*}
 
 One can define {\em closed} notations whose both sides are symbols. In
-this case, the default precedence level for inner subexpression is 200.
+this case, the default precedence level for inner subexpression is
+200, and the default level for the notation itself is 0.
 
 \begin{coq_eval}
 Set Printing Depth 50.
@@ -150,7 +158,7 @@ Set Printing Depth 50.
 (**** an incompatibility with the reserved notation ********)
 \end{coq_eval}
 \begin{coq_example*}
-Notation "( x , y )" := (@pair _ _ x y) (at level 0).
+Notation "( x , y )" := (@pair _ _ x y).
 \end{coq_example*}
 
 One can also define notations for binders.
@@ -161,17 +169,17 @@ Set Printing Depth 50.
 (**** an incompatibility with the reserved notation ********)
 \end{coq_eval}
 \begin{coq_example*}
-Notation "{ x : A  |  P }" := (sig A (fun x => P)) (at level 0).
+Notation "{ x : A  |  P }" := (sig A (fun x => P)).
 \end{coq_example*}
 
 In the last case though, there is a conflict with the notation for
-type casts. This last notation, as shown by the command {\tt Print Grammar
+type casts. The notation for type casts, as shown by the command {\tt Print Grammar
 constr} is at level 100. To avoid \verb=x : A= being parsed as a type cast,
 it is necessary to put {\tt x} at a level below 100, typically 99. Hence, a
-correct definition is 
+correct definition is the following.
 
 \begin{coq_example*}
-Notation "{ x : A  |  P }" := (sig A (fun x => P)) (at level 0, x at level 99).
+Notation "{ x : A  |  P }" := (sig A (fun x => P)) (x at level 99).
 \end{coq_example*}
 
 %This change has retrospectively an effect on the notation for notation
@@ -182,14 +190,17 @@ Notation "{ x : A  |  P }" := (sig A (fun x => P)) (at level 0, x at level 99).
 %Notation "{ A } + { B }" := (sumbool A B) (at level 0, A at level 99).
 %\end{coq_example*}
 
-See the next section for more about factorization.
+More generally, it is required that notations are explicitly
+factorized on the left. See the next section for more about
+factorization.
 
 \subsection{Simple factorization rules}
 
-{\Coq} extensible parsing is performed by Camlp5 which is essentially a
-LL1 parser. Hence, some care has to be taken not to hide already
-existing rules by new rules. Some simple left factorization work has
-to be done. Here is an example.
+{\Coq} extensible parsing is performed by {\camlpppp} which is
+essentially a LL1 parser: it decides which notation to parse by
+looking tokens from left to right. Hence, some care has to be taken
+not to hide already existing rules by new rules. Some simple left
+factorization work has to be done. Here is an example.
 
 \begin{coq_eval}
 (********** The next rule for notation _ < _ < _  produces **********)
@@ -242,17 +253,19 @@ on the {\Coq} printer. For example:
 Check (and True True).
 \end{coq_example}
 
-However, printing, especially pretty-printing, requires
-more care than parsing. We may want specific indentations,
-line breaks, alignment if on several lines, etc. 
+However, printing, especially pretty-printing, also requires some
+care. We may want specific indentations, line breaks, alignment if on
+several lines, etc. For pretty-printing, {\Coq} relies on {\ocaml}
+formatting library, which provides indentation and automatic line
+breaks depending on page width by means of {\em formatting boxes}.
 
-The default printing of notations is very rudimentary. For printing a
-notation, a {\em formatting box} is opened in such a way that if the
+The default printing of notations is rudimentary. For printing a
+notation, a formatting box is opened in such a way that if the
 notation and its arguments cannot fit on a single line, a line break
 is inserted before the symbols of the notation and the arguments on
 the next lines are aligned with the argument on the first line.
 
-A first, simple control that a user can have on the printing of a
+A first simple control that a user can have on the printing of a
 notation is the insertion of spaces at some places of the
 notation. This is performed by adding extra spaces between the symbols
 and parameters: each extra space (other than the single space needed
@@ -277,6 +290,13 @@ Notation "'If' c1 'then' c2 'else' c3" := (IF_then_else c1 c2 c3)
 \end{coq_example}
 \end{small}
 
+\begin{coq_example}
+Check
+ (IF_then_else (IF_then_else True False True)
+   (IF_then_else True False True)
+   (IF_then_else True False True)).
+\end{coq_example}
+
 A {\em format} is an extension of the string denoting the notation with
 the possible following elements delimited by single quotes:
 
@@ -313,22 +333,15 @@ Notations do not survive the end of sections. No typing of the denoted
 expression is performed at definition time. Type-checking is done only
 at the time of use of the notation.
 
-\begin{coq_example}
-Check 
- (IF_then_else (IF_then_else True False True) 
-   (IF_then_else True False True)
-   (IF_then_else True False True)).   
-\end{coq_example}
-
 \Rem
 Sometimes, a notation is expected only for the parser.
 %(e.g. because
 %the underlying parser of {\Coq}, namely {\camlpppp}, is LL1 and some extra
 %rules are needed to circumvent the absence of factorization).
-To do so, the option {\em only parsing} is allowed in the list of modifiers of
+To do so, the option {\tt only parsing} is allowed in the list of modifiers of
 \texttt{Notation}.
 
-Conversely, the {\em only printing} can be used to declare
+Conversely, the {\tt only printing} can be used to declare
 that a notation should only be used for printing and should not declare a
 parsing rule. In particular, such notations do not modify the parser.
 
@@ -339,16 +352,16 @@ The \texttt{Infix} command is a shortening for declaring notations of
 infix symbols. Its syntax is 
 
 \begin{quote}
-\noindent\texttt{Infix "{\symbolentry}" :=} {\qualid} {\tt (} \nelist{\em modifier}{,} {\tt )}.
+\noindent\texttt{Infix "{\symbolentry}" :=} {\term} {\tt (} \nelist{\em modifier}{,} {\tt )}.
 \end{quote}
 
 and it is equivalent to
 
 \begin{quote}
-\noindent\texttt{Notation "x {\symbolentry} y" := ({\qualid} x y)  (} \nelist{\em modifier}{,} {\tt )}.
+\noindent\texttt{Notation "x {\symbolentry} y" := ({\term} x y)  (} \nelist{\em modifier}{,} {\tt )}.
 \end{quote}
 
-where {\tt x} and {\tt y} are fresh names distinct from {\qualid}. Here is an example.
+where {\tt x} and {\tt y} are fresh names. Here is an example.
 
 \begin{coq_example*}
 Infix "/\" := and (at level 80, right associativity).
@@ -380,12 +393,14 @@ reserved. Hence their precedence and associativity cannot be changed.
 \comindex{CoFixpoint {\ldots} where {\ldots}}
 \comindex{Inductive {\ldots} where {\ldots}}}
 
-Thanks to reserved notations, the inductive, co-inductive, recursive
-and corecursive definitions can benefit of customized notations. To do
-this, insert a {\tt where} notation clause after the definition of the
-(co)inductive type or (co)recursive term (or after the definition of
-each of them in case of mutual definitions). The exact syntax is given
-on Figure~\ref{notation-syntax}. Here are examples:
+Thanks to reserved notations, the inductive, co-inductive, record,
+recursive and corecursive definitions can benefit of customized
+notations. To do this, insert a {\tt where} notation clause after the
+definition of the (co)inductive type or (co)recursive term (or after
+the definition of each of them in case of mutual definitions). The
+exact syntax is given on Figure~\ref{notation-syntax} for inductive,
+co-inductive, recursive and corecursive definitions and on
+Figure~\ref{record-syntax} for records. Here are examples:
 
 \begin{coq_eval}
 Set Printing Depth 50.
@@ -479,20 +494,28 @@ Locate "exists _ .. _ , _".
 \\
 \\
 {\modifiers}
-  & ::= & \nelist{\ident}{,} {\tt at level} {\naturalnumber} \\
-  & $|$ & \nelist{\ident}{,} {\tt at next level} \\
-  & $|$ & {\tt at level} {\naturalnumber} \\
-  & $|$ & {\tt left associativity} \\
-  & $|$ & {\tt right associativity} \\
-  & $|$ & {\tt no associativity} \\
+  & ::= & {\tt at level} {\naturalnumber} \\
+  & $|$ & \nelist{\ident}{,} {\tt at level} {\naturalnumber} \zeroone{\binderinterp}\\
+  & $|$ & \nelist{\ident}{,} {\tt at next level} \zeroone{\binderinterp}\\
+  & $|$ & {\ident} {\binderinterp} \\
   & $|$ & {\ident} {\tt ident} \\
-  & $|$ & {\ident} {\tt binder} \\
-  & $|$ & {\ident} {\tt closed binder} \\
   & $|$ & {\ident} {\tt global} \\
   & $|$ & {\ident} {\tt bigint} \\
+  & $|$ & {\ident} \zeroone{{\tt strict}} {\tt pattern} \zeroone{{\tt at level} {\naturalnumber}}\\
+  & $|$ & {\ident} {\tt binder} \\
+  & $|$ & {\ident} {\tt closed binder} \\
+  & $|$ & {\tt left associativity} \\
+  & $|$ & {\tt right associativity} \\
+  & $|$ & {\tt no associativity} \\
   & $|$ & {\tt only parsing} \\
   & $|$ & {\tt only printing} \\
-  & $|$ & {\tt format} {\str} 
+  & $|$ & {\tt format} {\str} \\
+\\
+\\
+{\binderinterp}
+  & ::= & {\tt as ident} \\
+  & $|$ & {\tt as pattern} \\
+  & $|$ & {\tt as strict pattern} \\
 \end{tabular}
 \end{centerframe}
 \end{small}
@@ -500,9 +523,93 @@ Locate "exists _ .. _ , _".
 \label{notation-syntax}
 \end{figure}
 
-\subsection{Notations and simple binders}
+\subsection{Notations and binders}
+
+Notations can include binders. This section lists
+different ways to deal with binders. For further examples, see also
+Section~\ref{RecursiveNotationsWithBinders}.
+
+\subsubsection{Binders bound in the notation and parsed as identifiers}
 
-Notations can be defined for binders as in the example:
+Here is the basic example of a notation using a binder:
+
+\begin{coq_example*}
+Notation "'sigma' x : A , B" := (sigT (fun x : A => B))
+  (at level 200, x ident, A at level 200, right associativity).
+\end{coq_example*}
+
+The binding variables in the right-hand side that occur as a parameter
+of the notation (here {\tt x}) dynamically bind all the occurrences
+in their respective binding scope after instantiation of the
+parameters of the notation. This means that the term bound to {\tt B} can
+refer to the variable name bound to {\tt x} as shown in the following
+application of the notation:
+
+\begin{coq_example}
+Check sigma z : nat, z = 0.
+\end{coq_example}
+
+Notice the modifier {\tt x ident} in the declaration of the
+notation. It tells to parse {\tt x} as a single identifier.
+
+\subsubsection{Binders bound in the notation and parsed as patterns}
+
+In the same way as patterns can be used as binders, as in {\tt fun
+  '(x,y) => x+y} or {\tt fun '(existT \_ x \_) => x}, notations can be
+defined so that any pattern (in the sense of the entry {\pattern} of
+Figure~\ref{term-syntax-aux}) can be used in place of the
+binder. Here is an example:
+
+\begin{coq_eval}
+Reset Initial.
+\end{coq_eval}
+
+\begin{coq_example*}
+Notation "'subset' ' p , P " := (sig (fun p => P))
+  (at level 200, p pattern, format "'subset'  ' p ,  P").
+\end{coq_example*}
+
+\begin{coq_example}
+Check subset '(x,y), x+y=0.
+\end{coq_example}
+
+The modifier {\tt p pattern} in the declaration of the notation
+tells to parse $p$ as a pattern. Note that a single
+variable is both an identifier and a pattern, so, e.g., the following
+also works:
+
+% Note: we rely on the notation of the standard library which does not
+% print the expected output, so we hide the output.
+\begin{coq_example}
+Check subset 'x, x=0.
+\end{coq_example}
+
+If one wants to prevent such a notation to be used for printing when the
+pattern is reduced to a single identifier, one has to use instead
+the modifier {\tt p strict pattern}. For parsing, however, a {\tt
+  strict pattern} will continue to include the case of a
+variable. Here is an example showing the difference:
+
+\begin{coq_example*}
+Notation "'subset_bis' ' p , P" := (sig (fun p => P))
+  (at level 200, p strict pattern).
+Notation "'subset_bis' p , P " := (sig (fun p => P))
+  (at level 200, p ident).
+\end{coq_example*}
+
+\begin{coq_example}
+Check subset_bis 'x, x=0.
+\end{coq_example}
+
+The default level for a {\tt pattern} is 0. One can use a different level by
+using {\tt pattern at level} $n$ where the scale is the same as the one for
+terms (Figure~\ref{init-notations}).
+
+\subsubsection{Binders bound in the notation and parsed as terms}
+
+Sometimes, for the sake of factorization of rules, a binder has to be
+parsed as a term. This is typically the case for a notation such as
+the following:
 
 \begin{coq_eval}
 Set Printing Depth 50.
@@ -510,18 +617,53 @@ Set Printing Depth 50.
 (**** an incompatibility with the reserved notation ********)
 \end{coq_eval}
 \begin{coq_example*}
-Notation "{ x : A  |  P  }" := (sig (fun x : A => P)) (at level 0).
+Notation "{ x : A  |  P  }" := (sig (fun x : A => P))
+  (at level 0, x at level 99 as ident).
+\end{coq_example*}
+
+This is so because the grammar also contains rules starting with
+{\tt \{} and followed by a term, such as the rule for the notation
+  {\tt \{ A \} + \{ B \}} for the constant {\tt
+    sumbool}~(see Section~\ref{sumbool}).
+
+Then, in the rule, {\tt x ident} is replaced by {\tt x at level 99 as
+  ident} meaning that {\tt x} is parsed as a term at level 99 (as done
+in the notation for {\tt sumbool}), but that this term has actually to
+be an identifier.
+
+The notation {\tt \{ x | P \}} is already defined in the standard
+library with the {\tt as ident} modifier. We cannot redefine it but
+one can define an alternative notation, say {\tt \{ p such that P }\},
+using instead {\tt as pattern}.
+
+% Note, this conflicts with the default rule in the standard library, so
+% we don't show the
+\begin{coq_example*}
+Notation "{ p 'such' 'that' P }" := (sig (fun p => P))
+  (at level 0, p at level 99 as pattern).
 \end{coq_example*}
 
-The binding variables in the left-hand-side that occur as a parameter
-of the notation naturally bind all their occurrences appearing in
-their respective scope after instantiation of the parameters of the
-notation.
+Then, the following works:
+\begin{coq_example}
+Check {(x,y) such that x+y=0}.
+\end{coq_example}
+
+To enforce that the pattern should not be used for printing when it
+is just an identifier, one could have said {\tt p at level
+  99 as strict pattern}.
+
+Note also that in the absence of a {\tt as ident}, {\tt as strict
+  pattern} or {\tt as pattern} modifiers, the default is to consider
+subexpressions occurring in binding position and parsed as terms to be
+{\tt as ident}.
+
+\subsubsection{Binders not bound in the notation}
+\label{NotationsWithBinders}
 
-Contrastingly, the binding variables that are not a parameter of the
-notation do not capture the variables of same name that
-could appear in their scope after instantiation of the
-notation. E.g., for the notation
+We can also have binders in the right-hand side of a notation which
+are not themselves bound in the notation. In this case, the binders
+are considered up to renaming of the internal binder. E.g., for the
+notation
 
 \begin{coq_example*}
 Notation "'exists_different' n" := (exists p:nat, p<>n) (at level 200).
@@ -537,14 +679,6 @@ Set Printing Depth 50.
 Fail Check (exists_different p).
 \end{coq_example}
 
-\Rem Binding variables must not necessarily be parsed using the
-{\tt ident} entry. For factorization purposes, they can be said to be
-parsed at another level (e.g. {\tt x} in \verb="{ x : A | P }"= must be
-parsed at level 99 to be factorized with the notation
-\verb="{ A } + { B }"= for which {\tt A} can be any term).  
-However, even if parsed as a term, this term must at the end be effectively 
-a single identifier.
-
 \subsection{Notations with recursive patterns}
 \label{RecursiveNotations}
 
@@ -565,24 +699,22 @@ notation parses any number of time (but at least one time) a sequence
 of expressions separated by the sequence of tokens $s$ (in the
 example, $s$ is just ``{\tt ;}'').
 
-In the right-hand side, the term enclosed within {\tt ..} must be a
-pattern with two holes of the form $\phi([~]_E,[~]_I)$ where the first
-hole is occupied either by $x$ or by $y$ and the second hole is
-occupied by an arbitrary term $t$ called the {\it terminating}
-expression of the recursive notation. The subterm {\tt ..} $\phi(x,t)$
-{\tt ..} (or {\tt ..} $\phi(y,t)$ {\tt ..})  must itself occur at
-second position of the same pattern where the first hole is occupied
-by the other variable, $y$ or $x$. Otherwise said, the right-hand side
-must contain a subterm of the form either $\phi(x,${\tt ..}
-$\phi(y,t)$ {\tt ..}$)$ or $\phi(y,${\tt ..}  $\phi(x,t)$ {\tt ..}$)$.
-The pattern $\phi$ is the {\em iterator} of the recursive notation
-and, of course, the name $x$ and $y$ can be chosen arbitrarily.
-
-The parsing phase produces a list of expressions which are used to
-fill in order the first hole of the iterating pattern which is
+The right-hand side must contain a subterm of the form either
+$\phi(x,${\tt ..}  $\phi(y,t)$ {\tt ..}$)$ or $\phi(y,${\tt ..}
+$\phi(x,t)$ {\tt ..}$)$ where $\phi([~]_E,[~]_I)$, called the {\em
+  iterator} of the recursive notation is an arbitrary expression with
+distinguished placeholders and
+where $t$ is called the {\tt terminating expression} of the recursive
+notation. In the example, we choose the name s$x$ and $y$ but in
+practice they can of course be chosen arbitrarily. Note that the
+placeholder $[~]_I$ has to occur only once but the $[~]_E$ can occur
+several times.
+
+Parsing the notation produces a list of expressions which are used to
+fill the first placeholder of the iterating pattern which itself is
 repeatedly nested as many times as the length of the list, the second
-hole being the nesting point. In the innermost occurrence of the
-nested iterating pattern, the second hole is finally filled with the
+placeholder being the nesting point. In the innermost occurrence of the
+nested iterating pattern, the second placeholder is finally filled with the
 terminating expression.
 
 In the example above, the iterator $\phi([~]_E,[~]_I)$ is {\tt cons
@@ -609,24 +741,26 @@ notations, they can also be declared within interpretation scopes (see
 section \ref{scopes}).
 
 \subsection{Notations with recursive patterns involving binders}
+\label{RecursiveNotationsWithBinders}
 
 Recursive notations can also be used with binders. The basic example is:
 
 \begin{coq_example*}
-Notation "'exists' x .. y , p" := (ex (fun x => .. (ex (fun y => p)) ..))
+Notation "'exists' x .. y , p" :=
+  (ex (fun x => .. (ex (fun y => p)) ..))
   (at level 200, x binder, y binder, right associativity).
 \end{coq_example*}
 
 The principle is the same as in Section~\ref{RecursiveNotations}
-except that in the iterator $\phi([~]_E,[~]_I)$, the first hole is a
-placeholder occurring at the position of the binding variable of a {\tt
+except that in the iterator $\phi([~]_E,[~]_I)$, the placeholder $[~]_E$ can
+also occur in position of the binding variable of a {\tt
   fun} or a {\tt forall}.
 
 To specify that the part ``$x$ {\tt ..} $y$'' of the notation
 parses a sequence of binders, $x$ and $y$ must be marked as {\tt
-  binder} in the list of modifiers of the notation.  Then, the list of
-binders produced at the parsing phase are used to fill in the first
-hole of the iterating pattern which is repeatedly nested as many times
+  binder} in the list of modifiers of the notation. The
+binders of the parsed sequence are used to fill the occurrences of the first
+placeholder of the iterating pattern which is repeatedly nested as many times
 as the number of binders generated. If ever the generalization
 operator {\tt `} (see Section~\ref{implicit-generalization}) is used
 in the binding list, the added binders are taken into account too.
@@ -635,14 +769,14 @@ Binders parsing exist in two flavors. If $x$ and $y$ are marked as
 {\tt binder}, then a sequence such as {\tt a b c : T} will be accepted
 and interpreted as the sequence of binders {\tt (a:T) (b:T)
   (c:T)}. For instance, in the notation above, the syntax {\tt exists
-  a b : nat, a = b} is provided.
+  a b : nat, a = b} is valid.
 
 The variables $x$ and $y$ can also be marked as {\tt closed binder} in
 which case only well-bracketed binders of the form {\tt (a b c:T)} or
 {\tt \{a b c:T\}} etc. are accepted.
 
 With closed binders, the recursive sequence in the left-hand side can
-be of the general form $x$ $s$ {\tt ..} $s$ $y$ where $s$ is an
+be of the more general form $x$ $s$ {\tt ..} $s$ $y$ where $s$ is an
 arbitrary sequence of tokens. With open binders though, $s$ has to be
 empty. Here is an example of recursive notation with closed binders:
 
@@ -661,6 +795,40 @@ Notation "'FUNAPP' x .. y , f" :=
   (at level 200, x binder, y binder, right associativity).
 \end{coq_example*}
 
+If an occurrence of the $[~]_E$ is not in position of a binding
+variable but of a term, it is the name used in the binding which is
+used. Here is an example:
+
+\begin{coq_example*}
+Notation "'exists_non_null' x .. y  , P" :=
+  (ex (fun x => x <> 0 /\ .. (ex (fun y => y <> 0 /\ P)) ..))
+  (at level 200, x binder).
+\end{coq_example*}
+
+\subsection{Predefined entries}
+
+By default, sub-expressions are parsed as terms and the corresponding
+grammar entry is called {\tt constr}. However, one may sometimes want
+to restrict the syntax of terms in a notation. For instance, the
+following notation will accept to parse only global reference in
+position of {\tt x}:
+
+\begin{coq_example*}
+Notation "'apply' f a1 .. an" := (.. (f a1) .. an)
+  (at level 10, f global, a1, an at level 9).
+\end{coq_example*}
+
+In addition to {\tt global}, one can restrict the syntax of a
+sub-expression by using the entry names {\tt ident} or {\tt pattern}
+already seen in Section~\ref{NotationsWithBinders}, even when the
+corresponding expression is not used as a binder in the right-hand
+side. E.g.:
+
+\begin{coq_example*}
+Notation "'apply_id' f a1 .. an" := (.. (f a1) .. an)
+  (at level 10, f ident, a1, an at level 9).
+\end{coq_example*}
+
 \subsection{Summary}
 
 \paragraph{Syntax of notations}
@@ -754,7 +922,7 @@ stack by using the command
 {\tt Close Scope} {\scope}.
 \end{quote}
 Notice that this command does not only cancel the last {\tt Open Scope
-{\scope}} but all the invocation of it.
+{\scope}} but all the invocations of it.
 
 \Rem {\tt Open Scope} and {\tt Close Scope} do not survive the end of
 sections where they occur. When defined outside of a section, they are
@@ -853,6 +1021,14 @@ Arguments scopes can be cleared with the following command:
 {\tt Arguments {\qualid} : clear scopes}
 \end{quote}
 
+Extra argument scopes, to be used in case of coercion to Funclass
+(see Chapter~\ref{Coercions-full}) or with a computed type,
+can be given with
+
+\begin{quote}
+{\tt Arguments} {\qualid} \nelist{\textunderscore {\tt \%} \scope}{} {\tt : extra scopes.}
+\end{quote}
+
 \begin{Variants}
 \item {\tt Global Arguments} {\qualid} \nelist{\name {\tt \%}\scope}{}
 
@@ -1108,7 +1284,7 @@ Check reflexive iff.
 \end{coq_example}
 
 An abbreviation expects no precedence nor associativity, since it
-follows the usual syntax of application. Abbreviations are used as
+is parsed as usual application. Abbreviations are used as
 much as possible by the {\Coq} printers unless the modifier
 \verb=(only parsing)= is given.
 
@@ -1121,7 +1297,7 @@ abbreviation but at the time it is used. Especially, abbreviations can
 be bound to terms with holes (i.e. with ``\_''). The general syntax
 for abbreviations is
 \begin{quote}
-\zeroone{{\tt Local}} \texttt{Notation} {\ident} \sequence{\ident} {\ident} \texttt{:=} {\term} 
+\zeroone{{\tt Local}} \texttt{Notation} {\ident} \sequence{\ident}{} \texttt{:=} {\term}
  \zeroone{{\tt (only parsing)}}~\verb=.=
 \end{quote}
 
@@ -1147,13 +1323,15 @@ at the time of use of the abbreviation.
 %\verb=(only parsing)= is given) while syntactic definitions were not.
 
 \section{Tactic Notations
+\label{Tactic-Notation}
 \comindex{Tactic Notation}}
 
 Tactic notations allow to customize the syntax of the tactics of the
-tactic language\footnote{Tactic notations are just a simplification of
-the {\tt Grammar tactic simple\_tactic} command that existed in
-versions prior to version 8.0.}. Tactic notations obey the following
-syntax
+tactic language.
+%% \footnote{Tactic notations are just a simplification of
+%% the {\tt Grammar tactic simple\_tactic} command that existed in
+%% versions prior to version 8.0.}
+Tactic notations obey the following syntax:
 \medskip
 
 \noindent
@@ -1196,7 +1374,9 @@ level indicates the parsing precedence of the tactic notation. This
 information is particularly relevant for notations of tacticals.
 Levels 0 to 5 are available (default is 0). 
 To know the parsing precedences of the
-existing tacticals, use the command {\tt Print Grammar tactic.}
+existing tacticals, use the command
+\comindex{Print Grammar tactic}
+ {\tt Print Grammar tactic.}
 
 Each type of tactic argument has a specific semantic regarding how it
 is parsed and how it is interpreted. The semantic is described in the
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 66a5f107a5..40ba43b6cd 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -2904,7 +2904,7 @@ This happens if \term$_1$ does not occur in the goal.
       rewrite H in H2 at - 2}. In particular a failure will happen if any of
     these three simpler tactics fails.
   \item \texttt{rewrite H in * |- } will do \texttt{rewrite H in
-      H$_i$} for all hypothesis \texttt{H$_i$ <> H}. A success will happen
+      H$_i$} for all hypotheses \texttt{H$_i$} different from \texttt{H}. A success will happen
     as soon as at least one of these simpler tactics succeeds.
   \item \texttt{rewrite H in *} is a combination of \texttt{rewrite H}
     and \texttt{rewrite H in * |-} that succeeds if at
@@ -3611,7 +3611,7 @@ $\beta$-expansion (the inverse of $\bt$-reduction) of the current goal
 \item applying the abstracted goal to {\term}
 \end{enumerate}
 
-For instance, if the current goal $T$ is expressible has $\phi(t)$
+For instance, if the current goal $T$ is expressible as $\phi(t)$
 where the notation captures all the instances of $t$ in $\phi(t)$,
 then {\tt pattern $t$} transforms it into {\tt (fun x:$A$ => $\phi(${\tt
 x}$)$) $t$}.  This command can be used, for instance, when the tactic
@@ -4589,7 +4589,6 @@ incompatibilities.
 \end{Variants}
 
 \optindex{Intuition Negation Unfolding}
-\optindex{Intuition Iff Unfolding}
 
 Some aspects of the tactic {\tt intuition} can be
 controlled using options. To avoid that inner negations which do not
@@ -4609,17 +4608,6 @@ To do that all negations of the goal are unfolded even inner ones
 To avoid that inner occurrence of {\tt iff} which do not need to be
 unfolded are unfolded (this is the default), use:
 
-\begin{quote}
-{\tt Unset Intuition Iff Unfolding}
-\end{quote}
-
-To do that all negations of the goal are unfolded even inner ones
-(this is the default), use:
-
-\begin{quote}
-{\tt Set Intuition Iff Unfolding}
-\end{quote}
-
 % En attente d'un moyen de valoriser les fichiers de demos
 %\SeeAlso file \texttt{contrib/Rocq/DEMOS/Demo\_tauto.v}
 
diff --git a/doc/refman/Universes.tex b/doc/refman/Universes.tex
index a1a6a43918..6c84a1818c 100644
--- a/doc/refman/Universes.tex
+++ b/doc/refman/Universes.tex
@@ -68,6 +68,13 @@ is only valid as long as \texttt{Top.4} is strictly smaller than
 monomorphic (not universe polymorphic), so the two universes
 (in this case \texttt{Top.3} and \texttt{Top.4}) are actually global levels.
 
+When printing \texttt{pidentity}, we can see the universes it binds in
+the annotation \texttt{@\{Top.2\}}. Additionally, when \texttt{Set
+  Printing Universes} is on we print the ``universe context'' of
+\texttt{pidentity} consisting of the bound universes and the
+constraints they must verify (for \texttt{pidentity} there are no
+constraints).
+
 Inductive types can also be declared universes polymorphic on universes
 appearing in their parameters or fields. A typical example is given by
 monoids:
@@ -138,7 +145,7 @@ producing global universe constraints, one can use the
 \optindex{Polymorphic Inductive Cumulativity}
 
 Polymorphic inductive types, coinductive types, variants and records can be
-declared cumulative using the \texttt{Cumulative}. Alternatively,
+declared cumulative using the \texttt{Cumulative} prefix. Alternatively,
 there is an option \texttt{Set Polymorphic Inductive Cumulativity} which when set,
 makes all subsequent \emph{polymorphic} inductive definitions cumulative.  When set,
 inductive types and the like can be enforced to be
@@ -151,15 +158,22 @@ Polymorphic Cumulative Inductive list {A : Type} :=
 \begin{coq_example}
 Print list.
 \end{coq_example}
-When printing \texttt{list}, the part of the output of the form
-\texttt{$\mathtt{\sim}$@\{i\} <= $\mathtt{\sim}$@\{j\} iff }
-indicates the universe constraints in order to have the subtyping
-$\WTEGLECONV{\mathtt{list@\{i\}} A}{\mathtt{list@\{j\}} B}$
-(for fully applied instances of \texttt{list}) whenever $\WTEGCONV{A}{B}$.
-In the case of \texttt{list} there is no constraint!
-This also means that any two instances of \texttt{list} are convertible:
-$\WTEGCONV{\mathtt{list@\{i\}} A}{\mathtt{list@\{j\}} B}$ whenever $\WTEGCONV{A}{B}$ and
-furthermore their corresponding (when fully applied to convertible arguments) constructors.
+When printing \texttt{list}, the universe context indicates the
+subtyping constraints by prefixing the level names with symbols.
+
+Because inductive subtypings are only produced by comparing inductives
+to themselves with universes changed, they amount to variance
+information: each universe is either invariant, covariant or
+irrelevant (there are no contravariant subtypings in Coq),
+respectively represented by the symbols \texttt{=}, \texttt{+} and
+\texttt{*}.
+
+Here we see that \texttt{list} binds an irrelevant universe, so any
+two instances of \texttt{list} are convertible:
+$\WTEGCONV{\mathtt{list@\{i\}} A}{\mathtt{list@\{j\}} B}$ whenever
+$\WTEGCONV{A}{B}$ and furthermore their corresponding (when fully
+applied to convertible arguments) constructors.
+
 See Chapter~\ref{Cic} for more details on convertibility and subtyping.
 The following is an example of a record with non-trivial subtyping relation:
 \begin{coq_example*}
@@ -168,8 +182,9 @@ Polymorphic Cumulative Record packType := {pk : Type}.
 \begin{coq_example}
 Print packType.
 \end{coq_example}
-Notice that as expected, \texttt{packType@\{i\}} and \texttt{packType@\{j\}} are
-convertible if and only if \texttt{i $=$ j}.
+\texttt{packType} binds a covariant universe, i.e.
+$\WTEGCONV{\mathtt{packType@\{i\}}}{\mathtt{packType@\{j\}}}$ whenever
+\texttt{i $\leq$ j}.
 
 Cumulative inductive types, coninductive types, variants and records
 only make sense when they are universe polymorphic. Therefore, an
diff --git a/doc/refman/coqide-queries.png b/doc/refman/coqide-queries.png
index dea5626f8e..7a46ac4e68 100644
--- a/doc/refman/coqide-queries.png
+++ b/doc/refman/coqide-queries.png
diff --git a/doc/refman/coqide.png b/doc/refman/coqide.png
index a6a0f5850e..e300401c9f 100644
--- a/doc/refman/coqide.png
+++ b/doc/refman/coqide.png
diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template
index 48048b7a0f..a2739e457e 100644
--- a/doc/stdlib/index-list.html.template
+++ b/doc/stdlib/index-list.html.template
@@ -18,6 +18,7 @@ through the <tt>Require Import</tt> command.</p>
     theories/Init/Logic.v
     theories/Init/Logic_Type.v
     theories/Init/Nat.v
+    theories/Init/Decimal.v
     theories/Init/Peano.v
     theories/Init/Specif.v
     theories/Init/Tactics.v
@@ -225,6 +226,12 @@ through the <tt>Require Import</tt> command.</p>
     theories/Numbers/BinNums.v
     theories/Numbers/NumPrelude.v
     theories/Numbers/NaryFunctions.v
+    theories/Numbers/DecimalFacts.v
+    theories/Numbers/DecimalNat.v
+    theories/Numbers/DecimalPos.v
+    theories/Numbers/DecimalN.v
+    theories/Numbers/DecimalZ.v
+    theories/Numbers/DecimalString.v
     </dd>
 
     <dt> <b>&nbsp;&nbsp;NatInt</b>:
@@ -589,7 +596,6 @@ through the <tt>Require Import</tt> command.</p>
   </dt>
   <dd>
     theories/Compat/AdmitAxiom.v
-    theories/Compat/Coq85.v
     theories/Compat/Coq86.v
     theories/Compat/Coq87.v
   </dd>