From bfae260f7ba026e17e0cc599b8507bd133c4edc0 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Fri, 22 Nov 2019 10:40:40 +0100
Subject: [CS] support #[local] attribute

---
 doc/sphinx/language/gallina-extensions.rst | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

(limited to 'doc/sphinx')

diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst
index ae0afc7819..8caa289a47 100644
--- a/doc/sphinx/language/gallina-extensions.rst
+++ b/doc/sphinx/language/gallina-extensions.rst
@@ -2003,10 +2003,11 @@ applied to an unknown structure instance (an implicit argument) and a
 value. The complete documentation of canonical structures can be found
 in :ref:`canonicalstructures`; here only a simple example is given.
 
-.. cmd:: Canonical {? Structure } @qualid
+.. cmd:: {? Local | #[local] } Canonical {? Structure } @qualid
 
    This command declares :token:`qualid` as a canonical instance of a
-   structure (a record).
+   structure (a record). When the :g:`#[local]` attribute is given the effect
+   stops at the end of the :g:`Section` containig it.
 
    Assume that :token:`qualid` denotes an object ``(Build_struct`` |c_1| … |c_n| ``)`` in the
    structure :g:`struct` of which the fields are |x_1|, …, |x_n|.
@@ -2069,7 +2070,7 @@ in :ref:`canonicalstructures`; here only a simple example is given.
 
       See :ref:`canonicalstructures` for a more realistic example.
 
-   .. cmdv:: Canonical {? Structure } @ident {? : @type } := @term
+   .. cmdv:: {? Local | #[local] } Canonical {? Structure } @ident {? : @type } := @term
 
       This is equivalent to a regular definition of :token:`ident` followed by the
       declaration :n:`Canonical @ident`.
-- 
cgit v1.2.3