From 29c9d9bd47d5b8cecd6a3ce038cef4302754329f Mon Sep 17 00:00:00 2001
From: Kenji Maillard
Date: Wed, 22 Apr 2020 15:35:22 +0200
Subject: [documentation] ssreflect: Abbreviations do not support scope

---
 doc/sphinx/proof-engine/ssreflect-proof-language.rst | 10 ++++++++--
 1 file changed, 8 insertions(+), 2 deletions(-)

diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
index b5d1e8bffd..28c5359a04 100644
--- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst
+++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
@@ -1624,9 +1624,15 @@ previous :token:`i_item` have been performed.
 
 The second entry in the :token:`i_view` grammar rule,
 ``/ltac:(`` :token:`tactic` ``)``, executes :token:`tactic`.
-Notations can be used to name tactics,  for example::
+Notations can be used to name tactics,  for example
 
-    Notation myop := (ltac:(some ltac code)) : ssripat_scope.
+.. coqtop:: none
+
+      Tactic Notation "my" "ltac" "code" := idtac.
+
+.. coqtop:: in warn
+
+   Notation "'myop'" := (ltac:(my ltac code)) : ssripat_scope.
 
 lets one write just ``/myop`` in the intro pattern. Note the scope
 annotation: views are interpreted opening the ``ssripat`` scope.
-- 
cgit v1.2.3