diff options
| author | Jim Fehrle | 2020-11-16 20:24:09 -0800 |
|---|---|---|
| committer | Jim Fehrle | 2020-11-18 12:14:48 -0800 |
| commit | 00003b625ed3d5f3f2d79cf38ca6ad08e634432e (patch) | |
| tree | efb7599f68adf68be2f6aea86970745ea3ca5341 /doc/tools/docgram/fullGrammar | |
| parent | 04b25a7635e796ad05ef7db537883594a5144a56 (diff) | |
Use only nats for occs_nums rather than ints
Diffstat (limited to 'doc/tools/docgram/fullGrammar')
| -rw-r--r-- | doc/tools/docgram/fullGrammar | 6 |
1 files changed, 4 insertions, 2 deletions
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 | ] |