diff options
| author | Clément Pit-Claudel | 2019-05-16 11:00:05 -0400 |
|---|---|---|
| committer | Clément Pit-Claudel | 2019-05-19 19:19:30 -0400 |
| commit | 4a69c594b484cb7e9af28b8ba9608a228e2376f1 (patch) | |
| tree | de9f94ae9f3cd5f0434919a4badfe5ab100473d0 /doc | |
| parent | 2a4bd4861d0ebf0b5d5a63774ac964b431e94fbb (diff) | |
[refman] Fix up the grammar entry for field_def
Diffstat (limited to 'doc')
| -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 |