diff options
Diffstat (limited to 'doc/sphinx/addendum/program.rst')
| -rw-r--r-- | doc/sphinx/addendum/program.rst | 15 |
1 files changed, 11 insertions, 4 deletions
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: |