diff options
| author | Théo Zimmermann | 2019-11-21 17:39:41 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2019-11-21 17:39:41 +0100 |
| commit | a876df3f1e9a495ee04c78321adf83a31ede7f3c (patch) | |
| tree | da75e474f97b2434bc39fd877830b33c75982537 /doc/sphinx/user-extensions/syntax-extensions.rst | |
| parent | c0f34539209842735ccb93f3c069632b7eee4d6c (diff) | |
| parent | b4eca882b6692b6374dfff8517f9f5a5cc4970f5 (diff) | |
Merge PR #10614: Update the Gallina grammar in doc, "Terms" section
Ack-by: Zimmi48
Diffstat (limited to 'doc/sphinx/user-extensions/syntax-extensions.rst')
| -rw-r--r-- | doc/sphinx/user-extensions/syntax-extensions.rst | 2 |
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` |