diff options
| author | Théo Zimmermann | 2020-03-26 11:34:39 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2020-03-26 11:34:39 +0100 |
| commit | 53a84d4e84034d213e86839d05b87a5cd80b4181 (patch) | |
| tree | a7166a10294be50844e5908895c68ac974b774fd /doc/sphinx | |
| parent | b398a4eb55c42a97d7d177839d5033a306ee7d52 (diff) | |
| parent | 245af3e197c36482931248479c8eca5d0e6459a6 (diff) | |
Merge PR #11913: Doc_grammar: Update cmd:: and tacn:: constructs in .rsts
Reviewed-by: Zimmi48
Diffstat (limited to 'doc/sphinx')
| -rw-r--r-- | doc/sphinx/language/gallina-extensions.rst | 2 | ||||
| -rw-r--r-- | doc/sphinx/language/gallina-specification-language.rst | 6 |
2 files changed, 3 insertions, 5 deletions
diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index 2abf6d02d2..8fcbeea570 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -996,7 +996,7 @@ are now available through the dot notation. Including multiple modules is a single :cmd:`Include` is equivalent to including each module in a separate :cmd:`Include` command. -.. cmd:: Include Type @module_type_inl {* <+ @module_type_inl } +.. cmd:: Include Type {+<+ @module_type_inl } .. deprecated:: 8.3 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 } |