From 00003b625ed3d5f3f2d79cf38ca6ad08e634432e Mon Sep 17 00:00:00 2001
From: Jim Fehrle
Date: Mon, 16 Nov 2020 20:24:09 -0800
Subject: Use only nats for occs_nums rather than ints

---
 doc/tools/docgram/orderedGrammar | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

(limited to 'doc/tools/docgram/orderedGrammar')

diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar
index e6fc6188b7..dddf0a908b 100644
--- a/doc/tools/docgram/orderedGrammar
+++ b/doc/tools/docgram/orderedGrammar
@@ -648,7 +648,7 @@ ref_or_pattern_occ: [
 
 occs_nums: [
 | LIST1 [ natural | ident ]
-| "-" [ natural | ident ] LIST0 int_or_var
+| "-" LIST1 [ natural | ident ]
 ]
 
 int_or_var: [
@@ -944,6 +944,7 @@ command: [
 | "Extract" "Inductive" qualid "=>" [ ident | string ] "[" LIST0 [ ident | string ] "]" OPT string      (* extraction plugin *)
 | "Show" "Extraction"      (* extraction plugin *)
 | "Proof"
+| "Proof" "using" section_var_expr
 | "Proof" "Mode" string
 | "Proof" term
 | "Abort" OPT [ "All" | ident ]
@@ -1024,7 +1025,7 @@ command: [
 | "Typeclasses" "Opaque" LIST1 qualid
 | "Typeclasses" "eauto" ":=" OPT "debug" OPT ( "(" [ "bfs" | "dfs" ] ")" ) OPT natural
 | "Proof" "with" ltac_expr OPT [ "using" section_var_expr ]
-| "Proof" "using" section_var_expr OPT [ "with" ltac_expr ]
+| "Proof" "using" section_var_expr "with" ltac_expr
 | "Tactic" "Notation" OPT ( "(" "at" "level" natural ")" ) LIST1 ltac_production_item ":=" ltac_expr
 | "Print" "Rewrite" "HintDb" ident
 | "Print" "Ltac" qualid
@@ -1960,6 +1961,7 @@ or_and_intropattern_loc: [
 
 as_or_and_ipat: [
 | "as" or_and_intropattern_loc
+| "as" equality_intropattern
 ]
 
 eqn_ipat: [
-- 
cgit v1.2.3