6 files changed, 38 insertions, 12 deletions
diff --git a/doc/refman/RefMan-com.tex b/doc/refman/RefMan-com.tex
index bef0a1686f..45230fb6e5 100644
--- a/doc/refman/RefMan-com.tex
+++ b/doc/refman/RefMan-com.tex
@@ -123,12 +123,6 @@ The following command-line options are recognized by the commands {\tt
   valid for {\tt coqc} as the toplevel module name is inferred from the
   name of the output file.
 
-\item[{\tt -notop}]\ %
-
-  Use the empty logical path for the toplevel module name instead of {\tt
-    Top}. Not valid for {\tt coqc} as the toplevel module name is
-  inferred from the name of the output file.
-
 \item[{\tt -exclude-dir} {\em directory}]\ %
 
   Exclude any subdirectory named {\em directory} while
diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex
index b475a5233c..1d423f8b16 100644
--- a/doc/refman/RefMan-ext.tex
+++ b/doc/refman/RefMan-ext.tex
@@ -991,7 +991,7 @@ but library file names based on other roots can be obtained by using
 {\Coq} commands ({\tt coqc}, {\tt coqtop}, {\tt coqdep}, \dots) options
 {\tt -Q} or {\tt -R} (see Section~\ref{coqoptions}). Also, when an
 interactive {\Coq} session starts, a library of root {\tt Top} is
-started, unless option {\tt -top} or {\tt -notop} is set (see
+started, unless option {\tt -top} is set (see
 Section~\ref{coqoptions}).
 
 \subsection{Qualified names
diff --git a/doc/refman/RefMan-pro.tex b/doc/refman/RefMan-pro.tex
index c37367de5b..16c822b6a5 100644
--- a/doc/refman/RefMan-pro.tex
+++ b/doc/refman/RefMan-pro.tex
@@ -477,15 +477,15 @@ names.
 \item{\tt Show Intro.}\comindex{Show Intro}\\
 If the current goal begins by at least one product, this command
 prints the name of the first product, as it would be generated by 
-an anonymous {\tt Intro}. The aim of this command is to ease the
+an anonymous {\tt intro}. The aim of this command is to ease the
 writing of more robust scripts. For example, with an appropriate 
 {\ProofGeneral} macro, it is possible to transform any anonymous {\tt
-  Intro} into a qualified one such as {\tt Intro y13}.
+  intro} into a qualified one such as {\tt intro y13}.
 In the case of a non-product goal, it prints nothing. 
 
 \item{\tt Show Intros.}\comindex{Show Intros}\\
 This command is similar to the previous one, it simulates the naming 
-process of an {\tt Intros}.
+process of an {\tt intros}.
 
 \item{\tt Show Existentials.\label{ShowExistentials}}\comindex{Show Existentials}
 \\ It displays
diff --git a/doc/refman/RefMan-syn.tex b/doc/refman/RefMan-syn.tex
index 21c39de967..61093709ec 100644
--- a/doc/refman/RefMan-syn.tex
+++ b/doc/refman/RefMan-syn.tex
@@ -59,6 +59,12 @@ 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, 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}}
 
@@ -297,7 +303,7 @@ the possible following elements delimited by single quotes:
   of each newline
 \end{itemize}
 
-Thus, for the previous example, we get
+%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}:
@@ -908,6 +914,28 @@ 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
diff --git a/doc/refman/RefMan-tus.tex b/doc/refman/RefMan-tus.tex
index 3e29886762..797b0adedd 100644
--- a/doc/refman/RefMan-tus.tex
+++ b/doc/refman/RefMan-tus.tex
@@ -1012,7 +1012,7 @@ the different kinds of errors used in \Coq{} :
 
 \fun{val Std.error : string -> 'a}
     {For simple error messages}
-\fun{val Std.errorlabstrm : string -> std\_ppcmds -> 'a}
+\fun{val Std.user_err : ?loc:Loc.t -> string -> std\_ppcmds -> 'a}
     {See Section~\ref{PrettyPrinter} : this can be used if the user
       want to display a term or build a complex error message}
 
diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template
index 9216c81fcd..aeb0de48a3 100644
--- a/doc/stdlib/index-list.html.template
+++ b/doc/stdlib/index-list.html.template
@@ -46,6 +46,7 @@ through the <tt>Require Import</tt> command.</p>
     theories/Logic/ClassicalDescription.v
     theories/Logic/ClassicalEpsilon.v
     theories/Logic/ClassicalUniqueChoice.v
+    theories/Logic/SetoidChoice.v
     theories/Logic/Berardi.v
     theories/Logic/Diaconescu.v
     theories/Logic/Hurkens.v
@@ -55,7 +56,10 @@ through the <tt>Require Import</tt> command.</p>
     theories/Logic/Description.v
     theories/Logic/Epsilon.v
     theories/Logic/IndefiniteDescription.v
+    theories/Logic/PropExtensionality.v
+    theories/Logic/PropExtensionalityFacts.v
     theories/Logic/FunctionalExtensionality.v
+    theories/Logic/ExtensionalFunctionRepresentative.v
     theories/Logic/ExtensionalityFacts.v
     theories/Logic/WeakFan.v
     theories/Logic/WKL.v