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/fullGrammar | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

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

diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar
index 033ece04de..e493f3e318 100644
--- a/doc/tools/docgram/fullGrammar
+++ b/doc/tools/docgram/fullGrammar
@@ -480,6 +480,7 @@ opt_hintbases: [
 command: [
 | "Goal" lconstr
 | "Proof"
+| "Proof" "using" G_vernac.section_subset_expr
 | "Proof" "Mode" string
 | "Proof" lconstr
 | "Abort"
@@ -604,7 +605,7 @@ command: [
 | "Typeclasses" "Opaque" LIST1 reference
 | "Typeclasses" "eauto" ":=" debug eauto_search_strategy OPT natural
 | "Proof" "with" Pltac.tactic OPT [ "using" G_vernac.section_subset_expr ]
-| "Proof" "using" G_vernac.section_subset_expr OPT [ "with" Pltac.tactic ]
+| "Proof" "using" G_vernac.section_subset_expr "with" Pltac.tactic
 | "Tactic" "Notation" OPT ltac_tactic_level LIST1 ltac_production_item ":=" tactic
 | "Print" "Ltac" reference
 | "Locate" "Ltac" reference
@@ -2327,7 +2328,7 @@ conversion: [
 
 occs_nums: [
 | LIST1 nat_or_var
-| "-" nat_or_var LIST0 int_or_var
+| "-" LIST1 nat_or_var
 ]
 
 occs: [
@@ -2537,6 +2538,7 @@ or_and_intropattern_loc: [
 
 as_or_and_ipat: [
 | "as" or_and_intropattern_loc
+| "as" equality_intropattern
 |
 ]
 
-- 
cgit v1.2.3