From ca42305f1ed1699065cffdef7d96bf5fcc0069be Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Sat, 14 Nov 2020 18:44:57 +0100
Subject: Review commit: improving the doc of boolean attributes.

---
 doc/sphinx/addendum/program.rst | 8 ++++----
 1 file changed, 4 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 298ea4b4ab..104f84a253 100644
--- a/doc/sphinx/addendum/program.rst
+++ b/doc/sphinx/addendum/program.rst
@@ -99,15 +99,15 @@ coercions.
 
    Enables the program mode, in which 1) typechecking allows subset coercions and
    2) the elaboration of pattern matching of :cmd:`Fixpoint` and
-   :cmd:`Definition` act as if the :attr:`program` attribute had been
+   :cmd:`Definition` acts as if the :attr:`program` attribute has been
    used, generating obligations if there are unresolved holes after
    typechecking.
 
-.. attr:: program
+.. attr:: program{? = {| yes | no } }
    :name: program; Program
 
-   Allows using the Program mode on a specific
-   definition.  An alternative syntax is to use the legacy ``Program``
+   This :term:`boolean attribute` allows using or disabling the Program mode on a specific
+   definition.  An alternative and commonly used syntax is to use the legacy ``Program``
    prefix (cf. :n:`@legacy_attr`) as it is elsewhere in this chapter.
 
 .. _syntactic_control:
-- 
cgit v1.2.3