From b7415c84269b1553470216b06871def933e2f3bd Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 9 Mar 2017 13:50:22 +0100
Subject: Clarifying doc about interpretation of scopes in notations (#5386).

---
 doc/refman/RefMan-syn.tex | 28 ++++++++++++++++++++++++++++
 1 file changed, 28 insertions(+)

(limited to 'doc/refman/RefMan-syn.tex')

diff --git a/doc/refman/RefMan-syn.tex b/doc/refman/RefMan-syn.tex
index 21c39de967..b7d36ecaa3 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}}
 
@@ -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
-- 
cgit v1.2.3


From cae09e5af6cf31d96662b1b66a63c6a236a8e741 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 9 Mar 2017 15:36:42 +0100
Subject: Typo doc notations.

---
 doc/refman/RefMan-syn.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'doc/refman/RefMan-syn.tex')

diff --git a/doc/refman/RefMan-syn.tex b/doc/refman/RefMan-syn.tex
index b7d36ecaa3..61093709ec 100644
--- a/doc/refman/RefMan-syn.tex
+++ b/doc/refman/RefMan-syn.tex
@@ -303,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}:
-- 
cgit v1.2.3


From 347827ef4ea72048762c1677f37cb716109a5d9c Mon Sep 17 00:00:00 2001
From: Valentin Robert
Date: Thu, 16 Feb 2017 14:37:47 -0800
Subject: doc: fix a French-ism

---
 doc/refman/RefMan-syn.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'doc/refman/RefMan-syn.tex')

diff --git a/doc/refman/RefMan-syn.tex b/doc/refman/RefMan-syn.tex
index 21c39de967..ce662eb208 100644
--- a/doc/refman/RefMan-syn.tex
+++ b/doc/refman/RefMan-syn.tex
@@ -114,7 +114,7 @@ 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 mention {\tt next
+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}.
 
-- 
cgit v1.2.3