diff options
| author | Clément Pit-Claudel | 2018-05-18 01:19:50 -0400 |
|---|---|---|
| committer | Théo Zimmermann | 2018-09-20 10:12:55 +0200 |
| commit | aaabad040eaf50c6c11823d64a08027c080aa113 (patch) | |
| tree | c2dcbe87823524e40343fb8230fe970732dbc661 | |
| parent | 0b5251ee8a6f69d4b0700991884e68dfdfcf8ad6 (diff) | |
[doc] Fix more duplicate-label issues in production lists
| -rw-r--r-- | doc/sphinx/language/gallina-extensions.rst | 16 |
1 files changed, 10 insertions, 6 deletions
diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index ae96a75a94..27ed176a9b 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -20,7 +20,7 @@ expressions. In this sense, the :cmd:`Record` construction allows defining .. _record_grammar: - .. productionlist:: `sentence` + .. productionlist:: sentence record : `record_keyword` `record_body` with … with `record_body` record_keyword : Record | Inductive | CoInductive record_body : `ident` [ `binders` ] [: `sort` ] := [ `ident` ] { [ `field` ; … ; `field` ] }. @@ -80,11 +80,13 @@ To build an object of type :n:`@ident`, one should provide the constructor Definition half := mkRat true 1 2 (O_S 1) one_two_irred. Check half. +.. FIXME: move this to the main grammar in the spec chapter + .. _record-named-fields-grammar: .. productionlist:: - term : {| [`field_def` ; … ; `field_def`] |} - field_def : name [binders] := `term` + record_term : {| [`field_def` ; … ; `field_def`] |} + field_def : name [binders] := `record_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 @@ -152,12 +154,14 @@ It can be activated for printing with Set Printing Projections. Check top half. +.. FIXME: move this to the main grammar in the spec chapter + .. _record_projections_grammar: .. productionlist:: terms - term : term `.` ( qualid ) - : | term `.` ( qualid arg … arg ) - : | term `.` ( @`qualid` `term` … `term` ) + projection : projection `.` ( `qualid` ) + : | projection `.` ( `qualid` `arg` … `arg` ) + : | projection `.` ( @`qualid` `term` … `term` ) Syntax of Record projections |