diff options
Diffstat (limited to 'doc/sphinx/language/gallina-specification-language.rst')
| -rw-r--r-- | doc/sphinx/language/gallina-specification-language.rst | 6 |
1 files changed, 2 insertions, 4 deletions
diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst index 12a9a30f3d..fe359a23a9 100644 --- a/doc/sphinx/language/gallina-specification-language.rst +++ b/doc/sphinx/language/gallina-specification-language.rst @@ -1533,10 +1533,8 @@ Computations | delta {? @delta_flag } ref_or_pattern_occ ::= @smart_qualid {? at @occs_nums } | @one_term {? at @occs_nums } - occs_nums ::= {+ @num_or_var } - | - @num_or_var {* @int_or_var } - num_or_var ::= @num - | @ident + occs_nums ::= {+ {| @num | @ident } } + | - {| @num | @ident } {* @int_or_var } int_or_var ::= @int | @ident unfold_occ ::= @smart_qualid {? at @occs_nums } |