aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorThéo Zimmermann2018-12-13 15:56:03 +0100
committerThéo Zimmermann2018-12-13 15:56:03 +0100
commit018c9472f1886e4701e445a5b65d4a0e9497ce2d (patch)
tree63117b888aab8681616c9bd5625195f90d3537e9
parent228f0d929bb5098d58cd285fde42bb08d70c6ee8 (diff)
parent2b9b32e9bba480811361b65d34ac12b3998a468e (diff)
Merge PR #9211: Fixing incorrect mention of coercions as being part of the interning phase
-rw-r--r--doc/sphinx/user-extensions/syntax-extensions.rst2
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst
index a54da6faf2..47afa5ba0c 100644
--- a/doc/sphinx/user-extensions/syntax-extensions.rst
+++ b/doc/sphinx/user-extensions/syntax-extensions.rst
@@ -70,7 +70,7 @@ associativity rules have to be given.
The right-hand side of a notation is interpreted at the time the notation is
given. In particular, disambiguation of constants, :ref:`implicit arguments
- <ImplicitArguments>`, :ref:`coercions <Coercions>`, etc. are resolved at the
+ <ImplicitArguments>` and other notations are resolved at the
time of the declaration of the notation.
Precedences and associativity