diff options
| author | Emilio Jesus Gallego Arias | 2019-05-24 00:45:40 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-05-24 00:45:40 +0200 |
| commit | 48bda9d680f605f012eb9c3af61f9e076a7d51be (patch) | |
| tree | 6d86a4ed1f3f5d54aeeaf9e55d35d9d3813496bc /doc/sphinx/language | |
| parent | 5cfdc20560392c2125dbcee31cfd308d5346b428 (diff) | |
| parent | 7c82a2713c8827ebc1e2896c83c6e7bd2f81c063 (diff) | |
Merge PR #10167: do not parse `|` as infix in patterns; parse `|}` as `|` `}`
Ack-by: SkySkimmer
Ack-by: Zimmi48
Reviewed-by: ejgallego
Ack-by: ggonthier
Reviewed-by: herbelin
Ack-by: jfehrle
Reviewed-by: mattam82
Diffstat (limited to 'doc/sphinx/language')
| -rw-r--r-- | doc/sphinx/language/gallina-specification-language.rst | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst index 8acbcbec8f..ebaa6fde66 100644 --- a/doc/sphinx/language/gallina-specification-language.rst +++ b/doc/sphinx/language/gallina-specification-language.rst @@ -185,8 +185,7 @@ is described in Chapter :ref:`syntaxextensionsandinterpretationscopes`. : `qualid` : _ : `num` - : ( `or_pattern` , … , `or_pattern` ) - or_pattern : `pattern` | … | `pattern` + : ( `pattern` | … | `pattern` ) Types |