From 2c785aaab9b54b3d3406e7e021de635247f6535c Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Wed, 18 Mar 2020 18:36:10 +0100
Subject: Document all the existing attributes.

And fix documentation following the removal of the Template Check flag
in #11546.
---
 doc/sphinx/addendum/program.rst | 15 +++++++++++----
 1 file changed, 11 insertions(+), 4 deletions(-)

(limited to 'doc/sphinx/addendum/program.rst')

diff --git a/doc/sphinx/addendum/program.rst b/doc/sphinx/addendum/program.rst
index 549249d25c..cbb5c0db8a 100644
--- a/doc/sphinx/addendum/program.rst
+++ b/doc/sphinx/addendum/program.rst
@@ -98,10 +98,17 @@ coercions.
 .. flag:: Program Mode
 
    Enables the program mode, in which 1) typechecking allows subset coercions and
-   2) the elaboration of pattern matching of :cmd:`Program Fixpoint` and
-   :cmd:`Program Definition` act
-   like Program Fixpoint/Definition, generating obligations if there are
-   unresolved holes after typechecking.
+   2) the elaboration of pattern matching of :cmd:`Fixpoint` and
+   :cmd:`Definition` act as if the :attr:`program` attribute had been
+   used, generating obligations if there are unresolved holes after
+   typechecking.
+
+.. attr:: program
+
+   This attribute allows to use the Program mode on a specific
+   definition.  An alternative syntax is to use the legacy ``Program``
+   prefix (cf. :n:`@legacy_attr`) as documented in the rest of this
+   chapter.
 
 .. _syntactic_control:
 
-- 
cgit v1.2.3