aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx/user-extensions
diff options
context:
space:
mode:
authorJim Fehrle2019-08-05 15:10:32 -0700
committerJim Fehrle2019-11-20 08:53:00 -0800
commitb4eca882b6692b6374dfff8517f9f5a5cc4970f5 (patch)
treeed72a4b0a4cc67c4a988349fb28e0600e7f03ea7 /doc/sphinx/user-extensions
parent4aa756934eb37c6b6d70eddf2b46871bb8ff0956 (diff)
Update grammar in the Terms section of Gallina chapter
Update doc_grammar tool The grammar in the doc is generated semi-automatically with doc_grammar: - the grammar is automatically extracted from the mlg files - developer-prepared editing scripts *.mlg_edit modify the extracted grammar for clarity, simplicity and ordering of productions - chunks of the resulting grammar are automatically inserted into the rsts using instructions embedded in the rsts Running doc_grammar is currently a manual step. The grammar updates in the rst files have been manually reviewed.
Diffstat (limited to 'doc/sphinx/user-extensions')
-rw-r--r--doc/sphinx/user-extensions/syntax-extensions.rst2
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst
index 02910e603a..dbe714c388 100644
--- a/doc/sphinx/user-extensions/syntax-extensions.rst
+++ b/doc/sphinx/user-extensions/syntax-extensions.rst
@@ -871,7 +871,7 @@ notations are given below. The optional :production:`scope` is described in
: Inductive `ind_body` [`decl_notation`] with … with `ind_body` [`decl_notation`].
: CoInductive `ind_body` [`decl_notation`] with … with `ind_body` [`decl_notation`].
: Fixpoint `fix_body` [`decl_notation`] with … with `fix_body` [`decl_notation`].
- : CoFixpoint `cofix_body` [`decl_notation`] with … with `cofix_body` [`decl_notation`].
+ : CoFixpoint `fix_body` [`decl_notation`] with … with `fix_body` [`decl_notation`].
: [Local] Declare Custom Entry `ident`.
decl_notation : [where `string` := `term` [: `scope`] and … and `string` := `term` [: `scope`]].
modifiers : `modifier`, … , `modifier`