From e74d328b32634a44ab049f971ec33fe6cd24df72 Mon Sep 17 00:00:00 2001
From: Jim Fehrle
Date: Wed, 18 Nov 2020 13:18:04 -0800
Subject: Use nat_or_var where negative values don't make sense

---
 doc/sphinx/proofs/writing-proofs/rewriting.rst | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

(limited to 'doc/sphinx/proofs')

diff --git a/doc/sphinx/proofs/writing-proofs/rewriting.rst b/doc/sphinx/proofs/writing-proofs/rewriting.rst
index 31050cb107..121c5422dd 100644
--- a/doc/sphinx/proofs/writing-proofs/rewriting.rst
+++ b/doc/sphinx/proofs/writing-proofs/rewriting.rst
@@ -319,10 +319,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 }
 
-- 
cgit v1.2.3