diff options
| -rw-r--r-- | doc/sphinx/language/gallina-extensions.rst | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index 96e74bf118..5e214f6f7f 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -85,7 +85,7 @@ To build an object of type :token:`ident`, one should provide the constructor .. productionlist:: record_term : {| [`field_def` ; … ; `field_def`] |} - field_def : name [binders] := `record_term` + field_def : `ident` [`binders`] := `term` Alternatively, the following syntax allows creating objects by using named fields, as shown in this grammar. The fields do not have to be in any particular order, nor do they have |