diff options
| author | coqbot-app[bot] | 2020-11-20 09:21:27 +0000 |
|---|---|---|
| committer | GitHub | 2020-11-20 09:21:27 +0000 |
| commit | 122aef582e69f692e6720097a3fac7e0d4d41bcd (patch) | |
| tree | 062a2e1a02e687d5f5fe68b6dd949ee2b4c9dbae /doc/sphinx | |
| parent | 57c85b0d54e54ca33238399cab3285ef34d4edd2 (diff) | |
| parent | 00003b625ed3d5f3f2d79cf38ca6ad08e634432e (diff) | |
Merge PR #13403: Use only nats for occs_nums rather than ints
Reviewed-by: Zimmi48
Reviewed-by: herbelin
Diffstat (limited to 'doc/sphinx')
| -rw-r--r-- | doc/sphinx/proofs/writing-proofs/rewriting.rst | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/sphinx/proofs/writing-proofs/rewriting.rst b/doc/sphinx/proofs/writing-proofs/rewriting.rst index f3f69a2fdc..31050cb107 100644 --- a/doc/sphinx/proofs/writing-proofs/rewriting.rst +++ b/doc/sphinx/proofs/writing-proofs/rewriting.rst @@ -320,7 +320,7 @@ Performing computations ref_or_pattern_occ ::= @reference {? at @occs_nums } | @one_term {? at @occs_nums } occs_nums ::= {+ {| @natural | @ident } } - | - {| @natural | @ident } {* @int_or_var } + | - {+ {| @natural | @ident } } int_or_var ::= @integer | @ident unfold_occ ::= @reference {? at @occs_nums } |