diff options
Diffstat (limited to 'doc/sphinx/proofs')
| -rw-r--r-- | doc/sphinx/proofs/writing-proofs/rewriting.rst | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/doc/sphinx/proofs/writing-proofs/rewriting.rst b/doc/sphinx/proofs/writing-proofs/rewriting.rst index 5283f60b11..9ec568c2c7 100644 --- a/doc/sphinx/proofs/writing-proofs/rewriting.rst +++ b/doc/sphinx/proofs/writing-proofs/rewriting.rst @@ -323,10 +323,12 @@ Performing computations | delta {? @delta_flag } ref_or_pattern_occ ::= @reference {? at @occs_nums } | @one_term {? at @occs_nums } - occs_nums ::= {+ {| @natural | @ident } } - | - {+ {| @natural | @ident } } + occs_nums ::= {+ @nat_or_var } + | - {+ @nat_or_var } int_or_var ::= @integer | @ident + nat_or_var ::= @natural + | @ident unfold_occ ::= @reference {? at @occs_nums } pattern_occ ::= @one_term {? at @occs_nums } |