From 2802a98273bd1478113130a235bf406d2f7f73f5 Mon Sep 17 00:00:00 2001
From: Vincent Laporte
Date: Mon, 29 Jul 2019 13:48:06 +0000
Subject: Document changes by PR 10324

White spaces are forbidden in the “&ident” syntax for ltac2 references.
---
 doc/sphinx/proof-engine/ltac2.rst | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

(limited to 'doc/sphinx/proof-engine')

diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst
index ceaa2775bf..80950966e4 100644
--- a/doc/sphinx/proof-engine/ltac2.rst
+++ b/doc/sphinx/proof-engine/ltac2.rst
@@ -427,6 +427,8 @@ In general, quotations can be introduced in terms using the following syntax, wh
 .. prodn::
    ltac2_term += @ident : ( @quotentry )
 
+.. _ltac2_built-in-quotations:
+
 Built-in quotations
 +++++++++++++++++++
 
@@ -439,10 +441,11 @@ The current implementation recognizes the following built-in quotations:
   holes at runtime (type ``Init.constr`` as well).
 - ``pattern``, which parses Coq patterns and produces a pattern used for term
   matching (type ``Init.pattern``).
-- ``reference``, which parses either a :n:`@qualid` or :n:`& @ident`. Qualified names
+- ``reference``, which parses either a :n:`@qualid` or :n:`&@ident`. Qualified names
   are globalized at internalization into the corresponding global reference,
   while ``&id`` is turned into ``Std.VarRef id``. This produces at runtime a
-  ``Std.reference``.
+  ``Std.reference``. There shall be no white space between the ampersand
+  symbol (``&``) and the identifier (:n:`@ident`).
 
 The following syntactic sugar is provided for two common cases.
 
-- 
cgit v1.2.3