Merge PR #9884: doc_grammar, a utility to extract Coq's grammar from .mlg files and insert it into .rst files

Ack-by: Zimmi48
Ack-by: gares
Ack-by: ppedrot

7 files changed, 9383 insertions, 0 deletions

diff --git a/doc/tools/docgram/README.md b/doc/tools/docgram/README.md
new file mode 100644
index 0000000000..98fdc38ca7
--- /dev/null
+++ b/doc/tools/docgram/README.md
@@ -0,0 +1,208 @@
+# Grammar extraction tool for documentation
+
+`doc_grammar` extracts Coq's grammar from `.mlg` files, edits it and inserts it in
+chunks into `.rst` files.  The tool currently inserts Sphinx
+`productionlist` constructs.  It also generates a file with `prodn` constructs
+for the entire grammar, but updates to `tacn` and `cmd` constructs must be done
+manually since the grammar doesn't have names for them as it does for
+nonterminals.  There is an option to report which `tacn` and `cmd` were not
+found in the `.rst` files.  `tacv` and `cmdv` constructs are not processed at all.
+
+The mlg grammars present several challenges to generating an accurate grammar
+for documentation purposes:
+
+* The 30+ mlg files don't define an overall order in which nonterminals should
+  appear in a complete grammar.
+
+* Even within a single mlg file, nonterminals and productions are often given
+  in an order that's much different from what a reader of the documentation would
+  expect.  In a small number of cases, changing the order in the mlg would change
+  how some inputs are parsed, in particular when the order determines how to distinguish
+  otherwise ambiguous inputs.
+
+  Strictly speaking, that means our grammar is not a context free grammar even though
+  we gloss over that distinction in the documentation.
+
+* For a few nonterminals, some productions are only available if certain plugins
+  are activated (e.g. SSR).  Readers should be informed about these.
+
+* Some limited parts of the grammar are defined in OCaml, including lookahead symbols
+  like `test_bracket_ident` and references to nonterminals in other files using
+  qualified names such as `Prim.ident`.  A few symbols are defined multiple times,
+  such as `scope` and `orient`.
+
+## What the tool does
+
+1. The tool reads all the `mlg` files and generates `fullGrammar`, which includes
+all the grammar without the actions for each production or the OCaml code.  This
+file is provided as a convenience to make it easier to examine the (mostly)
+unprocessed grammar of the mlg files with less clutter.  Nonterminals that use
+levels (`"5" RIGHTA` below) are modified, for example:
+
+```
+tactic_expr:
+  [ "5" RIGHTA
+    [ te = binder_tactic -> { te } ]
+```
+
+becomes
+
+```
+tactic_expr5: [
+| binder_tactic
+| tactic_expr4
+]
+```
+
+2. The tool applies grammar editing operations specified by `common.edit_mlg` to
+generate `editedGrammar`.
+
+3. `orderedGrammar` gives the desired order for the nonterminals and productions
+in the documented grammar.  Developers should edit this file to change the order.
+`doc_grammar` updates `orderedGrammar` so it has the same set of nonterminals and productions
+as `editedGrammar`.  The update process removes manually-added comments from
+`orderedGrammar` while automatically-generated comments will be regenerated.
+
+4. The tool applies further edits to the grammar specified by `productionlist.edit_mlg`,
+then it updates the productionlists in the `.rst` files as specified by comments in the form
+`.. insertgram <first nt> <last nt>`.  The edits are primarily to expand
+`.mlg` constructs such as `LIST1` and `OPT` into separate productions.  The tool
+generates `productionlistGrammar`, which has the entire grammar in the form of `productionlists`.
+
+5. Using the grammar produced in step 3, the tool applies edits specified by
+`prodn.edit_mlg` and generates `prodnGrammar`, representing each production as
+a Sphinx `prodn` construct.  Differently-edited grammars are used because `prodn`
+can naturally represent `LIST1 x SEP ','` whereas that is awkward for `productionlists`.
+
+## How to use the tool
+
+* `make doc_gram` updates `fullGrammar`.
+
+* `make doc_gram_verify` verifies that `fullGrammar` is consistent with the `.mlg` files.
+  This is for use by CI.
+
+* `make doc_gram_rsts` updates the `*Grammar` and `.rst` files.
+
+Changes to `fullGrammar`, `orderedGrammar` and the `.rsts` should be checked in to git.
+The other `*Grammar` files should not.
+
+### Command line arguments
+
+The executable takes a list of `.mlg` and `.rst` files as arguments.  The tool
+inserts the grammar into the `.rsts` as specified by comments in those files.
+The order of the `.mlg` files affects the order of nonterminals and productions in
+`fullGrammar`.  The order doesn't matter for the `.rst` files.
+
+Specifying the `-verify` command line argument avoids updating any of the files,
+but verifies that the current files are consistent.  This setting is meant for
+use in CI; it will be up to each developer to include the changes to `*Grammar` and
+the `.rst` files in their PRs when they've changed the grammar.
+
+Other command line arguments:
+
+* `-check-tacs` reports on differences in tactics between the `rsts` and the grammar
+
+* `-check-cmds` reports on differences in commands between the `rsts` and the grammar
+
+* `-no-warn` suppresses printing of some warning messages
+
+* `-short` limits processing to updating/verifying only the `fullGrammar` file
+
+* `-verbose` prints more messages about the grammar
+
+* `-verify` described above
+
+### Grammar editing scripts
+
+The grammar editing scripts `*.edit_mlg` are similar in format to `.mlg` files stripped
+of all OCaml features.  This is an easy way to include productions to match or add without
+writing another parser.  The `DOC_GRAMMAR` token at the beginning of each file
+signals the use of streamlined syntax.
+
+Each edit file has a series of items in the form of productions.  Items are applied
+in the order they appear.  There are two types of editing operations:
+
+* Global edits - edit rules that apply to the entire grammar in a single operation.
+  These are identified by using specific reserved names as the non-terminal name.
+
+* Local edits - edit rules that apply to the productions of a single non-terminal.
+  The rule is a local edit if the non-terminal name isn't reserved.  Individual
+  productions within a local edit that begin with a different set of reserved names
+  edit existing productions.  For  example `binders: [ | DELETE Pcoq.Constr.binders ]`
+  deletes the production `binders: [ | Pcoq.Constr.binders]`
+
+Productions that don't begin with a reserved name are added to the grammar,
+such as `empty: [ | ]`, which adds a new non-terminal `empty` with an
+empty production on the right-hand side.
+
+Another example: `LEFTQMARK: [ | "?" ]` is a local edit that treats `LEFTQMARK` as
+the name of a non-terminal and adds one production for it.  (We know that LEFTQMARK
+is a token but doc_grammar does not.)  `SPLICE: [ | LEFTQMARK ]` requests replacing all
+uses of `LEFTQMARK` anywhere in the grammar with its productions and removing the
+non-terminal.  The combined effect of these two is to replace all uses of
+`LEFTQMARK` with `"?"`.
+
+Here are the current operations.  They are likely to be refined as we learn
+what operations are most useful while we update the mlg files and documentation:
+
+### Global edits
+
+`DELETE` - deletes the specified non-terminals anywhere in the grammar.  Each
+should appear as a separate production.  Useful for removing non-terminals that
+only do lookahead that shouldn't be in the documentation.
+
+`RENAME` - each production specifies an (old name, new name) pair of
+non-terminals to rename.
+
+`SPLICE` - requests replacing all uses of the nonterminals anywhere in the
+grammar with its productions and removing the non-terminal. Each should appear
+as a separate production.  (Doesn't work recursively; splicing for both
+`A: [ | B ]` and `B: [ | C ]` must be done in separate SPLICE operations.)
+
+`EXPAND` - expands LIST0, LIST1, LIST* ... SEP and OPT constructs into
+new non-terminals
+
+### Local edits
+
+`DELETE <production>` - removes the specified production from the grammar
+
+`EDIT <production>` - modifies the specified production using the following tags
+that appear in the specified production:
+
+* `USE_NT <name>` LIST* - extracts LIST* as new nonterminal with the specified
+  new non-terminal name
+
+* `ADD_OPT <grammar symbol>` - looks for a production that matches the specified
+  production **without** `<grammar_symbol>`.  If found, both productions are
+  replaced with single production with `OPT <grammar_symbol>`
+
+  The current version handles a single USE_NT or ADD_OPT per EDIT.
+
+* `REPLACE` - (2 sequential productions) - removes `<oldprod>` and
+  inserts `<newprod>` in its place.
+
+```
+| REPLACE <oldprod>
+| WITH <newprod>
+```
+
+* (any other nonterminal name) - adds a new production (and possibly a new nonterminal)
+to the grammar.
+
+### `.rst` file updates
+
+`doc_grammar` updates `.rst` files when it sees the following 3 lines
+
+```
+.. insertgram <start> <end>
+.. productionlist:: XXX
+```
+
+The end of the existing `productionlist` is recognized by a blank line.
+
+### Other details
+
+The output identifies productions from plugins that aren't automatically loaded with
+`(* XXX plugin *)` in grammar files and with `(XXX plugin)` in productionlists.
+If desired, this mechanism could be extended to tag certain productions as deprecated,
+perhaps in conjunction with a coqpp change.
diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg
new file mode 100644
index 0000000000..ea94e21ff3
--- /dev/null
+++ b/doc/tools/docgram/common.edit_mlg
@@ -0,0 +1,220 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2019       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+(* Defines additional productions and edits for use in documentation.  Not compiled into Coq *)
+
+DOC_GRAMMAR
+
+(* additional nts to be spliced *)
+
+LEFTQMARK: [
+| "?"
+]
+
+SPLICE: [
+| LEFTQMARK
+]
+
+hyp: [
+| var
+]
+
+tactic_then_gen: [
+| EDIT ADD_OPT tactic_expr5 "|" tactic_then_gen
+| EDIT ADD_OPT tactic_expr5 ".." tactic_then_last
+]
+
+SPLICE: [
+| hyp
+| identref
+| pattern_ident (* depends on previous LEFTQMARK splice todo: improve *)
+| constr_eval  (* splices as multiple prods *)
+| tactic_then_last  (* todo: dependency on c.edit_mlg edit?? really useful? *)
+| Prim.name
+| ltac_selector
+| Constr.ident
+| tactic_then_locality  (* todo: cleanup *)
+| attribute_list
+]
+
+RENAME: [
+  (* map missing names for rhs *)
+| _binders binders
+| Constr.constr term
+| Constr.constr_pattern constr_pattern
+| Constr.global global
+| Constr.lconstr lconstr
+| Constr.lconstr_pattern lconstr_pattern
+| G_vernac.query_command query_command
+| G_vernac.section_subset_expr section_subset_expr
+| nonsimple_intropattern intropattern
+| Pltac.tactic tactic
+| Pltac.tactic_expr ltac_expr
+| Prim.ident ident
+| Prim.reference reference
+| Pvernac.Vernac_.main_entry vernac_control
+| Tactic.tactic tactic
+| tactic3 ltac_expr3  (* todo: can't figure out how this gets mapped by coqpp *)
+| tactic1 ltac_expr1  (* todo: can't figure out how this gets mapped by coqpp *)
+| tactic0 ltac_expr0  (* todo: can't figure out how this gets mapped by coqpp *)
+| tactic_expr5 ltac_expr
+| tactic_expr4 ltac_expr4
+| tactic_expr3 ltac_expr3
+| tactic_expr2 ltac_expr2
+| tactic_expr1 ltac_expr1
+| tactic_expr0 ltac_expr0
+
+  (* elementary renaming/OCaml-defined productions *)
+| clause clause_dft_concl
+| in_clause' in_clause
+| l_constr lconstr  (* todo: should delete the production *)
+
+  (* SSR *)
+| G_vernac.def_body def_body
+| Pcoq.Constr.constr term
+| Prim.by_notation by_notation
+| Prim.identref ident
+| Prim.natural natural
+| Vernac.rec_definition rec_definition
+
+  (* rename on lhs *)
+| intropatterns intropattern_list_opt
+| Constr.closed_binder closed_binder
+
+  (* historical name *)
+| constr term
+]
+
+DELETE: [
+| check_for_coloneq
+| impl_ident_head
+| local_test_lpar_id_colon
+| lookup_at_as_comma
+| only_starredidentrefs
+| test_bracket_ident
+| test_lpar_id_coloneq
+| test_lpar_id_rpar
+| test_lpar_idnum_coloneq
+| test_show_goal
+
+  (* SSR *)
+(* | ssr_null_entry *)
+| ssrtermkind  (* todo: rename as "test..." *)
+| term_annotation  (* todo: rename as "test..." *)
+| test_idcomma
+| test_nohidden
+| test_not_ssrslashnum
+| test_ssr_rw_syntax
+| test_ssreqid
+| test_ssrfwdid
+| test_ssrseqvar
+| test_ssrslashnum00
+| test_ssrslashnum01
+| test_ssrslashnum10
+| test_ssrslashnum11
+| test_ident_no_do
+| ssrdoarg  (* todo: this and the next one should be removed from the grammar? *)
+| ssrseqdir
+]
+
+ident: [
+| DELETE IDENT ssr_null_entry
+]
+
+natural: [
+| DELETE _natural
+]
+
+
+  (* added productions *)
+
+empty: [  (* todo: (bug) this is getting converted to empty -> empty *)
+|
+]
+
+lpar_id_coloneq: [
+| "(" IDENT; ":="
+]
+
+name_colon: [
+| IDENT; ":"
+| "_" ":"  (* todo: should "_" be a keyword or an identifier? *)
+]
+
+int: [ (* todo: probably should be NUMERAL *)
+| integer
+]
+
+command_entry: [
+| noedit_mode
+]
+
+binders: [
+| DELETE Pcoq.Constr.binders  (* todo: not sure why there are 2 "binders:" *)
+]
+
+(* edits to simplify *)
+
+ltac_expr1: [
+| EDIT match_key ADD_OPT "reverse" "goal" "with" match_context_list "end"
+]
+
+match_context_list: [
+| EDIT ADD_OPT "|" LIST1 match_context_rule SEP "|"
+]
+
+match_hyps: [
+| REPLACE name ":=" "[" match_pattern "]" ":" match_pattern
+| WITH name ":=" OPT ("[" match_pattern "]" ":") match_pattern
+| DELETE name ":=" match_pattern
+]
+
+match_list: [
+| EDIT ADD_OPT "|" LIST1 match_rule SEP "|"
+]
+
+
+selector_body: [
+| REPLACE range_selector_or_nth  (* depends on whether range_selector_or_nth is deleted first *)
+| WITH LIST1 range_selector SEP ","
+]
+
+range_selector_or_nth: [
+| DELETENT
+]
+
+simple_tactic: [
+| DELETE "intros"
+| REPLACE "intros" ne_intropatterns
+| WITH "intros" intropattern_list_opt
+| DELETE "eintros"
+| REPLACE "eintros" ne_intropatterns
+| WITH "eintros" intropattern_list_opt
+]
+
+intropattern_list_opt: [
+| DELETE LIST0 intropattern
+| intropattern_list_opt intropattern
+| empty
+]
+
+
+ne_intropatterns: [
+| DELETENT  (* todo: don't use DELETENT for this *)
+]
+
+
+or_and_intropattern: [
+| DELETE "()"
+| DELETE "(" simple_intropattern ")"
+| REPLACE "(" simple_intropattern "," LIST1 simple_intropattern SEP "," ")"
+|   WITH  "(" LIST0 simple_intropattern SEP "," ")"
+| EDIT "[" USE_NT intropattern_or LIST1 intropattern_list_opt SEP "|" "]"
+]
diff --git a/doc/tools/docgram/doc_grammar.ml b/doc/tools/docgram/doc_grammar.ml
new file mode 100644
index 0000000000..9f0a1942f9
--- /dev/null
+++ b/doc/tools/docgram/doc_grammar.ml
@@ -0,0 +1,1572 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2019       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+open Coqpp_parser
+open Coqpp_ast
+
+let exit_code = ref 0
+let show_warn = ref true
+
+let fprintf = Printf.fprintf
+
+let error s =
+  exit_code := 1;
+  Printf.eprintf "Error: ";
+  Printf.eprintf s
+
+(* todo: checking if !show_warn is true here gives a compilation error *)
+let warn s =
+  Printf.eprintf "Warning: ";
+  Printf.eprintf s
+
+type args = {
+  mlg_files : string list;
+  rst_files : string list;
+  fullGrammar : bool;
+  check_tacs : bool;
+  check_cmds : bool;
+  show_warn : bool;
+  verbose : bool;
+  verify : bool;
+}
+
+let default_args = {
+  mlg_files = [];
+  rst_files = [];
+  fullGrammar = false;
+  check_tacs = false;
+  check_cmds = false;
+  show_warn = true;
+  verbose = false;
+  verify = false;
+}
+
+(* translated symbols *)
+
+type doc_symbol =
+| Sterm of string
+| Snterm of string
+| Slist1 of doc_symbol
+| Slist1sep of doc_symbol * doc_symbol
+| Slist0 of doc_symbol
+| Slist0sep of doc_symbol * doc_symbol
+| Sopt of doc_symbol
+| Sparen of doc_symbol list (* for GRAMMAR EXTEND *)
+| Sprod of doc_symbol list list (* for GRAMMAR EXTEND *)
+  (* editing operations *)
+| Sedit of string
+| Sedit2 of string * string
+
+(* nonterminals to rename or delete *)
+module StringMap = Map.Make(String)
+module NTMap = StringMap
+module StringSet = Set.Make(String)
+
+type gram = {
+  (* map from nonterminal name to a list of prods *)
+  (* each production is a list of doc_symbol *)
+  map: doc_symbol list list NTMap.t;
+  (* specifies the order for nt's *)
+  order: string list;
+}
+
+module DocGram = struct
+  (* these guarantee that order and map have a 1-1 relationship
+     on the nt name.  They don't guarantee that nts on rhs of a production
+     are defined, nor do they prohibit duplicate productions *)
+
+  exception Duplicate
+  exception Invalid
+
+  (* add an nt at the end (if not already present) then set its prods *)
+  let g_maybe_add g nt prods =
+    if not (NTMap.mem nt !g.map) then
+      g := { !g with order = !g.order @ [nt] };
+    g := { !g with map = NTMap.add nt prods !g.map }
+
+  (* add an nt at the beginning (if not already present) then set its prods *)
+  let g_maybe_add_begin g nt prods =
+    if not (NTMap.mem nt !g.map) then
+      g := { !g with order = nt :: !g.order };
+    g := { !g with map = NTMap.add nt prods !g.map }
+
+  (* reverse the order of the grammar *)
+  let g_reverse g =
+    g := { !g with order = List.rev !g.order }
+
+  (* update the productions of an existing nt *)
+  let g_update_prods g nt prods =
+    ignore (NTMap.find nt !g.map);  (* don't add the nt if it's not present *)
+    g := { !g with map = NTMap.add nt prods !g.map }
+
+  (* remove a non-terminal *)
+  let g_remove g nt =
+    g := { map = NTMap.remove nt !g.map;
+           order = List.filter (fun elt -> elt <> nt) !g.order }
+
+  (* rename an nt and update its prods, keeping its original position.
+     If the new name already exists, include its prods *)
+  let g_rename_merge g nt nt' nprods =
+    let oprods =
+      try
+        let oprods = NTMap.find nt' !g.map in
+        g := { !g with order = List.filter (fun elt -> elt <> nt') !g.order };
+        oprods
+      with Not_found ->
+       g := { !g with map = NTMap.add nt' [] !g.map };
+       []
+    in
+    g := { map = NTMap.remove nt !g.map;
+           order = List.map (fun n -> if n = nt then nt' else n) !g.order };
+    g_update_prods g nt' (oprods @ nprods)
+
+  (* add a new nonterminal after "ins_after" None means insert at the beginning *)
+  let g_add_after g ins_after nt prods =
+    if NTMap.mem nt !g.map then raise Duplicate;  (* don't update the nt if it's already present *)
+    let rec insert_nt order res =
+      match ins_after, order with
+      | None, _ -> nt :: order
+      | Some _, [] -> raise Not_found
+      | Some ins_after_nt, hd :: tl ->
+        if hd = ins_after_nt then
+          (List.rev res) @ (hd :: nt :: tl)
+        else
+          insert_nt tl (hd :: res)
+    in
+    g := { order = insert_nt !g.order [];
+           map = NTMap.add nt prods !g.map }
+
+  (* replace the map and order *)
+  let g_reorder g map order =
+    let order_nts = StringSet.of_list order in
+    let map_nts = List.fold_left (fun res b -> let (nt, _) = b in StringSet.add nt res)
+      StringSet.empty (NTMap.bindings map) in
+    if List.length order <> NTMap.cardinal map ||
+      not (StringSet.equal order_nts map_nts) then raise Invalid;
+    g := { order = order; map = map }
+
+end
+open DocGram
+
+(*** Print routines ***)
+
+let sprintf = Printf.sprintf
+
+let map_and_concat f ?(delim="") l =
+  String.concat delim (List.map f l)
+
+let rec db_output_prodn = function
+  | Sterm s -> sprintf "(Sterm %s) " s
+  | Snterm s -> sprintf "(Snterm %s) " s
+  | Slist1 sym -> sprintf "(Slist1 %s) " (db_output_prodn sym)
+  | Slist1sep (sym, sep) -> sprintf "(Slist1sep %s %s) " (db_output_prodn sep) (db_output_prodn sym)
+  | Slist0 sym -> sprintf "(Slist0 %s) " (db_output_prodn sym)
+  | Slist0sep (sym, sep) -> sprintf "(Slist0sep %s %s)  " (db_output_prodn sep) (db_output_prodn sym)
+  | Sopt sym -> sprintf "(Sopt %s) " (db_output_prodn sym)
+  | Sparen prod -> sprintf "(Sparen %s) " (db_out_list prod)
+  | Sprod prods -> sprintf "(Sprod %s) " (db_out_prods prods)
+  | Sedit s -> sprintf "(Sedit %s) " s
+  | Sedit2 (s, s2) -> sprintf "(Sedit2 %s %s) " s s2
+and db_out_list prod = sprintf "(%s)" (map_and_concat db_output_prodn prod)
+and db_out_prods prods = sprintf "( %s )" (map_and_concat ~delim:" | " db_out_list prods)
+
+let rec output_prod plist need_semi = function
+    | Sterm s -> if plist then sprintf "%s" s else sprintf "\"%s\"" s
+    | Snterm s ->
+        if plist then sprintf "`%s`" s else
+          sprintf "%s%s" s (if s = "IDENT" && need_semi then ";" else "")
+    | Slist1 sym -> sprintf "LIST1 %s" (prod_to_str ~plist [sym])
+    | Slist1sep (sym, sep) -> sprintf "LIST1 %s SEP %s" (prod_to_str ~plist [sym]) (prod_to_str ~plist [sep])
+    | Slist0 sym -> sprintf "LIST0 %s" (prod_to_str ~plist [sym])
+    | Slist0sep (sym, sep) -> sprintf "LIST0 %s SEP %s" (prod_to_str ~plist [sym]) (prod_to_str ~plist [sep])
+    | Sopt sym -> sprintf "OPT %s" (prod_to_str ~plist [sym])
+    | Sparen sym_list -> sprintf "( %s )" (prod_to_str sym_list)
+    | Sprod sym_list ->
+      sprintf "[ %s ]" (String.concat " " (List.mapi (fun i r ->
+          let prod = (prod_to_str r) in
+          let sep = if i = 0 then "" else
+              if prod <> "" then "| " else "|" in
+          sprintf "%s%s" sep prod)
+        sym_list))
+    | Sedit s -> sprintf "%s" s
+    (* todo: make PLUGIN info output conditional on the set of prods? *)
+    | Sedit2 ("PLUGIN", plugin) ->
+      if plist then
+        sprintf "     (%s plugin)" plugin
+      else
+        sprintf "     (* %s plugin *)" plugin
+    | Sedit2 ("FILE", file) ->
+      let file_suffix_regex = Str.regexp ".*/\\([a-zA-Z0-9_\\.]+\\)" in
+      let suffix = if Str.string_match file_suffix_regex file 0 then Str.matched_group 1 file else file in
+      if plist then
+        sprintf "     (%s)" suffix
+      else
+        sprintf "     (* %s *)" suffix
+    | Sedit2 (s, s2) -> sprintf "%s \"%s\"" s s2
+
+and prod_to_str_r plist prod =
+  match prod with
+  | p :: tl ->
+    let need_semi =
+      match prod with
+      | Snterm "IDENT" :: Sterm _ :: _
+      | Snterm "IDENT" :: Sprod _ :: _ -> true
+      | _ -> false in
+    (output_prod plist need_semi p) :: (prod_to_str_r plist tl)
+  | [] -> []
+
+and prod_to_str ?(plist=false) prod =
+  String.concat " " (prod_to_str_r plist prod)
+
+
+let rec output_prodn = function
+  | Sterm s -> let s = if List.mem s ["{"; "{|"; "|"; "}"] then "%" ^ s else s in
+    sprintf "%s" s
+  | Snterm s -> sprintf "@%s" s
+  | Slist1 sym -> sprintf "{+ %s }" (output_prodn sym)
+  | Slist1sep (sym, sep) -> sprintf "{+%s %s }" (output_sep sep) (output_prodn sym)
+  | Slist0 sym -> sprintf "{* %s }" (output_prodn sym)
+  | Slist0sep (sym, sep) -> sprintf "{*%s %s }" (output_sep sep) (output_prodn sym)
+  | Sopt sym -> sprintf "{? %s }" (output_prodn sym)
+  | Sparen sym_list -> sprintf "%s" (prod_to_prodn sym_list)
+  | Sprod sym_list ->
+    let lcurly, rcurly = if List.length sym_list = 1 then "", "" else "{| ", " }" in
+    sprintf "%s%s%s"
+      lcurly
+      (String.concat " " (List.mapi (fun i r ->
+          let prod = (prod_to_prodn r) in
+          let sep = if i = 0 then "" else
+              if prod <> "" then "| " else "|" in
+          sprintf "%s%s" sep prod)
+        sym_list))
+      rcurly
+  | Sedit s -> sprintf "%s" s
+  | Sedit2 ("PLUGIN", s2) -> ""
+  | Sedit2 (s, s2) -> sprintf "%s \"%s\"" s s2
+
+and output_sep sep =
+  match sep with
+  | Sterm s -> sprintf "%s" s  (* avoid escaping separator *)
+  | _ -> output_prodn sep
+
+and prod_to_prodn prod = String.concat " " (List.map output_prodn prod)
+
+type fmt = [`MLG | `PRODLIST | `PRODN ]
+
+(* print a subset of the grammar with nts in the specified order *)
+let print_in_order out g fmt nt_order hide =
+  List.iter (fun nt ->
+      if not (StringSet.mem nt hide) then
+        try
+          let prods = NTMap.find nt !g.map in
+          match fmt with
+          | `MLG ->
+            fprintf out "%s: [\n" nt;
+            List.iter (fun prod ->
+                let str = prod_to_str ~plist:false prod in
+                let pfx = if str = "" then "|" else "| " in
+                fprintf out "%s%s\n" pfx str)
+              prods;
+            fprintf out "]\n\n"
+          | `PRODLIST ->
+            fprintf out "%s :" nt;
+            List.iteri (fun i prod ->
+                if i > 0 then
+                  fprintf out "%s :" (String.make (String.length nt) ' ');
+                let str = prod_to_str ~plist:true prod in
+                let pfx = if str = "" then "" else " " in
+                fprintf out "%s%s\n" pfx str)
+              prods;
+          | `PRODN ->
+            fprintf out "\n%s:\n" nt;
+            List.iter (fun prod ->
+                let str = prod_to_prodn prod in
+                let pfx = if str = "" then "" else " " in
+                fprintf out "%s%s\n" pfx str)
+              prods;
+        with Not_found -> error "Missing nt '%s' in print_in_order\n" nt)
+    nt_order
+
+
+(*** Read grammar routines ***)
+
+let cvt_ext prod =
+  let rec to_doc_sym = function
+    | Ulist1 sym -> Slist1 (to_doc_sym sym)
+    | Ulist1sep (sym, s) -> Slist1sep ((to_doc_sym sym), Sterm s)
+    | Ulist0 sym -> Slist0 (to_doc_sym sym)
+    | Ulist0sep (sym, s) -> Slist0sep ((to_doc_sym sym), Sterm s)
+    | Uopt sym -> Sopt (to_doc_sym sym)
+    | Uentry s -> Snterm s
+    | Uentryl (s, i) -> Snterm (s ^ (string_of_int i))
+ in
+ let from_ext = function
+   | ExtTerminal s -> Sterm s
+   | ExtNonTerminal (s, _) -> to_doc_sym s
+ in
+ List.map from_ext prod
+
+let rec cvt_gram_sym = function
+  | GSymbString s -> Sterm s
+  | GSymbQualid (s, level) ->
+    Snterm (match level with
+           | Some str -> s ^ str
+           | None -> s)
+  | GSymbParen l -> Sparen (cvt_gram_sym_list l)
+  | GSymbProd ll ->
+    let cvt = List.map cvt_gram_prod ll in
+    (match cvt with
+    | (Snterm x :: []) :: [] -> Snterm x
+    | (Sterm x :: []) :: []  -> Sterm x
+    | _ -> Sprod cvt)
+
+and cvt_gram_sym_list l =
+  let get_sym = function
+    | GSymbQualid (s, level) -> s
+    | _ -> ""
+  in
+
+  match l with
+  | GSymbQualid ("LIST0", _) :: s :: GSymbQualid ("SEP", _) :: sep :: tl ->
+    Slist0sep (cvt_gram_sym s, cvt_gram_sym sep) :: cvt_gram_sym_list tl
+  | GSymbQualid ("LIST1", _) :: s :: GSymbQualid ("SEP", _) :: sep :: tl ->
+    Slist1sep (cvt_gram_sym s, cvt_gram_sym sep) :: cvt_gram_sym_list tl
+  | GSymbQualid ("LIST0", _) :: s :: tl ->
+    Slist0 (cvt_gram_sym s) :: cvt_gram_sym_list tl
+  | GSymbQualid ("LIST1", _) :: s :: tl ->
+    Slist1 (cvt_gram_sym s) :: cvt_gram_sym_list tl
+  | GSymbQualid ("OPT", _) :: s :: tl ->
+    Sopt (cvt_gram_sym s) :: cvt_gram_sym_list tl
+  | GSymbQualid ("IDENT", _) :: s2 :: tl when get_sym s2 = "" ->
+    cvt_gram_sym s2 :: cvt_gram_sym_list tl
+  | GSymbQualid ("ADD_OPT", _) :: tl ->
+    (Sedit "ADD_OPT") :: cvt_gram_sym_list tl
+  | GSymbQualid ("NOTE", _) :: GSymbQualid (s2, l) :: tl ->
+    (Sedit2 ("NOTE", s2)) :: cvt_gram_sym_list tl
+  | GSymbQualid ("USE_NT", _) :: GSymbQualid (s2, l) :: tl ->
+    (Sedit2 ("USE_NT", s2)) :: cvt_gram_sym_list tl
+  | hd :: tl ->
+    cvt_gram_sym hd :: cvt_gram_sym_list tl
+  | [] -> []
+
+and cvt_gram_prod p =
+ List.concat (List.map (fun x -> let _, gs = x in cvt_gram_sym_list gs)  p.gprod_symbs)
+
+
+let add_symdef nt file symdef_map =
+  let ent =
+    try
+      StringMap.find nt !symdef_map
+    with Not_found -> []
+  in
+  symdef_map := StringMap.add nt (Filename.basename file::ent) !symdef_map
+
+let rec edit_SELF nt cur_level next_level right_assoc prod =
+  let len = List.length prod in
+  List.mapi (fun i sym ->
+    match sym with
+    | Snterm s -> begin match s with
+      | s when s = nt || s = "SELF" ->
+        if i = 0 then Snterm next_level
+        else if i+1 < len then sym
+        else if right_assoc then Snterm cur_level else Snterm next_level
+      | "NEXT" -> Snterm next_level
+      | _ -> sym
+    end
+    | Slist1 sym -> Slist1 (List.hd (edit_SELF nt cur_level next_level right_assoc [sym]))
+    | Slist0 sym -> Slist0 (List.hd (edit_SELF nt cur_level next_level right_assoc [sym]))
+    | x -> x)
+  prod
+
+
+let autoloaded_mlgs = [ (* in the order they are loaded by Coq *)
+ "parsing/g_constr.mlg";
+ "parsing/g_prim.mlg";
+ "vernac/g_vernac.mlg";
+ "vernac/g_proofs.mlg";
+ "toplevel/g_toplevel.mlg";
+ "plugins/ltac/extraargs.mlg";
+ "plugins/ltac/g_obligations.mlg";
+ "plugins/ltac/coretactics.mlg";
+ "plugins/ltac/extratactics.mlg";
+ "plugins/ltac/profile_ltac_tactics.mlg";
+ "plugins/ltac/g_auto.mlg";
+ "plugins/ltac/g_class.mlg";
+ "plugins/ltac/g_rewrite.mlg";
+ "plugins/ltac/g_eqdecide.mlg";
+ "plugins/ltac/g_tactic.mlg";
+ "plugins/ltac/g_ltac.mlg";
+ "plugins/syntax/g_string.mlg";
+ "plugins/btauto/g_btauto.mlg";
+ "plugins/rtauto/g_rtauto.mlg";
+ "plugins/cc/g_congruence.mlg";
+ "plugins/firstorder/g_ground.mlg";
+ "plugins/syntax/g_numeral.mlg";
+]
+
+
+let ematch prod edit =
+  let rec ematchr prod edit =
+    (*Printf.printf "%s and\n  %s\n\n" (prod_to_str prod) (prod_to_str edit);*)
+    match (prod, edit) with
+    | (_, Sedit _ :: tl)
+    | (_, Sedit2 _ :: tl)
+      -> ematchr prod tl
+    | (Sedit _ :: tl, _)
+    | (Sedit2 _ :: tl, _)
+      -> ematchr tl edit
+    | (phd :: ptl, hd :: tl) ->
+      let m = match (phd, hd) with
+        | (Slist1 psym, Slist1 sym)
+        | (Slist0 psym, Slist0 sym)
+        | (Sopt psym, Sopt sym)
+          -> ematchr [psym] [sym]
+        | (Slist1sep (psym, psep), Slist1sep (sym, sep))
+        | (Slist0sep (psym, psep), Slist0sep (sym, sep))
+          -> ematchr [psym] [sym] && ematchr [psep] [sep]
+        | (Sparen psyml, Sparen syml)
+          -> ematchr psyml syml
+        | (Sprod psymll, Sprod symll)
+          -> List.fold_left (&&) true (List.map2 ematchr psymll symll)
+        | _, _ -> phd = hd
+      in
+      m && ematchr ptl tl
+    | ([], hd :: tl) -> false
+    | (phd :: ptl, []) -> false
+    | ([], []) -> true
+in
+  (*Printf.printf "\n";*)
+  let rv = ematchr prod edit in
+  (*Printf.printf "%b\n" rv;*)
+  rv
+
+let has_match p prods = List.exists (fun p2 -> ematch p p2) prods
+
+let plugin_regex = Str.regexp "^plugins/\\([a-zA-Z0-9_]+\\)/"
+
+let read_mlg is_edit ast file level_renames symdef_map =
+  let res = ref [] in
+  let add_prods nt prods =
+    if not is_edit then
+      add_symdef nt file symdef_map;
+    let prods = if not is_edit &&
+        not (List.mem file autoloaded_mlgs) &&
+        Str.string_match plugin_regex file 0 then
+      let plugin = Str.matched_group 1 file in
+      List.map (fun p -> p @ [Sedit2 ("PLUGIN", plugin)]) prods
+    else
+      prods
+    in
+    (* todo: doesn't yet work perfectly with SPLICE *)
+(*    let prods = if not is_edit then List.map (fun p -> p @ [Sedit2 ("FILE", file)]) prods else prods in*)
+    res := (nt, prods) :: !res
+  in
+  let prod_loop = function
+    | GramExt grammar_ext ->
+      let get_label = function
+        | Some s -> s
+        | None -> ""
+      in
+      List.iter (fun ent ->
+          let len = List.length ent.gentry_rules in
+          List.iteri (fun i rule ->
+              let nt = ent.gentry_name in
+              let level = (get_label rule.grule_label) in
+              let level = if level <> "" then level else
+                match ent.gentry_pos with
+                | Some Level lev
+                | Some Before lev
+                | Some After lev
+                  -> lev
+                (* Looks like FIRST/LAST can be ignored for documenting the current grammar *)
+                | _ -> "" in
+              let cur_level = nt ^ level in
+              let next_level = nt ^
+                  if i+1 < len then (get_label (List.nth ent.gentry_rules (i+1)).grule_label) else "" in
+              let right_assoc = (rule.grule_assoc = Some RightA) in
+
+              if i = 0 && cur_level <> nt && not (StringMap.mem nt !level_renames) then begin
+                level_renames := StringMap.add nt cur_level !level_renames;
+              end;
+              let cvted = List.map cvt_gram_prod rule.grule_prods in
+              (* edit names for levels *)
+              (* See https://camlp5.github.io/doc/html/grammars.html#b:Associativity *)
+              let edited = List.map (edit_SELF nt cur_level next_level right_assoc) cvted in
+              let prods_to_add =
+                if cur_level <> nt && i+1 < len then
+                  edited @ [[Snterm next_level]]
+                else
+                  edited in
+              add_prods cur_level prods_to_add)
+            ent.gentry_rules
+        ) grammar_ext.gramext_entries
+
+    | VernacExt vernac_ext ->
+      let node = match vernac_ext.vernacext_entry with
+      | None -> "command"
+      | Some c -> String.trim c.code
+      in
+      add_prods node
+        (List.map (fun r -> cvt_ext r.vernac_toks) vernac_ext.vernacext_rules)
+    | VernacArgumentExt vernac_argument_ext ->
+      add_prods vernac_argument_ext.vernacargext_name
+        (List.map (fun r -> cvt_ext r.tac_toks) vernac_argument_ext.vernacargext_rules)
+    | TacticExt tactic_ext ->
+      add_prods "simple_tactic"
+        (List.map (fun r -> cvt_ext r.tac_toks) tactic_ext.tacext_rules)
+    | ArgumentExt argument_ext ->
+      add_prods argument_ext.argext_name
+        (List.map (fun r -> cvt_ext r.tac_toks) argument_ext.argext_rules)
+    | _ -> ()
+  in
+
+  List.iter prod_loop ast;
+  List.rev !res
+
+let dir s = "doc/tools/docgram/" ^ s
+
+let read_mlg_edit file =
+  let fdir = dir file in
+  let level_renames = ref StringMap.empty in (* ignored *)
+  let symdef_map = ref StringMap.empty in (* ignored *)
+  read_mlg true (parse_file fdir) fdir level_renames symdef_map
+
+let add_rule g nt prods file =
+  let ent = try NTMap.find nt !g.map with Not_found -> [] in
+  let nodups = List.concat (List.map (fun prod ->
+      if has_match prod ent then begin
+        if !show_warn then
+          warn "%s: Duplicate production '%s: %s'\n" file nt (prod_to_str prod);
+        []
+      end else
+        [prod])
+    prods) in
+  g_maybe_add_begin g nt (ent @ nodups)
+
+let read_mlg_files g args symdef_map =
+  let level_renames = ref StringMap.empty in
+  let last_autoloaded = List.hd (List.rev autoloaded_mlgs) in
+  List.iter (fun file ->
+    (* does nt renaming, deletion and splicing *)
+    let rules = read_mlg false (parse_file file) file level_renames symdef_map in
+    let numprods = List.fold_left (fun num rule ->
+        let nt, prods = rule in
+        add_rule g nt prods file;
+        num + List.length prods)
+      0 rules
+    in
+    if args.verbose then begin
+      Printf.eprintf "%s:  %d nts,  %d prods\n" file (List.length rules) numprods;
+      if file = last_autoloaded then
+        Printf.eprintf "  Optionally loaded plugins:\n"
+    end
+  ) args.mlg_files;
+  g_reverse g;
+  !level_renames
+
+
+(*** global editing ops ***)
+
+let create_edit_map edits =
+  let rec aux edits map =
+    match edits with
+    | [] -> map
+    | edit :: tl ->
+      let (key, binding) = edit in
+      aux tl (StringMap.add key binding map)
+  in
+  aux edits StringMap.empty
+
+(* edit a production: rename nonterminals, drop nonterminals, substitute nonterminals *)
+let rec edit_prod g top edit_map prod =
+  let edit_nt edit_map sym0 nt =
+    try
+      let binding = StringMap.find nt edit_map in
+      match binding with
+      | "DELETE" -> []
+      | "SPLICE" ->
+        begin
+          try let splice_prods = NTMap.find nt !g.map in
+            match splice_prods with
+            | [] -> assert false
+            | [p] -> List.rev p
+            | _ -> [Sprod splice_prods]
+          with Not_found -> error "Missing nt '%s' for splice\n" nt; [Snterm nt]
+        end
+      | _ -> [Snterm binding]
+    with Not_found -> [sym0]
+  in
+
+  let rec edit_symbol sym0 =
+    match sym0 with
+      | Sterm s -> [sym0]
+      | Snterm s -> edit_nt edit_map sym0 s
+      | Slist1 sym -> [Slist1 (List.hd (edit_symbol sym))]
+      (* you'll get a run-time failure deleting a SEP symbol *)
+      | Slist1sep (sym, sep) -> [Slist1sep (List.hd (edit_symbol sym), (List.hd (edit_symbol sep)))]
+      | Slist0 sym -> [Slist0 (List.hd (edit_symbol sym))]
+      | Slist0sep (sym, sep) -> [Slist0sep (List.hd (edit_symbol sym), (List.hd (edit_symbol sep)))]
+      | Sopt sym -> [Sopt (List.hd (edit_symbol sym))]
+      | Sparen slist -> [Sparen (List.hd (edit_prod g false edit_map slist))]
+      | Sprod slistlist -> let (_, prods) = edit_rule g edit_map "" slistlist in
+                           [Sprod prods]
+      | Sedit _
+      | Sedit2 _ -> [sym0] (* these constructors not used here *)
+  in
+  let is_splice nt =
+    try
+      StringMap.find nt edit_map = "SPLICE"
+    with Not_found -> false
+  in
+  let get_splice_prods nt =
+    try NTMap.find nt !g.map
+    with Not_found -> (error "Missing nt '%s' for splice\n" nt; [])
+  in
+
+  (* special case splice creating multiple new productions *)
+  let splice_prods = match prod with
+    | Snterm nt :: [] when is_splice nt ->
+      get_splice_prods nt
+    | _ -> []
+  in
+  if top && splice_prods <> [] then
+    splice_prods
+  else
+    [List.rev (List.concat (List.rev (List.map (fun sym -> edit_symbol sym) prod)))]
+
+and edit_rule g edit_map nt rule =
+  let nt =
+    try let new_name = StringMap.find nt edit_map in
+      match new_name with
+      | "SPLICE" -> nt
+      | "DELETE" -> ""
+      | _ -> new_name
+    with Not_found -> nt
+  in
+  (nt, (List.concat (List.map (edit_prod g true edit_map) rule)))
+
+(*** splice: replace a reference to a nonterminal with its definition ***)
+
+(* todo: create a better splice routine, handle recursive case *)
+let apply_splice g splice_map =
+  StringMap.iter (fun nt b ->
+      if not (NTMap.mem nt !g.map) then
+        error "Unknown nt '%s' for apply_splice\n" nt)
+    splice_map;
+  List.iter (fun b ->
+      let (nt, prods) = b in
+      let (nt', prods) = edit_rule g splice_map nt prods in
+      g_update_prods g nt' prods)
+    (NTMap.bindings !g.map);
+  List.iter (fun b ->
+      let (nt, op) = b in
+      match op with
+      | "DELETE"
+      | "SPLICE" ->
+        g_remove g nt;
+      | _ -> ())
+    (StringMap.bindings splice_map)
+
+let find_first edit prods nt =
+  let rec find_first_r edit prods nt i =
+    match prods with
+    | [] ->
+      error "Can't find '%s' in REPLACE for '%s'\n" (prod_to_str edit) nt;
+      raise Not_found
+    | prod :: tl ->
+      if ematch prod edit then i
+      else find_first_r edit tl nt (i+1)
+  in
+  find_first_r edit prods nt 0
+
+let remove_prod edit prods nt =
+  let res, got_first = List.fold_left (fun args prod ->
+      let res, got_first = args in
+      if not got_first && ematch prod edit then
+        res, true
+      else
+        prod :: res, got_first)
+    ([], false) prods in
+  if not got_first then
+    error "Can't find '%s' to DELETE for '%s'\n" (prod_to_str edit) nt;
+  List.rev res
+
+let insert_after posn insert prods =
+  List.concat (List.mapi (fun i prod ->
+      if i = posn then prod :: insert else [prod])
+    prods)
+
+(*** replace LIST*, OPT with new nonterminals ***)
+
+(* generate a non-terminal name for a replacement *)
+let nt_regex = Str.regexp "^[a-zA-Z_][a-zA-Z0-9_\\.]*$"
+let good_name name = if Str.string_match nt_regex name 0 then name else ""
+let map_name s =
+  let s = match s with
+  | "|" -> "or"
+  | "!" -> "exclam"
+  | ">" -> "gt"
+  | "<" -> "lt"
+  | "+" -> "plus"
+  | "?" -> "qmark"
+  | "}" -> "rbrace"
+  | "," -> "comma"
+  | ";" -> "semi"
+  | _ -> s
+  in
+  good_name s
+
+let rec gen_nt_name sym =
+  let name_from_prod prod =
+    let rec aux name sterm_name prod =
+      if name <> "" then name else
+        match prod with
+        | [] -> sterm_name
+        | Sterm s :: tl
+        | Snterm s :: tl ->
+          if good_name s <> "" then
+            aux (map_name s) sterm_name tl
+          else
+            aux name (map_name s) tl;
+        | sym :: tl->
+          aux (gen_nt_name sym) sterm_name tl
+    in
+    aux "" "" prod
+  in
+
+  let name = match sym with
+    | Sterm s -> map_name s
+    | Snterm s -> s
+    | Slist1 sym
+    | Slist1sep (sym, _)
+    | Slist0 sym
+    | Slist0sep (sym, _)
+    | Sopt sym ->
+      gen_nt_name sym
+    | Sparen slist ->
+      name_from_prod slist
+    | Sprod slistlist ->
+      name_from_prod (List.hd slistlist)
+    | _ -> ""
+  in
+  good_name name
+
+(* create a new nt for LIST* or OPT with the specified name *)
+let rec maybe_add_nt g insert_after name sym queue =
+  let empty = [Snterm "empty"] in
+  let maybe_unwrap ?(multi=false) sym =
+    match sym with
+    | Sprod slist when List.length slist = 1 || multi
+                   ->    slist
+    | Sparen slist -> [ slist ]
+    | _ ->            [ [sym] ]
+  in
+  let unw sym = List.hd (maybe_unwrap sym) in
+  let get_prods nt =
+    match sym with
+    | Slist1 sym ->           let sym' = unw sym in
+                              [ [Snterm nt] @ sym';           sym' ]
+    | Slist1sep (sym, sep)
+    | Slist0sep (sym, sep) -> let sym' = unw sym in
+                              [ [Snterm nt; sep] @ sym';      sym' ]
+    | Slist0 sym ->           [ [Snterm nt] @ (unw sym);      empty ]
+    | Sopt sym ->             (maybe_unwrap ~multi:true sym) @ [ empty ]
+    | Sprod slistlist ->      slistlist
+    | _ -> []
+  in
+
+  let is_slist0sep sym =
+    match sym with
+    | Slist0sep _ -> true
+    | _ -> false
+  in
+
+  (* find an existing nt with an identical definition, or generate an unused nt name *)
+  let rec find_name nt i =
+    let trial_name = sprintf "%s%s" nt (if i = 1 then "" else string_of_int i) in
+    try
+      if NTMap.find trial_name !g.map = get_prods trial_name then
+        trial_name
+      else
+        find_name nt (succ i)
+    with Not_found -> trial_name
+  in
+  let list_name sep =
+    match sep with
+      | Sterm s ->
+        let name = map_name s in
+        if name = s then "_list" else "_list_" ^ name
+      | _ -> "_list"
+  in
+  let nt = name ^ match sym with
+    | Slist1 sym ->           "_list"
+    | Slist1sep (sym, sep) -> list_name sep
+    | Slist0 sym ->           "_list_opt"
+    | Slist0sep (sym, sep) -> list_name sep   (* special handling *)
+    | Sopt sym ->             "_opt"
+    | Sprod slistlist ->      "_alt"
+    | _ -> (error "Invalid symbol for USE_NT for nt '%s'\n" name; "ERROR")
+  in
+  let base_nt = find_name nt 1 in
+  let new_nt = if is_slist0sep sym then base_nt ^ "_opt" else base_nt in
+  if not (NTMap.mem new_nt !g.map) then begin
+    let prods = if is_slist0sep sym then [ [Snterm base_nt]; empty ] else get_prods base_nt in
+    g_add_after g (Some !insert_after) new_nt prods;
+    insert_after := new_nt;
+    Queue.add new_nt queue
+  end;
+  if is_slist0sep sym && not (NTMap.mem base_nt !g.map) then begin
+    match sym with
+    | Slist0sep (sym, sep) ->
+      let prods = get_prods base_nt in
+      g_add_after g (Some !insert_after) base_nt prods;
+      insert_after := base_nt;
+      Queue.add base_nt queue
+    | _ -> ()
+  end;
+  new_nt
+
+(* expand LIST*, OPT and add "empty" *)
+(* todo: doesn't handle recursive expansions well, such as syntax_modifier_opt *)
+and expand_rule g edited_nt queue =
+  let rule = NTMap.find edited_nt !g.map in
+  let insert_after = ref edited_nt in
+  let rec expand rule =
+    let rec aux syms res =
+      match syms with
+      | [] -> res
+      | sym0 :: tl ->
+        let new_sym = match sym0 with
+          | Sterm _
+          | Snterm _ ->
+            sym0
+          | Slist1 sym
+          | Slist1sep (sym, _)
+          | Slist0 sym
+          | Slist0sep (sym, _)
+          | Sopt sym ->
+            let name = gen_nt_name sym in
+            if name <> "" then begin
+              let new_nt = maybe_add_nt g insert_after name sym0 queue in
+              Snterm new_nt
+            end else sym0
+          | Sparen slist -> Sparen (expand slist)
+          | Sprod slistlist ->
+            let has_empty = List.length (List.hd (List.rev slistlist)) = 0 in
+            let name = gen_nt_name sym0 in
+            if name <> "" then begin
+              let new_nt = maybe_add_nt g insert_after name
+                  (if has_empty then (Sopt (Sprod (List.rev (List.tl (List.rev slistlist))) ))
+                  else sym0) queue
+              in
+              Snterm new_nt
+            end else
+              Sprod (List.map expand slistlist)
+          | Sedit _
+          | Sedit2 _ ->
+            sym0 (* these constructors not used here *)
+        in
+        aux tl (new_sym :: res)
+    in
+    List.rev (aux rule (if edited_nt <> "empty" && ematch rule [] then [Snterm "empty"] else []))
+  in
+  let rule' = List.map expand rule in
+  g_update_prods g edited_nt rule'
+
+let expand_lists g =
+  (* todo: use Queue.of_seq w OCaml 4.07+ *)
+  let queue = Queue.create () in
+  List.iter (fun nt -> Queue.add nt queue) !g.order;
+  try
+    while true do
+      let nt = Queue.pop queue in
+      expand_rule g nt queue
+    done
+  with
+  | Queue.Empty -> ()
+
+let edit_all_prods g op eprods =
+  let do_it op eprods num =
+    let rec aux eprods res =
+      match eprods with
+      | [] -> res
+      | [Snterm old_nt; Snterm new_nt] :: tl when num = 2 ->
+        aux tl ((old_nt, new_nt) :: res)
+      | [Snterm old_nt] :: tl when num = 1 ->
+        aux tl ((old_nt, op) :: res)
+      | eprod :: tl ->
+        error "Production '%s: %s' must have only %d nonterminal(s)\n"
+            op (prod_to_str eprod) num;
+        aux tl res
+    in
+    let map = create_edit_map (aux eprods []) in
+    if op = "SPLICE" then
+      apply_splice g map
+    else (* RENAME/DELETE *)
+      List.iter (fun b -> let (nt, _) = b in
+          let prods = try NTMap.find nt !g.map  with Not_found -> [] in
+          let (nt', prods') = edit_rule g map nt prods in
+          if nt' = "" then
+            g_remove g nt
+          else if nt <> nt' then
+            g_rename_merge g nt nt' prods'
+          else
+            g_update_prods g nt prods')
+        (NTMap.bindings !g.map);
+  in
+  match op with
+  | "RENAME" -> do_it op eprods 2; true
+  | "DELETE" -> do_it op eprods 1; true
+  | "SPLICE" -> do_it op eprods 1; true
+  | "EXPAND" ->
+    if List.length eprods > 1 || List.length (List.hd eprods) <> 0 then
+      error "'EXPAND:' expects a single empty production\n";
+    expand_lists g; true
+  | _ -> false
+
+let edit_single_prod g edit0 prods nt =
+  let rec edit_single_prod_r edit prods nt seen =
+    match edit with
+    | [] -> prods
+    | Sedit "ADD_OPT" :: sym :: tl ->
+      let prods' = (try
+          let pfx = List.rev seen in
+          let posn = find_first edit0 prods nt in
+          let prods = insert_after posn [pfx @ (Sopt sym :: tl)] prods in
+          let prods = remove_prod (pfx @ (sym :: tl)) prods nt in
+          remove_prod (pfx @ tl) prods nt
+        with Not_found -> prods) in
+        edit_single_prod_r tl prods' nt seen
+    | Sedit "ADD_OPT" :: [] -> error "Bad position for ADD_OPT\n"; prods
+    | Sedit2 ("USE_NT", name) :: sym :: tl ->
+      let prods' = (try
+        let nt = maybe_add_nt g (ref nt) name sym (Queue.create ()) in
+        let pfx = List.rev seen in
+        let posn = find_first edit0 prods nt in
+        let prods = insert_after posn [pfx @ (Snterm nt :: tl)] prods in
+        remove_prod (pfx @ (sym :: tl)) prods nt
+      with Not_found -> prods) in
+      edit_single_prod_r tl prods' nt seen
+    | Sedit2 ("USE_NT", _) :: [] -> error "Bad position for USE_NT\n"; prods
+    | sym :: tl ->
+      edit_single_prod_r tl prods nt (sym :: seen)
+  in
+  edit_single_prod_r edit0 prods nt []
+
+let apply_edit_file g edits =
+  List.iter (fun b ->
+      let (nt, eprod) = b in
+      if not (edit_all_prods g nt eprod) then begin
+        let rec aux eprod prods add_nt =
+          match eprod with
+          | [] -> prods, add_nt
+          | (Snterm "DELETE" :: oprod) :: tl ->
+            aux tl (remove_prod oprod prods nt) add_nt
+          | (Snterm "DELETENT" :: _) :: tl ->  (* note this doesn't remove references *)
+            g_remove g nt;
+            aux tl prods false
+          | (Snterm "EDIT" :: oprod) :: tl ->
+            aux tl (edit_single_prod g oprod prods nt) add_nt
+          | (Snterm "REPLACE" :: oprod) :: (Snterm "WITH" :: rprod) :: tl ->
+            let prods' = (try
+              let posn = find_first oprod prods nt in
+              let prods = insert_after posn [rprod] prods in  (* insert new prod *)
+              remove_prod oprod prods nt      (* remove orig prod *)
+              with Not_found -> prods)
+            in
+            aux tl prods' add_nt
+          | (Snterm "REPLACE" :: _ as eprod) :: tl ->
+            error "Missing WITH after '%s' in '%s'\n" (prod_to_str eprod) nt;
+            aux tl prods add_nt
+          | prod :: tl ->
+            (* add a production *)
+            if has_match prod prods then
+              error "Duplicate production '%s' for %s\n" (prod_to_str prod) nt;
+            aux tl (prods @ [prod]) add_nt
+        in
+        let prods, add_nt =
+          aux eprod (try NTMap.find nt !g.map with Not_found -> []) true in
+        if add_nt then
+          g_maybe_add g nt prods
+      end)
+    edits
+
+
+(*** main routines ***)
+
+ (* get the nt's in the production, preserving order, don't worry about dups *)
+ let nts_in_prod prod =
+  let rec traverse = function
+  | Sterm s -> []
+  | Snterm s -> [s]
+  | Slist1 sym
+  | Slist0 sym
+  | Sopt sym
+    -> traverse sym
+  | Slist1sep (sym, sep)
+  | Slist0sep (sym, sep)
+    -> traverse sym @ (traverse sep)
+  | Sparen sym_list -> List.concat (List.map traverse sym_list)
+  | Sprod sym_list_list -> List.concat (List.map (fun l -> List.concat (List.map traverse l)) sym_list_list)
+  | Sedit _
+  | Sedit2 _ -> []
+  in
+  List.rev (List.concat (List.map traverse prod))
+
+(* get the transitive closure of a non-terminal excluding "stops" symbols.
+   Preserve ordering to the extent possible *)
+(* todo: at the moment, the code doesn't use the ordering; consider switching to using
+sets instead of lists *)
+let nt_closure g start stops =
+  let stop_set = StringSet.of_list stops in
+  let rec nt_closure_r res todo =
+    match todo with
+    | [] -> res
+    | nt :: tl ->
+      if List.mem nt res || StringSet.mem nt stop_set then
+        nt_closure_r res tl
+      else begin
+        let more_to_do =
+          try
+            let prods = NTMap.find nt !g.map in
+            tl @ (List.concat (List.map nts_in_prod prods))
+          with Not_found -> tl in
+        nt_closure_r (nt :: res) more_to_do
+      end
+  in
+  List.rev (nt_closure_r [] [start])
+
+let header = "--------------------------------------------"
+let nt_subset_in_orig_order g nts =
+  let subset = StringSet.of_list nts in
+  List.filter (fun nt -> StringSet.mem nt subset) !g.order
+
+let print_chunk out g seen fmt title starts ends =
+  fprintf out "\n\n%s:\n%s\n" title header;
+  List.iter (fun start ->
+      let nts = (nt_closure g start ends) in
+      print_in_order out g fmt (nt_subset_in_orig_order g nts) !seen;
+      seen := StringSet.union !seen (StringSet.of_list nts))
+    starts
+
+let print_chunks g out fmt () =
+  let seen = ref StringSet.empty in
+  print_chunk out g seen fmt "lconstr" ["lconstr"] ["binder_constr"; "tactic_expr5"];
+  print_chunk out g seen fmt "Gallina syntax of terms" ["binder_constr"] ["tactic_expr5"];
+  print_chunk out g seen fmt "Gallina The Vernacular" ["gallina"] ["tactic_expr5"];
+  print_chunk out g seen fmt "intropattern_list_opt" ["intropattern_list"; "or_and_intropattern_loc"] ["operconstr"; "tactic_expr5"];
+  print_chunk out g seen fmt "simple_tactic" ["simple_tactic"]
+    ["tactic_expr5"; "tactic_expr3"; "tactic_expr2"; "tactic_expr1"; "tactic_expr0"];
+
+  (*print_chunk out g seen fmt "Ltac" ["tactic_expr5"] [];*)
+  print_chunk out g seen fmt "Ltac" ["tactic_expr5"] ["tactic_expr4"];
+  print_chunk out g seen fmt "Ltac 4" ["tactic_expr4"] ["tactic_expr3"; "tactic_expr2"];
+  print_chunk out g seen fmt "Ltac 3" ["tactic_expr3"] ["tactic_expr2"];
+  print_chunk out g seen fmt "Ltac 2" ["tactic_expr2"] ["tactic_expr1"];
+  print_chunk out g seen fmt "Ltac 1" ["tactic_expr1"] ["tactic_expr0"];
+  print_chunk out g seen fmt "Ltac 0" ["tactic_expr0"] [];
+
+
+  print_chunk out g seen fmt "command" ["command"] [];
+  print_chunk out g seen fmt "vernac_toplevel" ["vernac_toplevel"] [];
+  print_chunk out g seen fmt "vernac_control" ["vernac_control"] []
+
+  (*
+    let ssr_tops = ["ssr_dthen"; "ssr_else"; "ssr_mpat"; "ssr_rtype"] in
+    seen := StringSet.union !seen (StringSet.of_list ssr_tops);
+
+    print_chunk out g seen fmt "ssrindex" ["ssrindex"] [];
+    print_chunk out g seen fmt "command" ["command"] [];
+    print_chunk out g seen fmt "binder_constr" ["binder_constr"] [];
+    (*print_chunk out g seen fmt "closed_binder" ["closed_binder"] [];*)
+    print_chunk out g seen fmt "gallina_ext" ["gallina_ext"] [];
+    (*print_chunk out g seen fmt "hloc" ["hloc"] [];*)
+    (*print_chunk out g seen fmt "hypident" ["hypident"] [];*)
+    print_chunk out g seen fmt "simple_tactic" ["simple_tactic"] [];
+    print_chunk out g seen fmt "tactic_expr" ["tactic_expr4"; "tactic_expr1"; "tactic_expr0"] [];
+    fprintf out "\n\nRemainder:\n";
+    print_in_order g (List.filter (fun x -> not (StringSet.mem x !seen)) !g.order) StringSet.empty;
+  *)
+
+
+    (*seen := StringSet.diff !seen (StringSet.of_list ssr_tops);*)
+    (*print_chunk out g seen fmt "vernac_toplevel" ["vernac_toplevel"] [];*)
+
+let start_symbols = ["vernac_toplevel"; "tactic_mode"]
+let tokens = [ "BULLET"; "FIELD"; "IDENT"; "NUMERAL"; "STRING" ] (* don't report as undefined *)
+
+let report_bad_nts g file =
+  let rec get_nts refd defd bindings =
+    match bindings with
+    | [] -> refd, defd
+    | (nt, prods) :: tl ->
+      get_nts (List.fold_left (fun res prod ->
+                  StringSet.union res (StringSet.of_list (nts_in_prod prod)))
+                refd prods)
+        (StringSet.add nt defd) tl
+  in
+  let all_nts_ref, all_nts_def =
+    get_nts (StringSet.of_list tokens) (StringSet.of_list tokens) (NTMap.bindings !g.map) in
+
+  let undef = StringSet.diff all_nts_ref all_nts_def in
+  List.iter (fun nt -> warn "%s: Undefined symbol '%s'\n" file nt) (StringSet.elements undef);
+
+  let reachable =
+    List.fold_left (fun res sym ->
+        StringSet.union res (StringSet.of_list (nt_closure g sym [])))
+      StringSet.empty start_symbols
+  in
+  let unreachable = List.filter (fun nt -> not (StringSet.mem nt reachable)) !g.order in
+  List.iter (fun nt -> warn "%s: Unreachable symbol '%s'\n" file nt) unreachable
+
+
+let report_info g symdef_map =
+  let num_prods = List.fold_left (fun sum nt -> let prods = NTMap.find nt !g.map in sum + (List.length prods))
+    0 !g.order
+  in
+
+  Printf.eprintf "\nstart symbols: %s\n" (String.concat " " start_symbols);
+  Printf.eprintf "%d nonterminals defined, %d productions\n" (NTMap.cardinal !g.map) num_prods;
+  Printf.eprintf "%d terminals\n" (List.length tokens);
+
+  Printf.eprintf "\nSymbols with multiple definition points in *.mlg:\n";
+  let bindings = List.sort (fun a b -> let (ak, _) = a and (bk, _) = b in
+                            String.compare ak bk) (StringMap.bindings symdef_map) in
+  List.iter (fun b ->
+      let (k, v) = b in
+      if List.length v > 1 then begin
+        Printf.eprintf "  %s:  " k;
+        List.iter (fun f -> Printf.eprintf "%s " f) v;
+        Printf.eprintf "\n"
+      end)
+    bindings;
+  Printf.eprintf "\n"
+
+
+
+[@@@ocaml.warning "-32"]
+let rec dump prod =
+  match prod with
+  | hd :: tl -> let s = (match hd with
+    | Sterm s -> sprintf "Sterm %s" s
+    | Snterm s -> sprintf "Snterm \"%s\"" s
+    | Slist1 sym -> "Slist1"
+    | Slist0 sym -> "Slist0"
+    | Sopt sym -> "Sopt"
+    | Slist1sep _ -> "Slist1sep"
+    | Slist0sep _ -> "Slist0sep"
+    | Sparen sym_list -> "Sparen"
+    | Sprod sym_list_list -> "Sprod"
+    | Sedit _ -> "Sedit"
+    | Sedit2 _ -> "Sedit2") in
+    Printf.printf "%s " s;
+    dump tl
+  | [] -> Printf.printf "\n"
+[@@@ocaml.warning "+32"]
+
+let reorder_grammar eg reordered_rules file =
+  let og = ref { map = NTMap.empty; order = [] } in
+  List.iter (fun rule ->
+      let nt, prods = rule in
+      try
+        (* only keep nts and prods in common with editedGrammar *)
+        let eg_prods = NTMap.find nt !eg.map in
+        let prods = List.filter (fun prod -> (has_match prod eg_prods)) prods in
+        if NTMap.mem nt !og.map then
+          warn "%s: Duplicate nonterminal '%s'\n" file nt;
+        add_rule og nt prods file
+      with Not_found -> ())
+    reordered_rules;
+  g_reverse og;
+
+  (* insert a prod in a list after prev_prod (None=at the beginning) *)
+  let rec insert_prod prev_prod prod prods res =
+    match prev_prod, prods with
+    | None, _ -> prod :: prods
+    | Some _, [] -> raise Not_found
+    | Some ins_after_prod, hd :: tl ->
+      if ematch hd ins_after_prod then
+        (List.rev res) @ (hd :: prod :: tl)
+      else
+        insert_prod prev_prod prod tl (hd :: res)
+  in
+
+  (* insert prods that are not already in og_prods *)
+  let rec upd_prods prev_prod eg_prods og_prods =
+    match eg_prods with
+    | [] -> og_prods
+    | prod :: tl ->
+      let og_prods =
+        if has_match prod og_prods then
+          List.map (fun p -> if ematch p prod then prod else p) og_prods
+        else
+          insert_prod prev_prod prod og_prods [] in
+      upd_prods (Some prod) tl og_prods
+  in
+
+  (* add nts and prods not present in orderedGrammar *)
+  let _ = List.fold_left (fun prev_nt nt ->
+      let e_prods = NTMap.find nt !eg.map in
+      if not (NTMap.mem nt !og.map) then
+        g_add_after og prev_nt nt e_prods
+      else
+        g_update_prods og nt (upd_prods None e_prods (NTMap.find nt !og.map));
+      Some nt)
+    None !eg.order in
+  g_reorder eg !og.map !og.order
+
+
+let finish_with_file old_file verify =
+  let files_eq f1 f2 =
+    let chunksize = 8192 in
+    (try
+      let ofile = open_in_bin f1 in
+      let nfile = open_in_bin f2 in
+      let rv = if (in_channel_length ofile) <> (in_channel_length nfile) then false
+        else begin
+        let obuf = Bytes.create chunksize in
+        Bytes.fill obuf 0 chunksize '\x00';
+        let nbuf = Bytes.create chunksize in
+        Bytes.fill nbuf 0 chunksize '\x00';
+        let rec read () =
+          let olen = input ofile obuf 0 chunksize in
+          let _ = input nfile nbuf 0 chunksize in
+          if obuf <> nbuf then
+            false
+          else if olen = 0 then
+            true
+          else
+            read ()
+        in
+        read ()
+        end
+      in
+      close_in ofile;
+      close_in nfile;
+      rv
+    with Sys_error _ -> false)
+  in
+
+  let temp_file = (old_file ^ "_temp") in
+  if verify then
+    if (files_eq old_file temp_file || !exit_code <> 0) then
+      Sys.remove temp_file
+    else
+      error "%s is not current\n" old_file
+  else
+    Sys.rename temp_file old_file
+
+let open_temp_bin file =
+  open_out_bin (sprintf "%s_temp" file)
+
+let find_longest_match prods str =
+  (* todo: require a minimum length? *)
+  let common_prefix_len s1 s2 =
+    let limit = min (String.length s1) (String.length s2) in
+    let rec aux off =
+      if off = limit then off
+      else if s1.[off] = s2.[off] then aux (succ off)
+      else off
+    in
+    aux 0
+  in
+
+  let slen = String.length str in
+  let rec longest best multi best_len prods =
+    match prods with
+    | [] -> best, multi, best_len
+    | prod :: tl ->
+      let pstr = String.trim (prod_to_prodn prod) in
+      let clen = common_prefix_len str pstr in
+      if clen = slen && slen = String.length pstr then
+        pstr, false, clen  (* exact match *)
+      else if clen > best_len then
+        longest pstr false clen tl  (* better match *)
+      else if clen = best_len then
+        longest best true best_len tl  (* 2nd match with same length *)
+      else
+        longest best multi best_len tl  (* worse match *)
+  in
+  longest "" false 0 prods
+
+type seen = {
+  nts: (string * int) NTMap.t;
+  tacs: (string * int) NTMap.t;
+  cmds: (string * int) NTMap.t;
+}
+
+let process_rst g file args seen tac_prods cmd_prods =
+  let old_rst = open_in file in
+  let new_rst = open_temp_bin file in
+  let linenum = ref 0 in
+  let dir_regex = Str.regexp "^\\([ \t]*\\)\\.\\.[ \t]*\\([a-zA-Z0-9:]*\\)\\(.*\\)" in
+  let ig_args_regex = Str.regexp "^[ \t]*\\([a-zA-Z0-9_\\.]*\\)[ \t]*\\([a-zA-Z0-9_\\.]*\\)" in
+  let blank_regex = Str.regexp "^[ \t]*$" in
+  let end_prodlist_regex = Str.regexp "^[ \t]*$" in
+  let rec index_of_r str list index =
+    match list with
+    | [] -> None
+    | hd :: list ->
+      if hd = str then Some index
+      else index_of_r str list (index+1)
+  in
+  let index_of str list = index_of_r str list 0 in
+  let getline () =
+    let line = input_line old_rst in
+    incr linenum;
+    line
+  in
+  let output_insertgram start_index end_ indent is_coq_group =
+    let rec nthcdr n list = if n = 0 then list else nthcdr (n-1) (List.tl list) in
+    let rec copy_prods list =
+      match list with
+      | [] -> ()
+      | nt :: tl ->
+        (try
+          let (prev_file, prev_linenum) = NTMap.find nt !seen.nts in
+          warn "%s line %d: '%s' already included at %s line %d\n"
+              file !linenum nt prev_file prev_linenum;
+        with Not_found ->
+          if is_coq_group then
+            seen := { !seen with nts = (NTMap.add nt (file, !linenum) !seen.nts)} );
+        let prods = NTMap.find nt !g.map in
+        List.iteri (fun i prod ->
+            let rhs = String.trim (sprintf ": %s" (prod_to_str ~plist:true prod)) in
+            fprintf new_rst "%s   %s %s\n" indent (if i = 0 then nt else String.make (String.length nt) ' ') rhs)
+          prods;
+        if nt <> end_ then copy_prods tl
+    in
+    copy_prods (nthcdr start_index !g.order)
+  in
+
+  let process_insertgram line rhs =
+    if not (Str.string_match ig_args_regex rhs 0) then
+      error "%s line %d: bad arguments '%s' for 'insertgram'\n" file !linenum rhs
+    else begin
+      let start = Str.matched_group 1 rhs in
+      let end_ = Str.matched_group 2 rhs in
+      let start_index = index_of start !g.order in
+      let end_index = index_of end_ !g.order in
+      if start_index = None then
+        error "%s line %d: '%s' is undefined\n" file !linenum start;
+      if end_index = None then
+        error "%s line %d: '%s' is undefined\n" file !linenum end_;
+      match start_index, end_index with
+      | Some start_index, Some end_index ->
+        if start_index > end_index then
+          error "%s line %d: '%s' must appear before '%s' in .../orderedGrammar\n" file !linenum start end_
+        else begin
+          try
+            let line2 = getline() in
+            if not (Str.string_match blank_regex line2 0) then
+              error "%s line %d: expecting a blank line after 'insertgram'\n" file !linenum
+            else begin
+              let line3 = getline() in
+              if not (Str.string_match dir_regex line3 0) || (Str.matched_group 2 line3) <> "productionlist::" then
+                error "%s line %d: expecting 'productionlist' after 'insertgram'\n" file !linenum
+              else begin
+                let indent = Str.matched_group 1 line3 in
+                let is_coq_group = ("coq" = String.trim (Str.matched_group 3 line3)) in
+                let rec skip_to_end () =
+                  let endline = getline() in
+                  if Str.string_match end_prodlist_regex endline 0 then begin
+                    fprintf new_rst "%s\n\n%s\n" line line3;
+                    output_insertgram start_index end_ indent is_coq_group;
+                    fprintf new_rst "%s\n" endline
+                  end else
+                    skip_to_end ()
+                in
+                skip_to_end ()
+              end
+            end
+          with End_of_file -> error "%s line %d: unexpected end of file\n" file !linenum;
+        end
+      | _ -> ()
+    end
+
+  in
+  try
+    while true do
+      let line = getline() in
+      if Str.string_match dir_regex line 0 then begin
+        let dir = Str.matched_group 2 line in
+        let rhs = String.trim (Str.matched_group 3 line) in
+        match dir with
+        | "productionlist::" ->
+          if rhs = "coq" then
+            warn "%s line %d: Missing 'insertgram' before 'productionlist:: coq'\n" file !linenum;
+          fprintf new_rst "%s\n" line;
+        | "tacn::" when args.check_tacs ->
+          if not (StringSet.mem rhs tac_prods) then
+            warn "%s line %d: Unknown tactic: '%s'\n" file !linenum rhs;
+          if NTMap.mem rhs !seen.tacs then
+            warn "%s line %d: Repeated tactic: '%s'\n" file !linenum rhs;
+          seen := { !seen with tacs = (NTMap.add rhs (file, !linenum) !seen.tacs)};
+          fprintf new_rst "%s\n" line
+        | "cmd::" when args.check_cmds ->
+          if not (StringSet.mem rhs cmd_prods) then
+            warn "%s line %d: Unknown command: '%s'\n" file !linenum rhs;
+          if NTMap.mem rhs !seen.cmds then
+            warn "%s line %d: Repeated command: '%s'\n" file !linenum rhs;
+          seen := { !seen with cmds = (NTMap.add rhs (file, !linenum) !seen.cmds)};
+          fprintf new_rst "%s\n" line
+        | "insertgram" ->
+          process_insertgram line rhs
+        | _ -> fprintf new_rst "%s\n" line
+      end else
+        fprintf new_rst "%s\n" line;
+    done
+  with End_of_file -> ();
+  close_in old_rst;
+  close_out new_rst;
+  finish_with_file file args.verify
+
+let report_omitted_prods entries seen label split =
+  let maybe_warn first last n =
+    if first <> "" then begin
+      if first <> last then
+        warn "%ss '%s' to %s'%s' not included in .rst files (%d)\n" label first split last n
+      else
+        warn "%s %s not included in .rst files\n" label first;
+    end
+  in
+
+  let first, last, n = List.fold_left (fun missing nt ->
+      let first, last, n = missing in
+      if NTMap.mem nt seen then begin
+        maybe_warn first last n;
+        "", "", 0
+      end else
+        (if first = "" then nt else first), nt, n + 1)
+    ("", "", 0) entries in
+  maybe_warn first last n
+
+let process_grammar args =
+  let symdef_map = ref StringMap.empty in
+  let g = ref { map = NTMap.empty; order = [] } in
+
+  let level_renames = read_mlg_files g args symdef_map in
+
+  (* rename nts with levels *)
+  List.iter (fun b -> let (nt, prod) = b in
+      let (_, prod) = edit_rule g level_renames nt prod in
+      g_update_prods g nt prod)
+    (NTMap.bindings !g.map);
+
+  (* print the full grammar with minimal editing *)
+  let out = open_temp_bin (dir "fullGrammar") in
+  fprintf out "%s\n%s\n\n"
+      "(* Coq grammar generated from .mlg files.  Do not edit by hand.  Not compiled into Coq *)"
+      "DOC_GRAMMAR";
+  print_in_order out g `MLG !g.order StringSet.empty;
+  close_out out;
+  finish_with_file (dir "fullGrammar") args.verify;
+
+  if not args.fullGrammar then begin
+    (* do shared edits *)
+    if !exit_code = 0 then begin
+      let common_edits = read_mlg_edit "common.edit_mlg" in
+      apply_edit_file g common_edits
+    end;
+    let prodn_gram = ref { map = !g.map; order = !g.order } in
+
+    if !exit_code = 0 && not args.verify then begin
+      let prodlist_edits = read_mlg_edit "productionlist.edit_mlg" in
+      apply_edit_file g prodlist_edits;
+      let out = open_temp_bin (dir "productionlistGrammar") in
+      if args.verbose then
+        report_info g !symdef_map;
+      print_in_order out g `PRODLIST !g.order StringSet.empty;
+      (*print_chunks g out `PRODLIST ();*)
+      close_out out;
+      finish_with_file (dir "productionlistGrammar") args.verify;
+    end;
+
+    if !exit_code = 0 && not args.verify then begin
+      let out = open_temp_bin (dir "editedGrammar") in
+      fprintf out "%s\n%s\n\n"
+          "(* Edited Coq grammar generated from .mlg files.  Do not edit by hand.  Not compiled into Coq *)"
+          "DOC_GRAMMAR";
+      print_in_order out g `MLG !g.order StringSet.empty;
+      close_out out;
+      finish_with_file (dir "editedGrammar") args.verify;
+      report_bad_nts g "editedGrammar"
+    end;
+
+    if !exit_code = 0 then begin
+      let ordered_grammar = read_mlg_edit "orderedGrammar" in
+      let out = open_temp_bin (dir "orderedGrammar") in
+      fprintf out "%s\n%s\n\n"
+          ("(* Defines the order to apply to editedGrammar to get productionlistGrammar.\n" ^
+          "doc_grammar will modify this file to add/remove nonterminals and productions\n" ^
+           "to match editedGrammar, which will remove comments.  Not compiled into Coq *)")
+          "DOC_GRAMMAR";
+      reorder_grammar g ordered_grammar "orderedGrammar";
+      print_in_order out g `MLG !g.order StringSet.empty;
+      close_out out;
+      finish_with_file (dir "orderedGrammar") args.verify;
+    end;
+
+    if !exit_code = 0 then begin
+      let plist nt =
+        let list = (List.map (fun t -> String.trim (prod_to_prodn t))
+          (NTMap.find nt !g.map)) in
+        list, StringSet.of_list list in
+      let tac_list, tac_prods = plist "simple_tactic" in
+      let cmd_list, cmd_prods = plist "command" in
+      let seen = ref { nts=NTMap.empty; tacs=NTMap.empty; cmds=NTMap.empty } in
+      List.iter (fun file -> process_rst g file args seen tac_prods cmd_prods) args.rst_files;
+      report_omitted_prods !g.order !seen.nts "Nonterminal" "";
+      if args.check_tacs then
+        report_omitted_prods tac_list !seen.tacs "Tactic" "\n                 ";
+      if args.check_cmds then
+        report_omitted_prods cmd_list !seen.cmds "Command" "\n                  "
+    end;
+
+    (* generate output for prodn: simple_tactic, command, also for Ltac?? *)
+    if !exit_code = 0 && not args.verify then begin
+      let prodn_edits = read_mlg_edit "prodn.edit_mlg" in
+      apply_edit_file prodn_gram prodn_edits;
+      let out = open_temp_bin (dir "prodnGrammar") in
+      print_in_order out prodn_gram `PRODN !prodn_gram.order StringSet.empty;
+      close_out out;
+      finish_with_file (dir "prodnGrammar") args.verify
+    end
+  end
+
+let parse_args () =
+  let suffix_regex = Str.regexp ".*\\.\\([a-z]+\\)$" in
+  let args =
+    List.fold_left (fun args arg ->
+        match arg with
+        | "-check-cmds" -> { args with check_cmds = true }
+        | "-check-tacs" -> { args with check_tacs = true }
+        | "-no-warn" -> show_warn := false; { args with show_warn = true }
+        | "-short" -> { args with fullGrammar = true }
+        | "-verbose" -> { args with verbose = true }
+        | "-verify" -> { args with verify = true }
+        | arg when Str.string_match suffix_regex arg 0 ->
+            (match Str.matched_group 1 arg with
+            | "mlg" -> { args with mlg_files = (arg :: args.mlg_files) }
+            | "rst" -> { args with rst_files = (arg :: args.rst_files) }
+            | _ -> error "Unknown command line argument '%s'\n" arg; args)
+        | arg -> error "Unknown command line argument '%s'\n" arg; args)
+      default_args (List.tl (Array.to_list Sys.argv)) in
+  { args with mlg_files = (List.rev args.mlg_files); rst_files = (List.rev args.rst_files)}
+
+let () =
+  (*try*)
+    Printexc.record_backtrace true;
+    let args = parse_args () in
+    if !exit_code = 0 then begin
+      process_grammar args
+    end;
+    exit !exit_code
+  (*with _ -> Printexc.print_backtrace stdout; exit 1*)
diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar
new file mode 100644
index 0000000000..a83638dd73
--- /dev/null
+++ b/doc/tools/docgram/fullGrammar
@@ -0,0 +1,3174 @@
+(* Coq grammar generated from .mlg files.  Do not edit by hand.  Not compiled into Coq *)
+DOC_GRAMMAR
+
+Constr.ident: [
+| Prim.ident
+]
+
+Prim.name: [
+| "_"
+]
+
+global: [
+| Prim.reference
+]
+
+constr_pattern: [
+| constr
+]
+
+lconstr_pattern: [
+| lconstr
+]
+
+sort: [
+| "Set"
+| "Prop"
+| "SProp"
+| "Type"
+| "Type" "@{" "_" "}"
+| "Type" "@{" universe "}"
+]
+
+sort_family: [
+| "Set"
+| "Prop"
+| "SProp"
+| "Type"
+]
+
+universe_increment: [
+| "+" natural
+|
+]
+
+universe_name: [
+| global
+| "Set"
+| "Prop"
+]
+
+universe_expr: [
+| universe_name universe_increment
+]
+
+universe: [
+| "max" "(" LIST1 universe_expr SEP "," ")"
+| universe_expr
+]
+
+lconstr: [
+| operconstr200
+| l_constr
+]
+
+constr: [
+| operconstr8
+| "@" global instance
+]
+
+operconstr200: [
+| binder_constr
+| operconstr100
+]
+
+operconstr100: [
+| operconstr99 "<:" binder_constr
+| operconstr99 "<:" operconstr100
+| operconstr99 "<<:" binder_constr
+| operconstr99 "<<:" operconstr100
+| operconstr99 ":" binder_constr
+| operconstr99 ":" operconstr100
+| operconstr99 ":>"
+| operconstr99
+]
+
+operconstr99: [
+| operconstr90
+]
+
+operconstr90: [
+| operconstr10
+]
+
+operconstr10: [
+| operconstr9 LIST1 appl_arg
+| "@" global instance LIST0 operconstr9
+| "@" pattern_identref LIST1 identref
+| operconstr9
+]
+
+operconstr9: [
+| ".." operconstr0 ".."
+| operconstr8
+]
+
+operconstr8: [
+| operconstr1
+]
+
+operconstr1: [
+| operconstr0 ".(" global LIST0 appl_arg ")"
+| operconstr0 ".(" "@" global LIST0 ( operconstr9 ) ")"
+| operconstr0 "%" IDENT
+| operconstr0
+]
+
+operconstr0: [
+| atomic_constr
+| match_constr
+| "(" operconstr200 ")"
+| "{|" record_declaration bar_cbrace
+| "{" binder_constr "}"
+| "`{" operconstr200 "}"
+| "`(" operconstr200 ")"
+| "ltac" ":" "(" Pltac.tactic_expr ")"
+]
+
+record_declaration: [
+| record_fields
+]
+
+record_fields: [
+| record_field_declaration ";" record_fields
+| record_field_declaration
+|
+| record_field ";" record_fields
+| record_field ";"
+| record_field
+]
+
+record_field_declaration: [
+| global binders ":=" lconstr
+]
+
+binder_constr: [
+| "forall" open_binders "," operconstr200
+| "fun" open_binders "=>" operconstr200
+| "let" name binders type_cstr ":=" operconstr200 "in" operconstr200
+| "let" single_fix "in" operconstr200
+| "let" [ "(" LIST0 name SEP "," ")" | "()" ] return_type ":=" operconstr200 "in" operconstr200
+| "let" "'" pattern200 ":=" operconstr200 "in" operconstr200
+| "let" "'" pattern200 ":=" operconstr200 case_type "in" operconstr200
+| "let" "'" pattern200 "in" pattern200 ":=" operconstr200 case_type "in" operconstr200
+| "if" operconstr200 return_type "then" operconstr200 "else" operconstr200
+| fix_constr
+| "if" operconstr200 "is" ssr_dthen ssr_else      (* ssr plugin *)
+| "if" operconstr200 "isn't" ssr_dthen ssr_else      (* ssr plugin *)
+| "let" ":" ssr_mpat ":=" lconstr "in" lconstr      (* ssr plugin *)
+| "let" ":" ssr_mpat ":=" lconstr ssr_rtype "in" lconstr      (* ssr plugin *)
+| "let" ":" ssr_mpat "in" pattern200 ":=" lconstr ssr_rtype "in" lconstr      (* ssr plugin *)
+]
+
+appl_arg: [
+| lpar_id_coloneq lconstr ")"
+| operconstr9
+]
+
+atomic_constr: [
+| global instance
+| sort
+| NUMERAL
+| string
+| "_"
+| "?" "[" ident "]"
+| "?" "[" pattern_ident "]"
+| pattern_ident evar_instance
+]
+
+inst: [
+| ident ":=" lconstr
+]
+
+evar_instance: [
+| "@{" LIST1 inst SEP ";" "}"
+|
+]
+
+instance: [
+| "@{" LIST0 universe_level "}"
+|
+]
+
+universe_level: [
+| "Set"
+| "Prop"
+| "Type"
+| "_"
+| global
+]
+
+fix_constr: [
+| single_fix
+| single_fix "with" LIST1 fix_decl SEP "with" "for" identref
+]
+
+single_fix: [
+| fix_kw fix_decl
+]
+
+fix_kw: [
+| "fix"
+| "cofix"
+]
+
+fix_decl: [
+| identref binders_fixannot type_cstr ":=" operconstr200
+]
+
+match_constr: [
+| "match" LIST1 case_item SEP "," OPT case_type "with" branches "end"
+]
+
+case_item: [
+| operconstr100 OPT [ "as" name ] OPT [ "in" pattern200 ]
+]
+
+case_type: [
+| "return" operconstr100
+]
+
+return_type: [
+| OPT [ OPT [ "as" name ] case_type ]
+]
+
+branches: [
+| OPT "|" LIST0 eqn SEP "|"
+]
+
+mult_pattern: [
+| LIST1 pattern200 SEP ","
+]
+
+eqn: [
+| LIST1 mult_pattern SEP "|" "=>" lconstr
+]
+
+record_pattern: [
+| global ":=" pattern200
+]
+
+record_patterns: [
+| record_pattern ";" record_patterns
+| record_pattern ";"
+| record_pattern
+|
+]
+
+pattern200: [
+| pattern100
+]
+
+pattern100: [
+| pattern99 ":" binder_constr
+| pattern99 ":" operconstr100
+| pattern99
+]
+
+pattern99: [
+| pattern90
+]
+
+pattern90: [
+| pattern10
+]
+
+pattern10: [
+| pattern1 "as" name
+| pattern1 LIST1 pattern1
+| "@" Prim.reference LIST0 pattern1
+| pattern1
+]
+
+pattern1: [
+| pattern0 "%" IDENT
+| pattern0
+]
+
+pattern0: [
+| Prim.reference
+| "{|" record_patterns bar_cbrace
+| "_"
+| "(" pattern200 ")"
+| "(" pattern200 "|" LIST1 pattern200 SEP "|" ")"
+| NUMERAL
+| string
+]
+
+impl_ident_tail: [
+| "}"
+| LIST1 name ":" lconstr "}"
+| LIST1 name "}"
+| ":" lconstr "}"
+]
+
+fixannot: [
+| "{" "struct" identref "}"
+| "{" "wf" constr identref "}"
+| "{" "measure" constr OPT identref OPT constr "}"
+| "{" "struct" name "}"
+|
+]
+
+impl_name_head: [
+| impl_ident_head
+]
+
+binders_fixannot: [
+| impl_name_head impl_ident_tail binders_fixannot
+| fixannot
+| binder binders_fixannot
+|
+]
+
+open_binders: [
+| name LIST0 name ":" lconstr
+| name LIST0 name binders
+| name ".." name
+| closed_binder binders
+]
+
+binders: [
+| LIST0 binder
+| Pcoq.Constr.binders
+]
+
+binder: [
+| name
+| closed_binder
+]
+
+closed_binder: [
+| "(" name LIST1 name ":" lconstr ")"
+| "(" name ":" lconstr ")"
+| "(" name ":=" lconstr ")"
+| "(" name ":" lconstr ":=" lconstr ")"
+| "{" name "}"
+| "{" name LIST1 name ":" lconstr "}"
+| "{" name ":" lconstr "}"
+| "{" name LIST1 name "}"
+| "`(" LIST1 typeclass_constraint SEP "," ")"
+| "`{" LIST1 typeclass_constraint SEP "," "}"
+| "'" pattern0
+| [ "of" | "&" ] operconstr99      (* ssr plugin *)
+]
+
+typeclass_constraint: [
+| "!" operconstr200
+| "{" name "}" ":" [ "!" | ] operconstr200
+| name_colon [ "!" | ] operconstr200
+| operconstr200
+]
+
+type_cstr: [
+| OPT [ ":" lconstr ]
+| ":" lconstr
+|
+]
+
+preident: [
+| IDENT
+]
+
+ident: [
+| IDENT
+]
+
+pattern_ident: [
+| LEFTQMARK ident
+]
+
+pattern_identref: [
+| pattern_ident
+]
+
+var: [
+| ident
+]
+
+identref: [
+| ident
+]
+
+field: [
+| FIELD
+]
+
+fields: [
+| field fields
+| field
+]
+
+fullyqualid: [
+| ident fields
+| ident
+]
+
+basequalid: [
+| ident fields
+| ident
+]
+
+name: [
+| "_"
+| ident
+]
+
+reference: [
+| ident fields
+| ident
+]
+
+by_notation: [
+| ne_string OPT [ "%" IDENT ]
+]
+
+smart_global: [
+| reference
+| by_notation
+]
+
+qualid: [
+| basequalid
+]
+
+ne_string: [
+| STRING
+]
+
+ne_lstring: [
+| ne_string
+]
+
+dirpath: [
+| ident LIST0 field
+]
+
+string: [
+| STRING
+]
+
+lstring: [
+| string
+]
+
+integer: [
+| NUMERAL
+| "-" NUMERAL
+]
+
+natural: [
+| NUMERAL
+| _natural
+]
+
+bigint: [
+| NUMERAL
+]
+
+bar_cbrace: [
+| "|" "}"
+]
+
+vernac_toplevel: [
+| "Drop" "."
+| "Quit" "."
+| "Backtrack" natural natural natural "."
+| test_show_goal "Show" "Goal" natural "at" natural "."
+| Pvernac.Vernac_.main_entry
+]
+
+opt_hintbases: [
+|
+| ":" LIST1 IDENT
+]
+
+command: [
+| "Goal" lconstr
+| "Proof"
+| "Proof" "Mode" string
+| "Proof" lconstr
+| "Abort"
+| "Abort" "All"
+| "Abort" identref
+| "Existential" natural constr_body
+| "Admitted"
+| "Qed"
+| "Save" identref
+| "Defined"
+| "Defined" identref
+| "Restart"
+| "Undo"
+| "Undo" natural
+| "Undo" "To" natural
+| "Focus"
+| "Focus" natural
+| "Unfocus"
+| "Unfocused"
+| "Show"
+| "Show" natural
+| "Show" ident
+| "Show" "Existentials"
+| "Show" "Universes"
+| "Show" "Conjectures"
+| "Show" "Proof"
+| "Show" "Intro"
+| "Show" "Intros"
+| "Show" "Match" reference
+| "Guarded"
+| "Create" "HintDb" IDENT; [ "discriminated" | ]
+| "Remove" "Hints" LIST1 global opt_hintbases
+| "Hint" hint opt_hintbases
+| "Comments" LIST0 comment
+| "Declare" "Instance" ident_decl binders ":" operconstr200 hint_info
+| "Declare" "Scope" IDENT
+| "Pwd"
+| "Cd"
+| "Cd" ne_string
+| "Load" [ "Verbose" | ] [ ne_string | IDENT ]
+| "Declare" "ML" "Module" LIST1 ne_string
+| "Locate" locatable
+| "Add" "LoadPath" ne_string as_dirpath
+| "Add" "Rec" "LoadPath" ne_string as_dirpath
+| "Remove" "LoadPath" ne_string
+| "AddPath" ne_string "as" as_dirpath
+| "AddRecPath" ne_string "as" as_dirpath
+| "DelPath" ne_string
+| "Type" lconstr
+| "Print" printable
+| "Print" smart_global OPT univ_name_list
+| "Print" "Module" "Type" global
+| "Print" "Module" global
+| "Print" "Namespace" dirpath
+| "Inspect" natural
+| "Add" "ML" "Path" ne_string
+| "Add" "Rec" "ML" "Path" ne_string
+| "Set" option_table option_setting
+| "Unset" option_table
+| "Print" "Table" option_table
+| "Add" IDENT IDENT LIST1 option_ref_value
+| "Add" IDENT LIST1 option_ref_value
+| "Test" option_table "for" LIST1 option_ref_value
+| "Test" option_table
+| "Remove" IDENT IDENT LIST1 option_ref_value
+| "Remove" IDENT LIST1 option_ref_value
+| "Write" "State" IDENT
+| "Write" "State" ne_string
+| "Restore" "State" IDENT
+| "Restore" "State" ne_string
+| "Reset" "Initial"
+| "Reset" identref
+| "Back"
+| "Back" natural
+| "BackTo" natural
+| "Debug" "On"
+| "Debug" "Off"
+| "Declare" "Reduction" IDENT; ":=" red_expr
+| "Declare" "Custom" "Entry" IDENT
+| "Derive" ident "SuchThat" constr "As" ident      (* derive plugin *)
+| "Extraction" global      (* extraction plugin *)
+| "Recursive" "Extraction" LIST1 global      (* extraction plugin *)
+| "Extraction" string LIST1 global      (* extraction plugin *)
+| "Extraction" "TestCompile" LIST1 global      (* extraction plugin *)
+| "Separate" "Extraction" LIST1 global      (* extraction plugin *)
+| "Extraction" "Library" ident      (* extraction plugin *)
+| "Recursive" "Extraction" "Library" ident      (* extraction plugin *)
+| "Extraction" "Language" language      (* extraction plugin *)
+| "Extraction" "Inline" LIST1 global      (* extraction plugin *)
+| "Extraction" "NoInline" LIST1 global      (* extraction plugin *)
+| "Print" "Extraction" "Inline"      (* extraction plugin *)
+| "Reset" "Extraction" "Inline"      (* extraction plugin *)
+| "Extraction" "Implicit" global "[" LIST0 int_or_id "]"      (* extraction plugin *)
+| "Extraction" "Blacklist" LIST1 ident      (* extraction plugin *)
+| "Print" "Extraction" "Blacklist"      (* extraction plugin *)
+| "Reset" "Extraction" "Blacklist"      (* extraction plugin *)
+| "Extract" "Constant" global LIST0 string "=>" mlname      (* extraction plugin *)
+| "Extract" "Inlined" "Constant" global "=>" mlname      (* extraction plugin *)
+| "Extract" "Inductive" global "=>" mlname "[" LIST0 mlname "]" OPT string      (* extraction plugin *)
+| "Show" "Extraction"      (* extraction plugin *)
+| "Set" "Firstorder" "Solver" tactic
+| "Print" "Firstorder" "Solver"
+| "Function" LIST1 function_rec_definition_loc SEP "with"      (* funind plugin *)
+| "Functional" "Scheme" LIST1 fun_scheme_arg SEP "with"      (* funind plugin *)
+| "Functional" "Case" fun_scheme_arg      (* funind plugin *)
+| "Generate" "graph" "for" reference      (* funind plugin *)
+| "Hint" "Rewrite" orient LIST1 constr ":" LIST0 preident
+| "Hint" "Rewrite" orient LIST1 constr "using" tactic ":" LIST0 preident
+| "Hint" "Rewrite" orient LIST1 constr
+| "Hint" "Rewrite" orient LIST1 constr "using" tactic
+| "Derive" "Inversion_clear" ident "with" constr "Sort" sort_family
+| "Derive" "Inversion_clear" ident "with" constr
+| "Derive" "Inversion" ident "with" constr "Sort" sort_family
+| "Derive" "Inversion" ident "with" constr
+| "Derive" "Dependent" "Inversion" ident "with" constr "Sort" sort_family
+| "Derive" "Dependent" "Inversion_clear" ident "with" constr "Sort" sort_family
+| "Declare" "Left" "Step" constr
+| "Declare" "Right" "Step" constr
+| "Grab" "Existential" "Variables"
+| "Unshelve"
+| "Declare" "Equivalent" "Keys" constr constr
+| "Print" "Equivalent" "Keys"
+| "Optimize" "Proof"
+| "Optimize" "Heap"
+| "Hint" "Cut" "[" hints_path "]" opthints
+| "Typeclasses" "Transparent" LIST0 reference
+| "Typeclasses" "Opaque" LIST0 reference
+| "Typeclasses" "eauto" ":=" debug eauto_search_strategy OPT int
+| "Proof" "with" Pltac.tactic OPT [ "using" G_vernac.section_subset_expr ]
+| "Proof" "using" G_vernac.section_subset_expr OPT [ "with" Pltac.tactic ]
+| "Tactic" "Notation" OPT ltac_tactic_level LIST1 ltac_production_item ":=" tactic
+| "Print" "Ltac" reference
+| "Locate" "Ltac" reference
+| "Ltac" LIST1 ltac_tacdef_body SEP "with"
+| "Print" "Ltac" "Signatures"
+| "Obligation" integer "of" ident ":" lglob withtac
+| "Obligation" integer "of" ident withtac
+| "Obligation" integer ":" lglob withtac
+| "Obligation" integer withtac
+| "Next" "Obligation" "of" ident withtac
+| "Next" "Obligation" withtac
+| "Solve" "Obligation" integer "of" ident "with" tactic
+| "Solve" "Obligation" integer "with" tactic
+| "Solve" "Obligations" "of" ident "with" tactic
+| "Solve" "Obligations" "with" tactic
+| "Solve" "Obligations"
+| "Solve" "All" "Obligations" "with" tactic
+| "Solve" "All" "Obligations"
+| "Admit" "Obligations" "of" ident
+| "Admit" "Obligations"
+| "Obligation" "Tactic" ":=" tactic
+| "Show" "Obligation" "Tactic"
+| "Obligations" "of" ident
+| "Obligations"
+| "Preterm" "of" ident
+| "Preterm"
+| "Add" "Relation" constr constr "reflexivity" "proved" "by" constr "symmetry" "proved" "by" constr "as" ident
+| "Add" "Relation" constr constr "reflexivity" "proved" "by" constr "as" ident
+| "Add" "Relation" constr constr "as" ident
+| "Add" "Relation" constr constr "symmetry" "proved" "by" constr "as" ident
+| "Add" "Relation" constr constr "symmetry" "proved" "by" constr "transitivity" "proved" "by" constr "as" ident
+| "Add" "Relation" constr constr "reflexivity" "proved" "by" constr "transitivity" "proved" "by" constr "as" ident
+| "Add" "Relation" constr constr "reflexivity" "proved" "by" constr "symmetry" "proved" "by" constr "transitivity" "proved" "by" constr "as" ident
+| "Add" "Relation" constr constr "transitivity" "proved" "by" constr "as" ident
+| "Add" "Parametric" "Relation" binders ":" constr constr "reflexivity" "proved" "by" constr "symmetry" "proved" "by" constr "as" ident
+| "Add" "Parametric" "Relation" binders ":" constr constr "reflexivity" "proved" "by" constr "as" ident
+| "Add" "Parametric" "Relation" binders ":" constr constr "as" ident
+| "Add" "Parametric" "Relation" binders ":" constr constr "symmetry" "proved" "by" constr "as" ident
+| "Add" "Parametric" "Relation" binders ":" constr constr "symmetry" "proved" "by" constr "transitivity" "proved" "by" constr "as" ident
+| "Add" "Parametric" "Relation" binders ":" constr constr "reflexivity" "proved" "by" constr "transitivity" "proved" "by" constr "as" ident
+| "Add" "Parametric" "Relation" binders ":" constr constr "reflexivity" "proved" "by" constr "symmetry" "proved" "by" constr "transitivity" "proved" "by" constr "as" ident
+| "Add" "Parametric" "Relation" binders ":" constr constr "transitivity" "proved" "by" constr "as" ident
+| "Add" "Setoid" constr constr constr "as" ident
+| "Add" "Parametric" "Setoid" binders ":" constr constr constr "as" ident
+| "Add" "Morphism" constr ":" ident
+| "Declare" "Morphism" constr ":" ident
+| "Add" "Morphism" constr "with" "signature" lconstr "as" ident
+| "Add" "Parametric" "Morphism" binders ":" constr "with" "signature" lconstr "as" ident
+| "Print" "Rewrite" "HintDb" preident
+| "Reset" "Ltac" "Profile"
+| "Show" "Ltac" "Profile"
+| "Show" "Ltac" "Profile" "CutOff" int
+| "Show" "Ltac" "Profile" string
+| "Add" "Ring" ident ":" constr OPT ring_mods      (* setoid_ring plugin *)
+| "Print" "Rings"      (* setoid_ring plugin *)
+| "Add" "Field" ident ":" constr OPT field_mods      (* setoid_ring plugin *)
+| "Print" "Fields"      (* setoid_ring plugin *)
+| "Prenex" "Implicits" LIST1 global      (* ssr plugin *)
+| "Search" ssr_search_arg ssr_modlocs      (* ssr plugin *)
+| "Print" "Hint" "View" ssrviewpos      (* ssr plugin *)
+| "Hint" "View" ssrviewposspc LIST1 ssrhintref      (* ssr plugin *)
+| "Numeral" "Notation" reference reference reference ":" ident numnotoption
+| "String" "Notation" reference reference reference ":" ident
+]
+
+reference_or_constr: [
+| global
+| constr
+]
+
+hint: [
+| "Resolve" LIST1 reference_or_constr hint_info
+| "Resolve" "->" LIST1 global OPT natural
+| "Resolve" "<-" LIST1 global OPT natural
+| "Immediate" LIST1 reference_or_constr
+| "Variables" "Transparent"
+| "Variables" "Opaque"
+| "Constants" "Transparent"
+| "Constants" "Opaque"
+| "Transparent" LIST1 global
+| "Opaque" LIST1 global
+| "Mode" global mode
+| "Unfold" LIST1 global
+| "Constructors" LIST1 global
+| "Extern" natural OPT Constr.constr_pattern "=>" Pltac.tactic
+]
+
+constr_body: [
+| ":=" lconstr
+| ":" lconstr ":=" lconstr
+]
+
+mode: [
+| LIST1 [ "+" | "!" | "-" ]
+]
+
+vernac_control: [
+| "Time" vernac_control
+| "Redirect" ne_string vernac_control
+| "Timeout" natural vernac_control
+| "Fail" vernac_control
+| decorated_vernac
+]
+
+decorated_vernac: [
+| LIST0 quoted_attributes vernac
+]
+
+quoted_attributes: [
+| "#[" attribute_list "]"
+]
+
+attribute_list: [
+| LIST0 attribute SEP ","
+]
+
+attribute: [
+| ident attribute_value
+]
+
+attribute_value: [
+| "=" string
+| "(" attribute_list ")"
+|
+]
+
+vernac: [
+| "Local" vernac_poly
+| "Global" vernac_poly
+| vernac_poly
+]
+
+vernac_poly: [
+| "Polymorphic" vernac_aux
+| "Monomorphic" vernac_aux
+| vernac_aux
+]
+
+vernac_aux: [
+| "Program" gallina "."
+| "Program" gallina_ext "."
+| gallina "."
+| gallina_ext "."
+| command "."
+| syntax "."
+| subprf
+| command_entry
+]
+
+noedit_mode: [
+| query_command
+]
+
+subprf: [
+| BULLET
+| "{"
+| "}"
+]
+
+gallina: [
+| thm_token ident_decl binders ":" lconstr LIST0 [ "with" ident_decl binders ":" lconstr ]
+| assumption_token inline assum_list
+| assumptions_token inline assum_list
+| def_token ident_decl def_body
+| "Let" identref def_body
+| OPT cumulativity_token private_token finite_token LIST1 inductive_definition SEP "with"
+| "Fixpoint" LIST1 rec_definition SEP "with"
+| "Let" "Fixpoint" LIST1 rec_definition SEP "with"
+| "CoFixpoint" LIST1 corec_definition SEP "with"
+| "Let" "CoFixpoint" LIST1 corec_definition SEP "with"
+| "Scheme" LIST1 scheme SEP "with"
+| "Combined" "Scheme" identref "from" LIST1 identref SEP ","
+| "Register" global "as" qualid
+| "Register" "Inline" global
+| "Primitive" identref OPT [ ":" lconstr ] ":=" register_token
+| "Universe" LIST1 identref
+| "Universes" LIST1 identref
+| "Constraint" LIST1 univ_constraint SEP ","
+]
+
+register_token: [
+| register_prim_token
+| register_type_token
+]
+
+register_type_token: [
+| "#int63_type"
+]
+
+register_prim_token: [
+| "#int63_head0"
+| "#int63_tail0"
+| "#int63_add"
+| "#int63_sub"
+| "#int63_mul"
+| "#int63_div"
+| "#int63_mod"
+| "#int63_lsr"
+| "#int63_lsl"
+| "#int63_land"
+| "#int63_lor"
+| "#int63_lxor"
+| "#int63_addc"
+| "#int63_subc"
+| "#int63_addcarryc"
+| "#int63_subcarryc"
+| "#int63_mulc"
+| "#int63_diveucl"
+| "#int63_div21"
+| "#int63_addmuldiv"
+| "#int63_eq"
+| "#int63_lt"
+| "#int63_le"
+| "#int63_compare"
+]
+
+thm_token: [
+| "Theorem"
+| "Lemma"
+| "Fact"
+| "Remark"
+| "Corollary"
+| "Proposition"
+| "Property"
+]
+
+def_token: [
+| "Definition"
+| "Example"
+| "SubClass"
+]
+
+assumption_token: [
+| "Hypothesis"
+| "Variable"
+| "Axiom"
+| "Parameter"
+| "Conjecture"
+]
+
+assumptions_token: [
+| "Hypotheses"
+| "Variables"
+| "Axioms"
+| "Parameters"
+| "Conjectures"
+]
+
+inline: [
+| "Inline" "(" natural ")"
+| "Inline"
+|
+]
+
+univ_constraint: [
+| universe_name [ "<" | "=" | "<=" ] universe_name
+]
+
+univ_decl: [
+| "@{" LIST0 identref [ "+" | ] [ "|" LIST0 univ_constraint SEP "," [ "+" | ] "}" | [ "}" | bar_cbrace ] ]
+]
+
+ident_decl: [
+| identref OPT univ_decl
+]
+
+finite_token: [
+| "Inductive"
+| "CoInductive"
+| "Variant"
+| "Record"
+| "Structure"
+| "Class"
+]
+
+cumulativity_token: [
+| "Cumulative"
+| "NonCumulative"
+]
+
+private_token: [
+| "Private"
+|
+]
+
+def_body: [
+| binders ":=" reduce lconstr
+| binders ":" lconstr ":=" reduce lconstr
+| binders ":" lconstr
+]
+
+reduce: [
+| "Eval" red_expr "in"
+|
+]
+
+one_decl_notation: [
+| ne_lstring ":=" constr OPT [ ":" IDENT ]
+]
+
+decl_sep: [
+| "and"
+]
+
+decl_notation: [
+| "where" LIST1 one_decl_notation SEP decl_sep
+|
+]
+
+opt_constructors_or_fields: [
+| ":=" constructor_list_or_record_decl
+|
+]
+
+inductive_definition: [
+| opt_coercion ident_decl binders OPT [ ":" lconstr ] opt_constructors_or_fields decl_notation
+]
+
+constructor_list_or_record_decl: [
+| "|" LIST1 constructor SEP "|"
+| identref constructor_type "|" LIST0 constructor SEP "|"
+| identref constructor_type
+| identref "{" record_fields "}"
+| "{" record_fields "}"
+|
+]
+
+opt_coercion: [
+| ">"
+|
+]
+
+rec_definition: [
+| ident_decl binders_fixannot type_cstr OPT [ ":=" lconstr ] decl_notation
+]
+
+corec_definition: [
+| ident_decl binders type_cstr OPT [ ":=" lconstr ] decl_notation
+]
+
+scheme: [
+| scheme_kind
+| identref ":=" scheme_kind
+]
+
+scheme_kind: [
+| "Induction" "for" smart_global "Sort" sort_family
+| "Minimality" "for" smart_global "Sort" sort_family
+| "Elimination" "for" smart_global "Sort" sort_family
+| "Case" "for" smart_global "Sort" sort_family
+| "Equality" "for" smart_global
+]
+
+record_field: [
+| LIST0 quoted_attributes record_binder OPT [ "|" natural ] decl_notation
+]
+
+record_binder_body: [
+| binders of_type_with_opt_coercion lconstr
+| binders of_type_with_opt_coercion lconstr ":=" lconstr
+| binders ":=" lconstr
+]
+
+record_binder: [
+| name
+| name record_binder_body
+]
+
+assum_list: [
+| LIST1 assum_coe
+| simple_assum_coe
+]
+
+assum_coe: [
+| "(" simple_assum_coe ")"
+]
+
+simple_assum_coe: [
+| LIST1 ident_decl of_type_with_opt_coercion lconstr
+]
+
+constructor_type: [
+| binders [ of_type_with_opt_coercion lconstr | ]
+]
+
+constructor: [
+| identref constructor_type
+]
+
+of_type_with_opt_coercion: [
+| ":>>"
+| ":>" ">"
+| ":>"
+| ":" ">" ">"
+| ":" ">"
+| ":"
+]
+
+gallina_ext: [
+| "Module" export_token identref LIST0 module_binder of_module_type is_module_expr
+| "Module" "Type" identref LIST0 module_binder check_module_types is_module_type
+| "Declare" "Module" export_token identref LIST0 module_binder ":" module_type_inl
+| "Section" identref
+| "Chapter" identref
+| "End" identref
+| "Collection" identref ":=" section_subset_expr
+| "Require" export_token LIST1 global
+| "From" global "Require" export_token LIST1 global
+| "Import" LIST1 global
+| "Export" LIST1 global
+| "Include" module_type_inl LIST0 ext_module_expr
+| "Include" "Type" module_type_inl LIST0 ext_module_type
+| "Transparent" LIST1 smart_global
+| "Opaque" LIST1 smart_global
+| "Strategy" LIST1 [ strategy_level "[" LIST1 smart_global "]" ]
+| "Canonical" OPT "Structure" global OPT [ OPT univ_decl def_body ]
+| "Canonical" OPT "Structure" by_notation
+| "Coercion" global OPT univ_decl def_body
+| "Identity" "Coercion" identref ":" class_rawexpr ">->" class_rawexpr
+| "Coercion" global ":" class_rawexpr ">->" class_rawexpr
+| "Coercion" by_notation ":" class_rawexpr ">->" class_rawexpr
+| "Context" LIST1 binder
+| "Instance" instance_name ":" operconstr200 hint_info [ ":=" "{" record_declaration "}" | ":=" lconstr | ]
+| "Existing" "Instance" global hint_info
+| "Existing" "Instances" LIST1 global OPT [ "|" natural ]
+| "Existing" "Class" global
+| "Arguments" smart_global LIST0 argument_spec_block OPT [ "," LIST1 [ LIST0 more_implicits_block ] SEP "," ] OPT [ ":" LIST1 arguments_modifier SEP "," ]
+| "Implicit" "Type" reserv_list
+| "Implicit" "Types" reserv_list
+| "Generalizable" [ "All" "Variables" | "No" "Variables" | [ "Variable" | "Variables" ] LIST1 identref ]
+| "Export" "Set" option_table option_setting
+| "Export" "Unset" option_table
+| "Import" "Prenex" "Implicits"      (* ssr plugin *)
+]
+
+export_token: [
+| "Import"
+| "Export"
+|
+]
+
+ext_module_type: [
+| "<+" module_type_inl
+]
+
+ext_module_expr: [
+| "<+" module_expr_inl
+]
+
+check_module_type: [
+| "<:" module_type_inl
+]
+
+check_module_types: [
+| LIST0 check_module_type
+]
+
+of_module_type: [
+| ":" module_type_inl
+| check_module_types
+]
+
+is_module_type: [
+| ":=" module_type_inl LIST0 ext_module_type
+|
+]
+
+is_module_expr: [
+| ":=" module_expr_inl LIST0 ext_module_expr
+|
+]
+
+functor_app_annot: [
+| "[" "inline" "at" "level" natural "]"
+| "[" "no" "inline" "]"
+|
+]
+
+module_expr_inl: [
+| "!" module_expr
+| module_expr functor_app_annot
+]
+
+module_type_inl: [
+| "!" module_type
+| module_type functor_app_annot
+]
+
+module_binder: [
+| "(" export_token LIST1 identref ":" module_type_inl ")"
+]
+
+module_expr: [
+| module_expr_atom
+| module_expr module_expr_atom
+]
+
+module_expr_atom: [
+| qualid
+| "(" module_expr ")"
+]
+
+with_declaration: [
+| "Definition" fullyqualid OPT univ_decl ":=" Constr.lconstr
+| "Module" fullyqualid ":=" qualid
+]
+
+module_type: [
+| qualid
+| "(" module_type ")"
+| module_type module_expr_atom
+| module_type "with" with_declaration
+]
+
+section_subset_expr: [
+| only_starredidentrefs LIST0 starredidentref
+| ssexpr35
+]
+
+starredidentref: [
+| identref
+| identref "*"
+| "Type"
+| "Type" "*"
+]
+
+ssexpr35: [
+| "-" ssexpr50
+| ssexpr50
+]
+
+ssexpr50: [
+| ssexpr0 "-" ssexpr0
+| ssexpr0 "+" ssexpr0
+| ssexpr0
+]
+
+ssexpr0: [
+| starredidentref
+| "(" only_starredidentrefs LIST0 starredidentref ")"
+| "(" only_starredidentrefs LIST0 starredidentref ")" "*"
+| "(" ssexpr35 ")"
+| "(" ssexpr35 ")" "*"
+]
+
+arguments_modifier: [
+| "simpl" "nomatch"
+| "simpl" "never"
+| "default" "implicits"
+| "clear" "implicits"
+| "clear" "scopes"
+| "clear" "bidirectionality" "hint"
+| "rename"
+| "assert"
+| "extra" "scopes"
+| "clear" "scopes" "and" "implicits"
+| "clear" "implicits" "and" "scopes"
+]
+
+scope: [
+| "%" IDENT
+]
+
+argument_spec: [
+| OPT "!" name OPT scope
+]
+
+argument_spec_block: [
+| argument_spec
+| "/"
+| "&"
+| "(" LIST1 argument_spec ")" OPT scope
+| "[" LIST1 argument_spec "]" OPT scope
+| "{" LIST1 argument_spec "}" OPT scope
+]
+
+more_implicits_block: [
+| name
+| "[" LIST1 name "]"
+| "{" LIST1 name "}"
+]
+
+strategy_level: [
+| "expand"
+| "opaque"
+| integer
+| "transparent"
+]
+
+instance_name: [
+| ident_decl binders
+|
+]
+
+hint_info: [
+| "|" OPT natural OPT constr_pattern
+|
+]
+
+reserv_list: [
+| LIST1 reserv_tuple
+| simple_reserv
+]
+
+reserv_tuple: [
+| "(" simple_reserv ")"
+]
+
+simple_reserv: [
+| LIST1 identref ":" lconstr
+]
+
+query_command: [
+| "Eval" red_expr "in" lconstr "."
+| "Compute" lconstr "."
+| "Check" lconstr "."
+| "About" smart_global OPT univ_name_list "."
+| "SearchHead" constr_pattern in_or_out_modules "."
+| "SearchPattern" constr_pattern in_or_out_modules "."
+| "SearchRewrite" constr_pattern in_or_out_modules "."
+| "Search" searchabout_query searchabout_queries "."
+| "SearchAbout" searchabout_query searchabout_queries "."
+| "SearchAbout" "[" LIST1 searchabout_query "]" in_or_out_modules "."
+]
+
+printable: [
+| "Term" smart_global OPT univ_name_list
+| "All"
+| "Section" global
+| "Grammar" IDENT
+| "Custom" "Grammar" IDENT
+| "LoadPath" OPT dirpath
+| "Modules"
+| "Libraries"
+| "ML" "Path"
+| "ML" "Modules"
+| "Debug" "GC"
+| "Graph"
+| "Classes"
+| "TypeClasses"
+| "Instances" smart_global
+| "Coercions"
+| "Coercion" "Paths" class_rawexpr class_rawexpr
+| "Canonical" "Projections"
+| "Tables"
+| "Options"
+| "Hint"
+| "Hint" smart_global
+| "Hint" "*"
+| "HintDb" IDENT
+| "Scopes"
+| "Scope" IDENT
+| "Visibility" OPT IDENT
+| "Implicit" smart_global
+| [ "Sorted" | ] "Universes" OPT printunivs_subgraph OPT ne_string
+| "Assumptions" smart_global
+| "Opaque" "Dependencies" smart_global
+| "Transparent" "Dependencies" smart_global
+| "All" "Dependencies" smart_global
+| "Strategy" smart_global
+| "Strategies"
+| "Registered"
+]
+
+printunivs_subgraph: [
+| "Subgraph" "(" LIST0 reference ")"
+]
+
+class_rawexpr: [
+| "Funclass"
+| "Sortclass"
+| smart_global
+]
+
+locatable: [
+| smart_global
+| "Term" smart_global
+| "File" ne_string
+| "Library" global
+| "Module" global
+]
+
+option_setting: [
+|
+| integer
+| STRING
+]
+
+option_ref_value: [
+| global
+| STRING
+]
+
+option_table: [
+| LIST1 IDENT
+]
+
+as_dirpath: [
+| OPT [ "as" dirpath ]
+]
+
+ne_in_or_out_modules: [
+| "inside" LIST1 global
+| "outside" LIST1 global
+]
+
+in_or_out_modules: [
+| ne_in_or_out_modules
+|
+]
+
+comment: [
+| constr
+| STRING
+| natural
+]
+
+positive_search_mark: [
+| "-"
+|
+]
+
+searchabout_query: [
+| positive_search_mark ne_string OPT scope
+| positive_search_mark constr_pattern
+]
+
+searchabout_queries: [
+| ne_in_or_out_modules
+| searchabout_query searchabout_queries
+|
+]
+
+univ_name_list: [
+| "@{" LIST0 name "}"
+]
+
+syntax: [
+| "Open" "Scope" IDENT
+| "Close" "Scope" IDENT
+| "Delimit" "Scope" IDENT; "with" IDENT
+| "Undelimit" "Scope" IDENT
+| "Bind" "Scope" IDENT; "with" LIST1 class_rawexpr
+| "Infix" ne_lstring ":=" constr [ "(" LIST1 syntax_modifier SEP "," ")" | ] OPT [ ":" IDENT ]
+| "Notation" identref LIST0 ident ":=" constr only_parsing
+| "Notation" lstring ":=" constr [ "(" LIST1 syntax_modifier SEP "," ")" | ] OPT [ ":" IDENT ]
+| "Format" "Notation" STRING STRING STRING
+| "Reserved" "Infix" ne_lstring [ "(" LIST1 syntax_modifier SEP "," ")" | ]
+| "Reserved" "Notation" ne_lstring [ "(" LIST1 syntax_modifier SEP "," ")" | ]
+]
+
+only_parsing: [
+| "(" "only" "parsing" ")"
+| "(" "compat" STRING ")"
+|
+]
+
+level: [
+| "level" natural
+| "next" "level"
+]
+
+syntax_modifier: [
+| "at" "level" natural
+| "in" "custom" IDENT
+| "in" "custom" IDENT; "at" "level" natural
+| "left" "associativity"
+| "right" "associativity"
+| "no" "associativity"
+| "only" "printing"
+| "only" "parsing"
+| "compat" STRING
+| "format" STRING OPT STRING
+| IDENT; "," LIST1 IDENT SEP "," "at" level
+| IDENT; "at" level
+| IDENT; "at" level constr_as_binder_kind
+| IDENT constr_as_binder_kind
+| IDENT syntax_extension_type
+]
+
+syntax_extension_type: [
+| "ident"
+| "global"
+| "bigint"
+| "binder"
+| "constr"
+| "constr" OPT at_level OPT constr_as_binder_kind
+| "pattern"
+| "pattern" "at" "level" natural
+| "strict" "pattern"
+| "strict" "pattern" "at" "level" natural
+| "closed" "binder"
+| "custom" IDENT OPT at_level OPT constr_as_binder_kind
+]
+
+at_level: [
+| "at" level
+]
+
+constr_as_binder_kind: [
+| "as" "ident"
+| "as" "pattern"
+| "as" "strict" "pattern"
+]
+
+simple_tactic: [
+| "btauto"
+| "congruence"
+| "congruence" integer
+| "congruence" "with" LIST1 constr
+| "congruence" integer "with" LIST1 constr
+| "f_equal"
+| "firstorder" OPT tactic firstorder_using
+| "firstorder" OPT tactic "with" LIST1 preident
+| "firstorder" OPT tactic firstorder_using "with" LIST1 preident
+| "gintuition" OPT tactic
+| "functional" "inversion" quantified_hypothesis OPT reference      (* funind plugin *)
+| "functional" "induction" LIST1 constr fun_ind_using with_names      (* funind plugin *)
+| "soft" "functional" "induction" LIST1 constr fun_ind_using with_names      (* funind plugin *)
+| "reflexivity"
+| "exact" casted_constr
+| "assumption"
+| "etransitivity"
+| "cut" constr
+| "exact_no_check" constr
+| "vm_cast_no_check" constr
+| "native_cast_no_check" constr
+| "casetype" constr
+| "elimtype" constr
+| "lapply" constr
+| "transitivity" constr
+| "left"
+| "eleft"
+| "left" "with" bindings
+| "eleft" "with" bindings
+| "right"
+| "eright"
+| "right" "with" bindings
+| "eright" "with" bindings
+| "constructor"
+| "constructor" int_or_var
+| "constructor" int_or_var "with" bindings
+| "econstructor"
+| "econstructor" int_or_var
+| "econstructor" int_or_var "with" bindings
+| "specialize" constr_with_bindings
+| "specialize" constr_with_bindings "as" simple_intropattern
+| "symmetry"
+| "symmetry" "in" in_clause
+| "split"
+| "esplit"
+| "split" "with" bindings
+| "esplit" "with" bindings
+| "exists"
+| "exists" LIST1 bindings SEP ","
+| "eexists"
+| "eexists" LIST1 bindings SEP ","
+| "intros" "until" quantified_hypothesis
+| "intro"
+| "intro" ident
+| "intro" ident "at" "top"
+| "intro" ident "at" "bottom"
+| "intro" ident "after" hyp
+| "intro" ident "before" hyp
+| "intro" "at" "top"
+| "intro" "at" "bottom"
+| "intro" "after" hyp
+| "intro" "before" hyp
+| "move" hyp "at" "top"
+| "move" hyp "at" "bottom"
+| "move" hyp "after" hyp
+| "move" hyp "before" hyp
+| "rename" LIST1 rename SEP ","
+| "revert" LIST1 hyp
+| "simple" "induction" quantified_hypothesis
+| "simple" "destruct" quantified_hypothesis
+| "double" "induction" quantified_hypothesis quantified_hypothesis
+| "admit"
+| "fix" ident natural
+| "cofix" ident
+| "clear" LIST0 hyp
+| "clear" "-" LIST1 hyp
+| "clearbody" LIST1 hyp
+| "generalize" "dependent" constr
+| "replace" uconstr "with" constr clause by_arg_tac
+| "replace" "->" uconstr clause
+| "replace" "<-" uconstr clause
+| "replace" uconstr clause
+| "simplify_eq"
+| "simplify_eq" destruction_arg
+| "esimplify_eq"
+| "esimplify_eq" destruction_arg
+| "discriminate"
+| "discriminate" destruction_arg
+| "ediscriminate"
+| "ediscriminate" destruction_arg
+| "injection"
+| "injection" destruction_arg
+| "einjection"
+| "einjection" destruction_arg
+| "injection" "as" LIST0 simple_intropattern
+| "injection" destruction_arg "as" LIST0 simple_intropattern
+| "einjection" "as" LIST0 simple_intropattern
+| "einjection" destruction_arg "as" LIST0 simple_intropattern
+| "simple" "injection"
+| "simple" "injection" destruction_arg
+| "dependent" "rewrite" orient constr
+| "dependent" "rewrite" orient constr "in" hyp
+| "cutrewrite" orient constr
+| "cutrewrite" orient constr "in" hyp
+| "decompose" "sum" constr
+| "decompose" "record" constr
+| "absurd" constr
+| "contradiction" OPT constr_with_bindings
+| "autorewrite" "with" LIST1 preident clause
+| "autorewrite" "with" LIST1 preident clause "using" tactic
+| "autorewrite" "*" "with" LIST1 preident clause
+| "autorewrite" "*" "with" LIST1 preident clause "using" tactic
+| "rewrite" "*" orient uconstr "in" hyp "at" occurrences by_arg_tac
+| "rewrite" "*" orient uconstr "at" occurrences "in" hyp by_arg_tac
+| "rewrite" "*" orient uconstr "in" hyp by_arg_tac
+| "rewrite" "*" orient uconstr "at" occurrences by_arg_tac
+| "rewrite" "*" orient uconstr by_arg_tac
+| "refine" uconstr
+| "simple" "refine" uconstr
+| "notypeclasses" "refine" uconstr
+| "simple" "notypeclasses" "refine" uconstr
+| "solve_constraints"
+| "subst" LIST1 var
+| "subst"
+| "simple" "subst"
+| "evar" test_lpar_id_colon "(" ident ":" lconstr ")"
+| "evar" constr
+| "instantiate" "(" ident ":=" lglob ")"
+| "instantiate" "(" integer ":=" lglob ")" hloc
+| "instantiate"
+| "stepl" constr "by" tactic
+| "stepl" constr
+| "stepr" constr "by" tactic
+| "stepr" constr
+| "generalize_eqs" hyp
+| "dependent" "generalize_eqs" hyp
+| "generalize_eqs_vars" hyp
+| "dependent" "generalize_eqs_vars" hyp
+| "specialize_eqs" hyp
+| "hresolve_core" "(" ident ":=" constr ")" "at" int_or_var "in" constr
+| "hresolve_core" "(" ident ":=" constr ")" "in" constr
+| "hget_evar" int_or_var
+| "destauto"
+| "destauto" "in" hyp
+| "transparent_abstract" tactic3
+| "transparent_abstract" tactic3 "using" ident
+| "constr_eq" constr constr
+| "constr_eq_strict" constr constr
+| "constr_eq_nounivs" constr constr
+| "is_evar" constr
+| "has_evar" constr
+| "is_var" constr
+| "is_fix" constr
+| "is_cofix" constr
+| "is_ind" constr
+| "is_constructor" constr
+| "is_proj" constr
+| "is_const" constr
+| "shelve"
+| "shelve_unifiable"
+| "unshelve" tactic1
+| "give_up"
+| "cycle" int_or_var
+| "swap" int_or_var int_or_var
+| "revgoals"
+| "guard" test
+| "decompose" "[" LIST1 constr "]" constr
+| "optimize_heap"
+| "eassumption"
+| "eexact" constr
+| "trivial" auto_using hintbases
+| "info_trivial" auto_using hintbases
+| "debug" "trivial" auto_using hintbases
+| "auto" OPT int_or_var auto_using hintbases
+| "info_auto" OPT int_or_var auto_using hintbases
+| "debug" "auto" OPT int_or_var auto_using hintbases
+| "prolog" "[" LIST0 uconstr "]" int_or_var
+| "eauto" OPT int_or_var OPT int_or_var auto_using hintbases
+| "new" "auto" OPT int_or_var auto_using hintbases
+| "debug" "eauto" OPT int_or_var OPT int_or_var auto_using hintbases
+| "info_eauto" OPT int_or_var OPT int_or_var auto_using hintbases
+| "dfs" "eauto" OPT int_or_var auto_using hintbases
+| "autounfold" hintbases clause_dft_concl
+| "autounfold_one" hintbases "in" hyp
+| "autounfold_one" hintbases
+| "unify" constr constr
+| "unify" constr constr "with" preident
+| "convert_concl_no_check" constr
+| "typeclasses" "eauto" "bfs" OPT int_or_var "with" LIST1 preident
+| "typeclasses" "eauto" OPT int_or_var "with" LIST1 preident
+| "typeclasses" "eauto" OPT int_or_var
+| "head_of_constr" ident constr
+| "not_evar" constr
+| "is_ground" constr
+| "autoapply" constr "using" preident
+| "autoapply" constr "with" preident
+| "progress_evars" tactic
+| "decide" "equality"
+| "compare" constr constr
+| "rewrite_strat" rewstrategy "in" hyp
+| "rewrite_strat" rewstrategy
+| "rewrite_db" preident "in" hyp
+| "rewrite_db" preident
+| "substitute" orient glob_constr_with_bindings
+| "setoid_rewrite" orient glob_constr_with_bindings
+| "setoid_rewrite" orient glob_constr_with_bindings "in" hyp
+| "setoid_rewrite" orient glob_constr_with_bindings "at" occurrences
+| "setoid_rewrite" orient glob_constr_with_bindings "at" occurrences "in" hyp
+| "setoid_rewrite" orient glob_constr_with_bindings "in" hyp "at" occurrences
+| "setoid_symmetry"
+| "setoid_symmetry" "in" hyp
+| "setoid_reflexivity"
+| "setoid_transitivity" constr
+| "setoid_etransitivity"
+| "intros" ne_intropatterns
+| "intros"
+| "eintros" ne_intropatterns
+| "eintros"
+| "apply" LIST1 constr_with_bindings_arg SEP "," in_hyp_as
+| "eapply" LIST1 constr_with_bindings_arg SEP "," in_hyp_as
+| "simple" "apply" LIST1 constr_with_bindings_arg SEP "," in_hyp_as
+| "simple" "eapply" LIST1 constr_with_bindings_arg SEP "," in_hyp_as
+| "elim" constr_with_bindings_arg OPT eliminator
+| "eelim" constr_with_bindings_arg OPT eliminator
+| "case" induction_clause_list
+| "ecase" induction_clause_list
+| "fix" ident natural "with" LIST1 fixdecl
+| "cofix" ident "with" LIST1 cofixdecl
+| "pose" bindings_with_parameters
+| "pose" constr as_name
+| "epose" bindings_with_parameters
+| "epose" constr as_name
+| "set" bindings_with_parameters clause_dft_concl
+| "set" constr as_name clause_dft_concl
+| "eset" bindings_with_parameters clause_dft_concl
+| "eset" constr as_name clause_dft_concl
+| "remember" constr as_name eqn_ipat clause_dft_all
+| "eremember" constr as_name eqn_ipat clause_dft_all
+| "assert" test_lpar_id_coloneq "(" identref ":=" lconstr ")"
+| "eassert" test_lpar_id_coloneq "(" identref ":=" lconstr ")"
+| "assert" test_lpar_id_colon "(" identref ":" lconstr ")" by_tactic
+| "eassert" test_lpar_id_colon "(" identref ":" lconstr ")" by_tactic
+| "enough" test_lpar_id_colon "(" identref ":" lconstr ")" by_tactic
+| "eenough" test_lpar_id_colon "(" identref ":" lconstr ")" by_tactic
+| "assert" constr as_ipat by_tactic
+| "eassert" constr as_ipat by_tactic
+| "pose" "proof" lconstr as_ipat
+| "epose" "proof" lconstr as_ipat
+| "enough" constr as_ipat by_tactic
+| "eenough" constr as_ipat by_tactic
+| "generalize" constr
+| "generalize" constr LIST1 constr
+| "generalize" constr lookup_at_as_comma occs as_name LIST0 [ "," pattern_occ as_name ]
+| "induction" induction_clause_list
+| "einduction" induction_clause_list
+| "destruct" induction_clause_list
+| "edestruct" induction_clause_list
+| "rewrite" LIST1 oriented_rewriter SEP "," clause_dft_concl by_tactic
+| "erewrite" LIST1 oriented_rewriter SEP "," clause_dft_concl by_tactic
+| "dependent" [ "simple" "inversion" | "inversion" | "inversion_clear" ] quantified_hypothesis as_or_and_ipat OPT [ "with" constr ]
+| "simple" "inversion" quantified_hypothesis as_or_and_ipat in_hyp_list
+| "inversion" quantified_hypothesis as_or_and_ipat in_hyp_list
+| "inversion_clear" quantified_hypothesis as_or_and_ipat in_hyp_list
+| "inversion" quantified_hypothesis "using" constr in_hyp_list
+| "red" clause_dft_concl
+| "hnf" clause_dft_concl
+| "simpl" delta_flag OPT ref_or_pattern_occ clause_dft_concl
+| "cbv" strategy_flag clause_dft_concl
+| "cbn" strategy_flag clause_dft_concl
+| "lazy" strategy_flag clause_dft_concl
+| "compute" delta_flag clause_dft_concl
+| "vm_compute" OPT ref_or_pattern_occ clause_dft_concl
+| "native_compute" OPT ref_or_pattern_occ clause_dft_concl
+| "unfold" LIST1 unfold_occ SEP "," clause_dft_concl
+| "fold" LIST1 constr clause_dft_concl
+| "pattern" LIST1 pattern_occ SEP "," clause_dft_concl
+| "change" conversion clause_dft_concl
+| "change_no_check" conversion clause_dft_concl
+| "start" "ltac" "profiling"
+| "stop" "ltac" "profiling"
+| "reset" "ltac" "profile"
+| "show" "ltac" "profile"
+| "show" "ltac" "profile" "cutoff" int
+| "show" "ltac" "profile" string
+| "restart_timer" OPT string
+| "finish_timing" OPT string
+| "finish_timing" "(" string ")" OPT string
+| "myred"      (* micromega plugin *)
+| "psatz_Z" int_or_var tactic      (* micromega plugin *)
+| "psatz_Z" tactic      (* micromega plugin *)
+| "xlia" tactic      (* micromega plugin *)
+| "xnlia" tactic      (* micromega plugin *)
+| "xnra" tactic      (* micromega plugin *)
+| "xnqa" tactic      (* micromega plugin *)
+| "sos_Z" tactic      (* micromega plugin *)
+| "sos_Q" tactic      (* micromega plugin *)
+| "sos_R" tactic      (* micromega plugin *)
+| "lra_Q" tactic      (* micromega plugin *)
+| "lra_R" tactic      (* micromega plugin *)
+| "psatz_R" int_or_var tactic      (* micromega plugin *)
+| "psatz_R" tactic      (* micromega plugin *)
+| "psatz_Q" int_or_var tactic      (* micromega plugin *)
+| "psatz_Q" tactic      (* micromega plugin *)
+| "nsatz_compute" constr      (* nsatz plugin *)
+| "omega"      (* omega plugin *)
+| "omega" "with" LIST1 ident      (* omega plugin *)
+| "omega" "with" "*"      (* omega plugin *)
+| "rtauto"
+| "protect_fv" string "in" ident      (* setoid_ring plugin *)
+| "protect_fv" string      (* setoid_ring plugin *)
+| "ring_lookup" tactic0 "[" LIST0 constr "]" LIST1 constr      (* setoid_ring plugin *)
+| "field_lookup" tactic "[" LIST0 constr "]" LIST1 constr      (* setoid_ring plugin *)
+| "YouShouldNotTypeThis" ssrintrosarg      (* ssr plugin *)
+| "by" ssrhintarg      (* ssr plugin *)
+| "YouShouldNotTypeThis" "do" ssrdoarg      (* ssr plugin *)
+| "YouShouldNotTypeThis" ssrtclarg ssrseqdir ssrseqarg      (* ssr plugin *)
+| "clear" natural      (* ssr plugin *)
+| "move" ssrmovearg ssrrpat      (* ssr plugin *)
+| "move" ssrmovearg ssrclauses      (* ssr plugin *)
+| "move" ssrrpat      (* ssr plugin *)
+| "move"      (* ssr plugin *)
+| "case" ssrcasearg ssrclauses      (* ssr plugin *)
+| "case"      (* ssr plugin *)
+| "elim" ssrarg ssrclauses      (* ssr plugin *)
+| "elim"      (* ssr plugin *)
+| "apply" ssrapplyarg      (* ssr plugin *)
+| "apply"      (* ssr plugin *)
+| "exact" ssrexactarg      (* ssr plugin *)
+| "exact"      (* ssr plugin *)
+| "exact" "<:" lconstr      (* ssr plugin *)
+| "congr" ssrcongrarg      (* ssr plugin *)
+| "ssrinstancesofruleL2R" ssrterm      (* ssr plugin *)
+| "ssrinstancesofruleR2L" ssrterm      (* ssr plugin *)
+| "rewrite" ssrrwargs ssrclauses      (* ssr plugin *)
+| "unlock" ssrunlockargs ssrclauses      (* ssr plugin *)
+| "pose" ssrfixfwd      (* ssr plugin *)
+| "pose" ssrcofixfwd      (* ssr plugin *)
+| "pose" ssrfwdid ssrposefwd      (* ssr plugin *)
+| "set" ssrfwdid ssrsetfwd ssrclauses      (* ssr plugin *)
+| "abstract" ssrdgens      (* ssr plugin *)
+| "have" ssrhavefwdwbinders      (* ssr plugin *)
+| "have" "suff" ssrhpats_nobs ssrhavefwd      (* ssr plugin *)
+| "have" "suffices" ssrhpats_nobs ssrhavefwd      (* ssr plugin *)
+| "suff" "have" ssrhpats_nobs ssrhavefwd      (* ssr plugin *)
+| "suffices" "have" ssrhpats_nobs ssrhavefwd      (* ssr plugin *)
+| "suff" ssrsufffwd      (* ssr plugin *)
+| "suffices" ssrsufffwd      (* ssr plugin *)
+| "wlog" ssrhpats_nobs ssrwlogfwd ssrhint      (* ssr plugin *)
+| "wlog" "suff" ssrhpats_nobs ssrwlogfwd ssrhint      (* ssr plugin *)
+| "wlog" "suffices" ssrhpats_nobs ssrwlogfwd ssrhint      (* ssr plugin *)
+| "without" "loss" ssrhpats_nobs ssrwlogfwd ssrhint      (* ssr plugin *)
+| "without" "loss" "suff" ssrhpats_nobs ssrwlogfwd ssrhint      (* ssr plugin *)
+| "without" "loss" "suffices" ssrhpats_nobs ssrwlogfwd ssrhint      (* ssr plugin *)
+| "gen" "have" ssrclear ssr_idcomma ssrhpats_nobs ssrwlogfwd ssrhint      (* ssr plugin *)
+| "generally" "have" ssrclear ssr_idcomma ssrhpats_nobs ssrwlogfwd ssrhint      (* ssr plugin *)
+| "under" ssrrwarg      (* ssr plugin *)
+| "under" ssrrwarg ssrintros_ne      (* ssr plugin *)
+| "under" ssrrwarg ssrintros_ne "do" ssrhint3arg      (* ssr plugin *)
+| "under" ssrrwarg "do" ssrhint3arg      (* ssr plugin *)
+| "ssrinstancesoftpat" cpattern      (* ssrmatching plugin *)
+]
+
+mlname: [
+| preident      (* extraction plugin *)
+| string      (* extraction plugin *)
+]
+
+int_or_id: [
+| preident      (* extraction plugin *)
+| integer      (* extraction plugin *)
+]
+
+language: [
+| "Ocaml"      (* extraction plugin *)
+| "OCaml"      (* extraction plugin *)
+| "Haskell"      (* extraction plugin *)
+| "Scheme"      (* extraction plugin *)
+| "JSON"      (* extraction plugin *)
+]
+
+firstorder_using: [
+| "using" reference
+| "using" reference "," LIST1 reference SEP ","
+| "using" reference reference LIST0 reference
+|
+]
+
+fun_ind_using: [
+| "using" constr_with_bindings      (* funind plugin *)
+|      (* funind plugin *)
+]
+
+with_names: [
+| "as" simple_intropattern      (* funind plugin *)
+|      (* funind plugin *)
+]
+
+constr_comma_sequence': [
+| constr "," constr_comma_sequence'      (* funind plugin *)
+| constr      (* funind plugin *)
+]
+
+auto_using': [
+| "using" constr_comma_sequence'      (* funind plugin *)
+|      (* funind plugin *)
+]
+
+function_rec_definition_loc: [
+| Vernac.rec_definition      (* funind plugin *)
+]
+
+fun_scheme_arg: [
+| ident ":=" "Induction" "for" reference "Sort" sort_family      (* funind plugin *)
+]
+
+orient: [
+| "->"
+| "<-"
+|
+]
+
+occurrences: [
+| LIST1 integer
+| var
+]
+
+glob: [
+| constr
+]
+
+lglob: [
+| lconstr
+]
+
+casted_constr: [
+| constr
+]
+
+hloc: [
+|
+| "in" "|-" "*"
+| "in" ident
+| "in" "(" "Type" "of" ident ")"
+| "in" "(" "Value" "of" ident ")"
+| "in" "(" "type" "of" ident ")"
+| "in" "(" "value" "of" ident ")"
+]
+
+rename: [
+| ident "into" ident
+]
+
+by_arg_tac: [
+| "by" tactic3
+|
+]
+
+in_clause: [
+| in_clause'
+| "*" occs
+| "*" "|-" concl_occ
+| LIST0 hypident_occ SEP "," "|-" concl_occ
+| LIST0 hypident_occ SEP ","
+]
+
+test_lpar_id_colon: [
+| local_test_lpar_id_colon
+]
+
+orient_string: [
+| orient preident
+]
+
+comparison: [
+| "="
+| "<"
+| "<="
+| ">"
+| ">="
+]
+
+test: [
+| int_or_var comparison int_or_var
+]
+
+hintbases: [
+| "with" "*"
+| "with" LIST1 preident
+|
+]
+
+auto_using: [
+| "using" LIST1 uconstr SEP ","
+|
+]
+
+hints_path_atom: [
+| LIST1 global
+| "_"
+]
+
+hints_path: [
+| "(" hints_path ")"
+| hints_path "*"
+| "emp"
+| "eps"
+| hints_path "|" hints_path
+| hints_path_atom
+| hints_path hints_path
+]
+
+opthints: [
+| ":" LIST1 preident
+|
+]
+
+debug: [
+| "debug"
+|
+]
+
+eauto_search_strategy: [
+| "(bfs)"
+| "(dfs)"
+|
+]
+
+tactic_then_last: [
+| "|" LIST0 ( OPT tactic_expr5 ) SEP "|"
+|
+]
+
+tactic_then_gen: [
+| tactic_expr5 "|" tactic_then_gen
+| tactic_expr5 ".." tactic_then_last
+| ".." tactic_then_last
+| tactic_expr5
+| "|" tactic_then_gen
+|
+]
+
+tactic_then_locality: [
+| "[" OPT ">"
+]
+
+tactic_expr5: [
+| binder_tactic
+| tactic_expr4
+]
+
+tactic_expr4: [
+| tactic_expr3 ";" binder_tactic
+| tactic_expr3 ";" tactic_expr3
+| tactic_expr3 ";" tactic_then_locality tactic_then_gen "]"
+| tactic_expr3
+| tactic_expr5 ";" "first" ssr_first_else      (* ssr plugin *)
+| tactic_expr5 ";" "first" ssrseqarg      (* ssr plugin *)
+| tactic_expr5 ";" "last" ssrseqarg      (* ssr plugin *)
+]
+
+tactic_expr3: [
+| "try" tactic_expr3
+| "do" int_or_var tactic_expr3
+| "timeout" int_or_var tactic_expr3
+| "time" OPT string tactic_expr3
+| "repeat" tactic_expr3
+| "progress" tactic_expr3
+| "once" tactic_expr3
+| "exactly_once" tactic_expr3
+| "infoH" tactic_expr3
+| "abstract" tactic_expr2
+| "abstract" tactic_expr2 "using" ident
+| selector tactic_expr3
+| tactic_expr2
+| "do" ssrmmod ssrdotac ssrclauses      (* ssr plugin *)
+| "do" ssrortacarg ssrclauses      (* ssr plugin *)
+| "do" int_or_var ssrmmod ssrdotac ssrclauses      (* ssr plugin *)
+| "abstract" ssrdgens      (* ssr plugin *)
+]
+
+tactic_expr2: [
+| tactic_expr1 "+" binder_tactic
+| tactic_expr1 "+" tactic_expr2
+| "tryif" tactic_expr5 "then" tactic_expr5 "else" tactic_expr2
+| tactic_expr1 "||" binder_tactic
+| tactic_expr1 "||" tactic_expr2
+| tactic_expr1
+]
+
+tactic_expr1: [
+| match_key "goal" "with" match_context_list "end"
+| match_key "reverse" "goal" "with" match_context_list "end"
+| match_key tactic_expr5 "with" match_list "end"
+| "first" "[" LIST0 tactic_expr5 SEP "|" "]"
+| "solve" "[" LIST0 tactic_expr5 SEP "|" "]"
+| "idtac" LIST0 message_token
+| failkw [ int_or_var | ] LIST0 message_token
+| simple_tactic
+| tactic_arg
+| reference LIST0 tactic_arg_compat
+| tactic_expr0
+| tactic_expr5 ssrintros_ne      (* ssr plugin *)
+]
+
+tactic_expr0: [
+| "(" tactic_expr5 ")"
+| "[" ">" tactic_then_gen "]"
+| tactic_atom
+| ssrparentacarg      (* ssr plugin *)
+]
+
+failkw: [
+| "fail"
+| "gfail"
+]
+
+binder_tactic: [
+| "fun" LIST1 input_fun "=>" tactic_expr5
+| "let" [ "rec" | ] LIST1 let_clause SEP "with" "in" tactic_expr5
+| "info" tactic_expr5
+]
+
+tactic_arg_compat: [
+| tactic_arg
+| Constr.constr
+| "()"
+]
+
+tactic_arg: [
+| constr_eval
+| "fresh" LIST0 fresh_id
+| "type_term" uconstr
+| "numgoals"
+]
+
+fresh_id: [
+| STRING
+| qualid
+]
+
+constr_eval: [
+| "eval" red_expr "in" Constr.constr
+| "context" identref "[" Constr.lconstr "]"
+| "type" "of" Constr.constr
+]
+
+constr_may_eval: [
+| constr_eval
+| Constr.constr
+]
+
+tactic_atom: [
+| integer
+| reference
+| "()"
+]
+
+match_key: [
+| "match"
+| "lazymatch"
+| "multimatch"
+]
+
+input_fun: [
+| "_"
+| ident
+]
+
+let_clause: [
+| identref ":=" tactic_expr5
+| "_" ":=" tactic_expr5
+| identref LIST1 input_fun ":=" tactic_expr5
+]
+
+match_pattern: [
+| "context" OPT Constr.ident "[" Constr.lconstr_pattern "]"
+| Constr.lconstr_pattern
+]
+
+match_hyps: [
+| name ":" match_pattern
+| name ":=" "[" match_pattern "]" ":" match_pattern
+| name ":=" match_pattern
+]
+
+match_context_rule: [
+| LIST0 match_hyps SEP "," "|-" match_pattern "=>" tactic_expr5
+| "[" LIST0 match_hyps SEP "," "|-" match_pattern "]" "=>" tactic_expr5
+| "_" "=>" tactic_expr5
+]
+
+match_context_list: [
+| LIST1 match_context_rule SEP "|"
+| "|" LIST1 match_context_rule SEP "|"
+]
+
+match_rule: [
+| match_pattern "=>" tactic_expr5
+| "_" "=>" tactic_expr5
+]
+
+match_list: [
+| LIST1 match_rule SEP "|"
+| "|" LIST1 match_rule SEP "|"
+]
+
+message_token: [
+| identref
+| STRING
+| integer
+]
+
+ltac_def_kind: [
+| ":="
+| "::="
+]
+
+tacdef_body: [
+| Constr.global LIST1 input_fun ltac_def_kind tactic_expr5
+| Constr.global ltac_def_kind tactic_expr5
+]
+
+tactic: [
+| tactic_expr5
+]
+
+range_selector: [
+| natural "-" natural
+| natural
+]
+
+range_selector_or_nth: [
+| natural "-" natural OPT [ "," LIST1 range_selector SEP "," ]
+| natural OPT [ "," LIST1 range_selector SEP "," ]
+]
+
+selector_body: [
+| range_selector_or_nth
+| test_bracket_ident "[" ident "]"
+]
+
+selector: [
+| "only" selector_body ":"
+]
+
+toplevel_selector: [
+| selector_body ":"
+| "!" ":"
+| "all" ":"
+]
+
+tactic_mode: [
+| OPT toplevel_selector G_vernac.query_command
+| OPT toplevel_selector "{"
+| OPT ltac_selector OPT ltac_info tactic ltac_use_default
+| "par" ":" OPT ltac_info tactic ltac_use_default
+]
+
+ltac_selector: [
+| toplevel_selector
+]
+
+ltac_info: [
+| "Info" natural
+]
+
+ltac_use_default: [
+| "."
+| "..."
+]
+
+ltac_tactic_level: [
+| "(" "at" "level" natural ")"
+]
+
+ltac_production_sep: [
+| "," string
+]
+
+ltac_production_item: [
+| string
+| ident "(" ident OPT ltac_production_sep ")"
+| ident
+]
+
+ltac_tacdef_body: [
+| tacdef_body
+]
+
+withtac: [
+| "with" Tactic.tactic
+|
+]
+
+Constr.closed_binder: [
+| "(" Prim.name ":" Constr.lconstr "|" Constr.lconstr ")"
+]
+
+glob_constr_with_bindings: [
+| constr_with_bindings
+]
+
+rewstrategy: [
+| glob
+| "<-" constr
+| "subterms" rewstrategy
+| "subterm" rewstrategy
+| "innermost" rewstrategy
+| "outermost" rewstrategy
+| "bottomup" rewstrategy
+| "topdown" rewstrategy
+| "id"
+| "fail"
+| "refl"
+| "progress" rewstrategy
+| "try" rewstrategy
+| "any" rewstrategy
+| "repeat" rewstrategy
+| rewstrategy ";" rewstrategy
+| "(" rewstrategy ")"
+| "choice" rewstrategy rewstrategy
+| "old_hints" preident
+| "hints" preident
+| "terms" LIST0 constr
+| "eval" red_expr
+| "fold" constr
+]
+
+int_or_var: [
+| integer
+| identref
+]
+
+nat_or_var: [
+| natural
+| identref
+]
+
+id_or_meta: [
+| identref
+]
+
+open_constr: [
+| constr
+]
+
+uconstr: [
+| constr
+]
+
+destruction_arg: [
+| natural
+| test_lpar_id_rpar constr_with_bindings
+| constr_with_bindings_arg
+]
+
+constr_with_bindings_arg: [
+| ">" constr_with_bindings
+| constr_with_bindings
+]
+
+quantified_hypothesis: [
+| ident
+| natural
+]
+
+conversion: [
+| constr
+| constr "with" constr
+| constr "at" occs_nums "with" constr
+]
+
+occs_nums: [
+| LIST1 nat_or_var
+| "-" nat_or_var LIST0 int_or_var
+]
+
+occs: [
+| "at" occs_nums
+|
+]
+
+pattern_occ: [
+| constr occs
+]
+
+ref_or_pattern_occ: [
+| smart_global occs
+| constr occs
+]
+
+unfold_occ: [
+| smart_global occs
+]
+
+intropatterns: [
+| LIST0 intropattern
+]
+
+ne_intropatterns: [
+| LIST1 intropattern
+]
+
+or_and_intropattern: [
+| "[" LIST1 intropatterns SEP "|" "]"
+| "()"
+| "(" simple_intropattern ")"
+| "(" simple_intropattern "," LIST1 simple_intropattern SEP "," ")"
+| "(" simple_intropattern "&" LIST1 simple_intropattern SEP "&" ")"
+]
+
+equality_intropattern: [
+| "->"
+| "<-"
+| "[=" intropatterns "]"
+]
+
+naming_intropattern: [
+| pattern_ident
+| "?"
+| ident
+]
+
+intropattern: [
+| simple_intropattern
+| "*"
+| "**"
+]
+
+simple_intropattern: [
+| simple_intropattern_closed LIST0 [ "%" operconstr0 ]
+]
+
+simple_intropattern_closed: [
+| or_and_intropattern
+| equality_intropattern
+| "_"
+| naming_intropattern
+]
+
+simple_binding: [
+| "(" ident ":=" lconstr ")"
+| "(" natural ":=" lconstr ")"
+]
+
+bindings: [
+| test_lpar_idnum_coloneq LIST1 simple_binding
+| LIST1 constr
+]
+
+constr_with_bindings: [
+| constr with_bindings
+]
+
+with_bindings: [
+| "with" bindings
+|
+]
+
+red_flags: [
+| "beta"
+| "iota"
+| "match"
+| "fix"
+| "cofix"
+| "zeta"
+| "delta" delta_flag
+]
+
+delta_flag: [
+| "-" "[" LIST1 smart_global "]"
+| "[" LIST1 smart_global "]"
+|
+]
+
+strategy_flag: [
+| LIST1 red_flags
+| delta_flag
+]
+
+red_expr: [
+| "red"
+| "hnf"
+| "simpl" delta_flag OPT ref_or_pattern_occ
+| "cbv" strategy_flag
+| "cbn" strategy_flag
+| "lazy" strategy_flag
+| "compute" delta_flag
+| "vm_compute" OPT ref_or_pattern_occ
+| "native_compute" OPT ref_or_pattern_occ
+| "unfold" LIST1 unfold_occ SEP ","
+| "fold" LIST1 constr
+| "pattern" LIST1 pattern_occ SEP ","
+| IDENT
+]
+
+hypident: [
+| id_or_meta
+| "(" "type" "of" id_or_meta ")"
+| "(" "value" "of" id_or_meta ")"
+| "(" "type" "of" Prim.identref ")"      (* ssr plugin *)
+| "(" "value" "of" Prim.identref ")"      (* ssr plugin *)
+]
+
+hypident_occ: [
+| hypident occs
+]
+
+clause_dft_concl: [
+| "in" in_clause
+| occs
+|
+]
+
+clause_dft_all: [
+| "in" in_clause
+|
+]
+
+opt_clause: [
+| "in" in_clause
+| "at" occs_nums
+|
+]
+
+concl_occ: [
+| "*" occs
+|
+]
+
+in_hyp_list: [
+| "in" LIST1 id_or_meta
+|
+]
+
+in_hyp_as: [
+| "in" id_or_meta as_ipat
+|
+]
+
+simple_binder: [
+| name
+| "(" LIST1 name ":" lconstr ")"
+]
+
+fixdecl: [
+| "(" ident LIST0 simple_binder fixannot ":" lconstr ")"
+]
+
+cofixdecl: [
+| "(" ident LIST0 simple_binder ":" lconstr ")"
+]
+
+bindings_with_parameters: [
+| check_for_coloneq "(" ident LIST0 simple_binder ":=" lconstr ")"
+]
+
+eliminator: [
+| "using" constr_with_bindings
+]
+
+as_ipat: [
+| "as" simple_intropattern
+|
+]
+
+or_and_intropattern_loc: [
+| or_and_intropattern
+| identref
+]
+
+as_or_and_ipat: [
+| "as" or_and_intropattern_loc
+|
+]
+
+eqn_ipat: [
+| "eqn" ":" naming_intropattern
+| "_eqn" ":" naming_intropattern
+| "_eqn"
+|
+]
+
+as_name: [
+| "as" ident
+|
+]
+
+by_tactic: [
+| "by" tactic_expr3
+|
+]
+
+rewriter: [
+| "!" constr_with_bindings_arg
+| [ "?" | LEFTQMARK ] constr_with_bindings_arg
+| natural "!" constr_with_bindings_arg
+| natural [ "?" | LEFTQMARK ] constr_with_bindings_arg
+| natural constr_with_bindings_arg
+| constr_with_bindings_arg
+]
+
+oriented_rewriter: [
+| orient rewriter
+]
+
+induction_clause: [
+| destruction_arg as_or_and_ipat eqn_ipat opt_clause
+]
+
+induction_clause_list: [
+| LIST1 induction_clause SEP "," OPT eliminator opt_clause
+]
+
+ring_mod: [
+| "decidable" constr      (* setoid_ring plugin *)
+| "abstract"      (* setoid_ring plugin *)
+| "morphism" constr      (* setoid_ring plugin *)
+| "constants" "[" tactic "]"      (* setoid_ring plugin *)
+| "closed" "[" LIST1 global "]"      (* setoid_ring plugin *)
+| "preprocess" "[" tactic "]"      (* setoid_ring plugin *)
+| "postprocess" "[" tactic "]"      (* setoid_ring plugin *)
+| "setoid" constr constr      (* setoid_ring plugin *)
+| "sign" constr      (* setoid_ring plugin *)
+| "power" constr "[" LIST1 global "]"      (* setoid_ring plugin *)
+| "power_tac" constr "[" tactic "]"      (* setoid_ring plugin *)
+| "div" constr      (* setoid_ring plugin *)
+]
+
+ring_mods: [
+| "(" LIST1 ring_mod SEP "," ")"      (* setoid_ring plugin *)
+]
+
+field_mod: [
+| ring_mod      (* setoid_ring plugin *)
+| "completeness" constr      (* setoid_ring plugin *)
+]
+
+field_mods: [
+| "(" LIST1 field_mod SEP "," ")"      (* setoid_ring plugin *)
+]
+
+ssrtacarg: [
+| tactic_expr5      (* ssr plugin *)
+]
+
+ssrtac3arg: [
+| tactic_expr3      (* ssr plugin *)
+]
+
+ssrtclarg: [
+| ssrtacarg      (* ssr plugin *)
+]
+
+ssrhyp: [
+| ident      (* ssr plugin *)
+]
+
+ssrhoi_hyp: [
+| ident      (* ssr plugin *)
+]
+
+ssrhoi_id: [
+| ident      (* ssr plugin *)
+]
+
+ssrsimpl_ne: [
+| "//="      (* ssr plugin *)
+| "/="      (* ssr plugin *)
+| test_ssrslashnum11 "/" natural "/" natural "="      (* ssr plugin *)
+| test_ssrslashnum10 "/" natural "/"      (* ssr plugin *)
+| test_ssrslashnum10 "/" natural "="      (* ssr plugin *)
+| test_ssrslashnum10 "/" natural "/="      (* ssr plugin *)
+| test_ssrslashnum10 "/" natural "/" "="      (* ssr plugin *)
+| test_ssrslashnum01 "//" natural "="      (* ssr plugin *)
+| test_ssrslashnum00 "//"      (* ssr plugin *)
+]
+
+ssrclear_ne: [
+| "{" LIST1 ssrhyp "}"      (* ssr plugin *)
+]
+
+ssrclear: [
+| ssrclear_ne      (* ssr plugin *)
+|      (* ssr plugin *)
+]
+
+ssrindex: [
+| int_or_var      (* ssr plugin *)
+]
+
+ssrocc: [
+| natural LIST0 natural      (* ssr plugin *)
+| "-" LIST0 natural      (* ssr plugin *)
+| "+" LIST0 natural      (* ssr plugin *)
+]
+
+ssrmmod: [
+| "!"      (* ssr plugin *)
+| LEFTQMARK      (* ssr plugin *)
+| "?"      (* ssr plugin *)
+]
+
+ssrmult_ne: [
+| natural ssrmmod      (* ssr plugin *)
+| ssrmmod      (* ssr plugin *)
+]
+
+ssrmult: [
+| ssrmult_ne      (* ssr plugin *)
+|      (* ssr plugin *)
+]
+
+ssrdocc: [
+| "{" ssrocc "}"      (* ssr plugin *)
+| "{" LIST0 ssrhyp "}"      (* ssr plugin *)
+]
+
+ssrterm: [
+| "YouShouldNotTypeThis" constr      (* ssr plugin *)
+| ssrtermkind Pcoq.Constr.constr      (* ssr plugin *)
+]
+
+ast_closure_term: [
+| term_annotation constr      (* ssr plugin *)
+]
+
+ast_closure_lterm: [
+| term_annotation lconstr      (* ssr plugin *)
+]
+
+ssrbwdview: [
+| "YouShouldNotTypeThis"      (* ssr plugin *)
+| test_not_ssrslashnum "/" Pcoq.Constr.constr      (* ssr plugin *)
+| test_not_ssrslashnum "/" Pcoq.Constr.constr ssrbwdview      (* ssr plugin *)
+]
+
+ssrfwdview: [
+| "YouShouldNotTypeThis"      (* ssr plugin *)
+| test_not_ssrslashnum "/" ast_closure_term      (* ssr plugin *)
+| test_not_ssrslashnum "/" ast_closure_term ssrfwdview      (* ssr plugin *)
+]
+
+ident_no_do: [
+| "YouShouldNotTypeThis" ident      (* ssr plugin *)
+| test_ident_no_do IDENT      (* ssr plugin *)
+]
+
+ssripat: [
+| "_"      (* ssr plugin *)
+| "*"      (* ssr plugin *)
+| ">"      (* ssr plugin *)
+| ident_no_do      (* ssr plugin *)
+| "?"      (* ssr plugin *)
+| "+"      (* ssr plugin *)
+| "++"      (* ssr plugin *)
+| ssrsimpl_ne      (* ssr plugin *)
+| ssrdocc "->"      (* ssr plugin *)
+| ssrdocc "<-"      (* ssr plugin *)
+| ssrdocc      (* ssr plugin *)
+| "->"      (* ssr plugin *)
+| "<-"      (* ssr plugin *)
+| "-"      (* ssr plugin *)
+| "-/" "="      (* ssr plugin *)
+| "-/="      (* ssr plugin *)
+| "-/" "/"      (* ssr plugin *)
+| "-//"      (* ssr plugin *)
+| "-/" integer "/"      (* ssr plugin *)
+| "-/" "/="      (* ssr plugin *)
+| "-//" "="      (* ssr plugin *)
+| "-//="      (* ssr plugin *)
+| "-/" integer "/="      (* ssr plugin *)
+| "-/" integer "/" integer "="      (* ssr plugin *)
+| ssrfwdview      (* ssr plugin *)
+| "[" ":" LIST0 ident "]"      (* ssr plugin *)
+| "[:" LIST0 ident "]"      (* ssr plugin *)
+| ssrcpat      (* ssr plugin *)
+]
+
+ssripats: [
+| ssripat ssripats      (* ssr plugin *)
+|      (* ssr plugin *)
+]
+
+ssriorpat: [
+| ssripats "|" ssriorpat      (* ssr plugin *)
+| ssripats "|-" ">" ssriorpat      (* ssr plugin *)
+| ssripats "|-" ssriorpat      (* ssr plugin *)
+| ssripats "|->" ssriorpat      (* ssr plugin *)
+| ssripats "||" ssriorpat      (* ssr plugin *)
+| ssripats "|||" ssriorpat      (* ssr plugin *)
+| ssripats "||||" ssriorpat      (* ssr plugin *)
+| ssripats      (* ssr plugin *)
+]
+
+ssrcpat: [
+| "YouShouldNotTypeThis" ssriorpat      (* ssr plugin *)
+| test_nohidden "[" hat "]"      (* ssr plugin *)
+| test_nohidden "[" ssriorpat "]"      (* ssr plugin *)
+| test_nohidden "[=" ssriorpat "]"      (* ssr plugin *)
+]
+
+hat: [
+| "^" ident      (* ssr plugin *)
+| "^" "~" ident      (* ssr plugin *)
+| "^" "~" natural      (* ssr plugin *)
+| "^~" ident      (* ssr plugin *)
+| "^~" natural      (* ssr plugin *)
+]
+
+ssripats_ne: [
+| ssripat ssripats      (* ssr plugin *)
+]
+
+ssrhpats: [
+| ssripats      (* ssr plugin *)
+]
+
+ssrhpats_wtransp: [
+| ssripats      (* ssr plugin *)
+| ssripats "@" ssripats      (* ssr plugin *)
+]
+
+ssrhpats_nobs: [
+| ssripats      (* ssr plugin *)
+]
+
+ssrrpat: [
+| "->"      (* ssr plugin *)
+| "<-"      (* ssr plugin *)
+]
+
+ssrintros_ne: [
+| "=>" ssripats_ne      (* ssr plugin *)
+]
+
+ssrintros: [
+| ssrintros_ne      (* ssr plugin *)
+|      (* ssr plugin *)
+]
+
+ssrintrosarg: [
+| "YouShouldNotTypeThis" ssrtacarg ssrintros_ne      (* ssr plugin *)
+]
+
+ssrfwdid: [
+| test_ssrfwdid Prim.ident      (* ssr plugin *)
+]
+
+ssrortacs: [
+| ssrtacarg "|" ssrortacs      (* ssr plugin *)
+| ssrtacarg "|"      (* ssr plugin *)
+| ssrtacarg      (* ssr plugin *)
+| "|" ssrortacs      (* ssr plugin *)
+| "|"      (* ssr plugin *)
+]
+
+ssrhintarg: [
+| "[" "]"      (* ssr plugin *)
+| "[" ssrortacs "]"      (* ssr plugin *)
+| ssrtacarg      (* ssr plugin *)
+]
+
+ssrhint3arg: [
+| "[" "]"      (* ssr plugin *)
+| "[" ssrortacs "]"      (* ssr plugin *)
+| ssrtac3arg      (* ssr plugin *)
+]
+
+ssrortacarg: [
+| "[" ssrortacs "]"      (* ssr plugin *)
+]
+
+ssrhint: [
+|      (* ssr plugin *)
+| "by" ssrhintarg      (* ssr plugin *)
+]
+
+ssrwgen: [
+| ssrclear_ne      (* ssr plugin *)
+| ssrhoi_hyp      (* ssr plugin *)
+| "@" ssrhoi_hyp      (* ssr plugin *)
+| "(" ssrhoi_id ":=" lcpattern ")"      (* ssr plugin *)
+| "(" ssrhoi_id ")"      (* ssr plugin *)
+| "(@" ssrhoi_id ":=" lcpattern ")"      (* ssr plugin *)
+| "(" "@" ssrhoi_id ":=" lcpattern ")"      (* ssr plugin *)
+]
+
+ssrclausehyps: [
+| ssrwgen "," ssrclausehyps      (* ssr plugin *)
+| ssrwgen ssrclausehyps      (* ssr plugin *)
+| ssrwgen      (* ssr plugin *)
+]
+
+ssrclauses: [
+| "in" ssrclausehyps "|-" "*"      (* ssr plugin *)
+| "in" ssrclausehyps "|-"      (* ssr plugin *)
+| "in" ssrclausehyps "*"      (* ssr plugin *)
+| "in" ssrclausehyps      (* ssr plugin *)
+| "in" "|-" "*"      (* ssr plugin *)
+| "in" "*"      (* ssr plugin *)
+| "in" "*" "|-"      (* ssr plugin *)
+|      (* ssr plugin *)
+]
+
+ssrfwd: [
+| ":=" ast_closure_lterm      (* ssr plugin *)
+| ":" ast_closure_lterm ":=" ast_closure_lterm      (* ssr plugin *)
+]
+
+ssrbvar: [
+| ident      (* ssr plugin *)
+| "_"      (* ssr plugin *)
+]
+
+ssrbinder: [
+| ssrbvar      (* ssr plugin *)
+| "(" ssrbvar ")"      (* ssr plugin *)
+| "(" ssrbvar ":" lconstr ")"      (* ssr plugin *)
+| "(" ssrbvar LIST1 ssrbvar ":" lconstr ")"      (* ssr plugin *)
+| "(" ssrbvar ":" lconstr ":=" lconstr ")"      (* ssr plugin *)
+| "(" ssrbvar ":=" lconstr ")"      (* ssr plugin *)
+| [ "of" | "&" ] operconstr99      (* ssr plugin *)
+]
+
+ssrstruct: [
+| "{" "struct" ident "}"      (* ssr plugin *)
+|      (* ssr plugin *)
+]
+
+ssrposefwd: [
+| LIST0 ssrbinder ssrfwd      (* ssr plugin *)
+]
+
+ssrfixfwd: [
+| "fix" ssrbvar LIST0 ssrbinder ssrstruct ssrfwd      (* ssr plugin *)
+]
+
+ssrcofixfwd: [
+| "cofix" ssrbvar LIST0 ssrbinder ssrfwd      (* ssr plugin *)
+]
+
+ssrsetfwd: [
+| ":" ast_closure_lterm ":=" "{" ssrocc "}" cpattern      (* ssr plugin *)
+| ":" ast_closure_lterm ":=" lcpattern      (* ssr plugin *)
+| ":=" "{" ssrocc "}" cpattern      (* ssr plugin *)
+| ":=" lcpattern      (* ssr plugin *)
+]
+
+ssrhavefwd: [
+| ":" ast_closure_lterm ssrhint      (* ssr plugin *)
+| ":" ast_closure_lterm ":=" ast_closure_lterm      (* ssr plugin *)
+| ":" ast_closure_lterm ":="      (* ssr plugin *)
+| ":=" ast_closure_lterm      (* ssr plugin *)
+]
+
+ssrhavefwdwbinders: [
+| ssrhpats_wtransp LIST0 ssrbinder ssrhavefwd      (* ssr plugin *)
+]
+
+ssrdoarg: [
+]
+
+ssrseqarg: [
+| ssrswap      (* ssr plugin *)
+| ssrseqidx ssrortacarg OPT ssrorelse      (* ssr plugin *)
+| ssrseqidx ssrswap      (* ssr plugin *)
+| tactic_expr3      (* ssr plugin *)
+]
+
+ssrseqidx: [
+| test_ssrseqvar Prim.ident      (* ssr plugin *)
+| Prim.natural      (* ssr plugin *)
+]
+
+ssrswap: [
+| "first"      (* ssr plugin *)
+| "last"      (* ssr plugin *)
+]
+
+ssrorelse: [
+| "||" tactic_expr2      (* ssr plugin *)
+]
+
+Prim.ident: [
+| IDENT ssr_null_entry      (* ssr plugin *)
+]
+
+ssrparentacarg: [
+| "(" tactic_expr5 ")"      (* ssr plugin *)
+]
+
+ssrdotac: [
+| tactic_expr3      (* ssr plugin *)
+| ssrortacarg      (* ssr plugin *)
+]
+
+ssrseqdir: [
+]
+
+ssr_first: [
+| ssr_first ssrintros_ne      (* ssr plugin *)
+| "[" LIST0 tactic_expr5 SEP "|" "]"      (* ssr plugin *)
+]
+
+ssr_first_else: [
+| ssr_first ssrorelse      (* ssr plugin *)
+| ssr_first      (* ssr plugin *)
+]
+
+ssrgen: [
+| ssrdocc cpattern      (* ssr plugin *)
+| cpattern      (* ssr plugin *)
+]
+
+ssrdgens_tl: [
+| "{" LIST1 ssrhyp "}" cpattern ssrdgens_tl      (* ssr plugin *)
+| "{" LIST1 ssrhyp "}"      (* ssr plugin *)
+| "{" ssrocc "}" cpattern ssrdgens_tl      (* ssr plugin *)
+| "/" ssrdgens_tl      (* ssr plugin *)
+| cpattern ssrdgens_tl      (* ssr plugin *)
+|      (* ssr plugin *)
+]
+
+ssrdgens: [
+| ":" ssrgen ssrdgens_tl      (* ssr plugin *)
+]
+
+ssreqid: [
+| test_ssreqid ssreqpat      (* ssr plugin *)
+| test_ssreqid      (* ssr plugin *)
+]
+
+ssreqpat: [
+| Prim.ident      (* ssr plugin *)
+| "_"      (* ssr plugin *)
+| "?"      (* ssr plugin *)
+| "+"      (* ssr plugin *)
+| ssrdocc "->"      (* ssr plugin *)
+| ssrdocc "<-"      (* ssr plugin *)
+| "->"      (* ssr plugin *)
+| "<-"      (* ssr plugin *)
+]
+
+ssrarg: [
+| ssrfwdview ssreqid ssrdgens ssrintros      (* ssr plugin *)
+| ssrfwdview ssrclear ssrintros      (* ssr plugin *)
+| ssreqid ssrdgens ssrintros      (* ssr plugin *)
+| ssrclear_ne ssrintros      (* ssr plugin *)
+| ssrintros_ne      (* ssr plugin *)
+]
+
+ssrmovearg: [
+| ssrarg      (* ssr plugin *)
+]
+
+ssrcasearg: [
+| ssrarg      (* ssr plugin *)
+]
+
+ssragen: [
+| "{" LIST1 ssrhyp "}" ssrterm      (* ssr plugin *)
+| ssrterm      (* ssr plugin *)
+]
+
+ssragens: [
+| "{" LIST1 ssrhyp "}" ssrterm ssragens      (* ssr plugin *)
+| "{" LIST1 ssrhyp "}"      (* ssr plugin *)
+| ssrterm ssragens      (* ssr plugin *)
+|      (* ssr plugin *)
+]
+
+ssrapplyarg: [
+| ":" ssragen ssragens ssrintros      (* ssr plugin *)
+| ssrclear_ne ssrintros      (* ssr plugin *)
+| ssrintros_ne      (* ssr plugin *)
+| ssrbwdview ":" ssragen ssragens ssrintros      (* ssr plugin *)
+| ssrbwdview ssrclear ssrintros      (* ssr plugin *)
+]
+
+ssrexactarg: [
+| ":" ssragen ssragens      (* ssr plugin *)
+| ssrbwdview ssrclear      (* ssr plugin *)
+| ssrclear_ne      (* ssr plugin *)
+]
+
+ssrcongrarg: [
+| natural constr ssrdgens      (* ssr plugin *)
+| natural constr      (* ssr plugin *)
+| constr ssrdgens      (* ssr plugin *)
+| constr      (* ssr plugin *)
+]
+
+ssrrwocc: [
+| "{" LIST0 ssrhyp "}"      (* ssr plugin *)
+| "{" ssrocc "}"      (* ssr plugin *)
+|      (* ssr plugin *)
+]
+
+ssrrule_ne: [
+| test_not_ssrslashnum [ "/" ssrterm | ssrterm | ssrsimpl_ne ]      (* ssr plugin *)
+| ssrsimpl_ne      (* ssr plugin *)
+]
+
+ssrrule: [
+| ssrrule_ne      (* ssr plugin *)
+|      (* ssr plugin *)
+]
+
+ssrpattern_squarep: [
+| "[" rpattern "]"      (* ssr plugin *)
+|      (* ssr plugin *)
+]
+
+ssrpattern_ne_squarep: [
+| "[" rpattern "]"      (* ssr plugin *)
+]
+
+ssrrwarg: [
+| "-" ssrmult ssrrwocc ssrpattern_squarep ssrrule_ne      (* ssr plugin *)
+| "-/" ssrterm      (* ssr plugin *)
+| ssrmult_ne ssrrwocc ssrpattern_squarep ssrrule_ne      (* ssr plugin *)
+| "{" LIST1 ssrhyp "}" ssrpattern_ne_squarep ssrrule_ne      (* ssr plugin *)
+| "{" LIST1 ssrhyp "}" ssrrule      (* ssr plugin *)
+| "{" ssrocc "}" ssrpattern_squarep ssrrule_ne      (* ssr plugin *)
+| "{" "}" ssrpattern_squarep ssrrule_ne      (* ssr plugin *)
+| ssrpattern_ne_squarep ssrrule_ne      (* ssr plugin *)
+| ssrrule_ne      (* ssr plugin *)
+]
+
+ssrrwargs: [
+| test_ssr_rw_syntax LIST1 ssrrwarg      (* ssr plugin *)
+]
+
+ssrunlockarg: [
+| "{" ssrocc "}" ssrterm      (* ssr plugin *)
+| ssrterm      (* ssr plugin *)
+]
+
+ssrunlockargs: [
+| LIST0 ssrunlockarg      (* ssr plugin *)
+]
+
+ssrsufffwd: [
+| ssrhpats LIST0 ssrbinder ":" ast_closure_lterm ssrhint      (* ssr plugin *)
+]
+
+ssrwlogfwd: [
+| ":" LIST0 ssrwgen "/" ast_closure_lterm      (* ssr plugin *)
+]
+
+ssr_idcomma: [
+|      (* ssr plugin *)
+| test_idcomma [ IDENT | "_" ] ","      (* ssr plugin *)
+]
+
+ssr_rtype: [
+| "return" operconstr100      (* ssr plugin *)
+]
+
+ssr_mpat: [
+| pattern200      (* ssr plugin *)
+]
+
+ssr_dpat: [
+| ssr_mpat "in" pattern200 ssr_rtype      (* ssr plugin *)
+| ssr_mpat ssr_rtype      (* ssr plugin *)
+| ssr_mpat      (* ssr plugin *)
+]
+
+ssr_dthen: [
+| ssr_dpat "then" lconstr      (* ssr plugin *)
+]
+
+ssr_elsepat: [
+| "else"      (* ssr plugin *)
+]
+
+ssr_else: [
+| ssr_elsepat lconstr      (* ssr plugin *)
+]
+
+ssr_search_item: [
+| string      (* ssr plugin *)
+| string "%" preident      (* ssr plugin *)
+| constr_pattern      (* ssr plugin *)
+]
+
+ssr_search_arg: [
+| "-" ssr_search_item ssr_search_arg      (* ssr plugin *)
+| ssr_search_item ssr_search_arg      (* ssr plugin *)
+|      (* ssr plugin *)
+]
+
+ssr_modlocs: [
+|      (* ssr plugin *)
+| "in" LIST1 modloc      (* ssr plugin *)
+]
+
+modloc: [
+| "-" global      (* ssr plugin *)
+| global      (* ssr plugin *)
+]
+
+ssrhintref: [
+| constr      (* ssr plugin *)
+| constr "|" natural      (* ssr plugin *)
+]
+
+ssrviewpos: [
+| "for" "move" "/"      (* ssr plugin *)
+| "for" "apply" "/"      (* ssr plugin *)
+| "for" "apply" "/" "/"      (* ssr plugin *)
+| "for" "apply" "//"      (* ssr plugin *)
+|      (* ssr plugin *)
+]
+
+ssrviewposspc: [
+| ssrviewpos      (* ssr plugin *)
+]
+
+rpattern: [
+| lconstr      (* ssrmatching plugin *)
+| "in" lconstr      (* ssrmatching plugin *)
+| lconstr "in" lconstr      (* ssrmatching plugin *)
+| "in" lconstr "in" lconstr      (* ssrmatching plugin *)
+| lconstr "in" lconstr "in" lconstr      (* ssrmatching plugin *)
+| lconstr "as" lconstr "in" lconstr      (* ssrmatching plugin *)
+]
+
+cpattern: [
+| "Qed" constr      (* ssrmatching plugin *)
+| ssrtermkind constr      (* ssrmatching plugin *)
+]
+
+lcpattern: [
+| "Qed" lconstr      (* ssrmatching plugin *)
+| ssrtermkind lconstr      (* ssrmatching plugin *)
+]
+
+ssrpatternarg: [
+| rpattern      (* ssrmatching plugin *)
+]
+
+numnotoption: [
+|
+| "(" "warning" "after" bigint ")"
+| "(" "abstract" "after" bigint ")"
+]
+
diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar
new file mode 100644
index 0000000000..cd6e11505c
--- /dev/null
+++ b/doc/tools/docgram/orderedGrammar
@@ -0,0 +1,4170 @@
+(* Defines the order to apply to editedGrammar to get productionlistGrammar.
+doc_grammar will modify this file to add/remove nonterminals and productions
+to match editedGrammar, which will remove comments.  Not compiled into Coq *)
+DOC_GRAMMAR
+
+global: [
+| reference
+]
+
+constr_pattern: [
+| term
+]
+
+sort: [
+| "Set"
+| "Prop"
+| "SProp"
+| "Type"
+| "Type" "@{" "_" "}"
+| "Type" "@{" universe "}"
+]
+
+sort_family: [
+| "Set"
+| "Prop"
+| "SProp"
+| "Type"
+]
+
+universe_increment: [
+| "+" natural
+| empty
+]
+
+universe_name: [
+| global
+| "Set"
+| "Prop"
+]
+
+universe_expr: [
+| universe_name universe_increment
+]
+
+universe: [
+| "max" "(" universe_expr_list_comma ")"
+| universe_expr
+]
+
+universe_expr_list_comma: [
+| universe_expr_list_comma "," universe_expr
+| universe_expr
+]
+
+lconstr: [
+| operconstr200
+| lconstr
+]
+
+term: [
+| operconstr8
+| "@" global instance
+]
+
+operconstr200: [
+| binder_constr
+| operconstr100
+]
+
+operconstr100: [
+| operconstr99 "<:" binder_constr
+| operconstr99 "<:" operconstr100
+| operconstr99 "<<:" binder_constr
+| operconstr99 "<<:" operconstr100
+| operconstr99 ":" binder_constr
+| operconstr99 ":" operconstr100
+| operconstr99 ":>"
+| operconstr99
+]
+
+operconstr99: [
+| operconstr90
+]
+
+operconstr90: [
+| operconstr10
+]
+
+operconstr10: [
+| operconstr9 appl_arg_list
+| "@" global instance operconstr9_list_opt
+| "@" pattern_identref ident_list
+| operconstr9
+]
+
+appl_arg_list: [
+| appl_arg_list appl_arg
+| appl_arg
+]
+
+operconstr9: [
+| ".." operconstr0 ".."
+| operconstr8
+]
+
+operconstr8: [
+| operconstr1
+]
+
+operconstr1: [
+| operconstr0 ".(" global appl_arg_list_opt ")"
+| operconstr0 ".(" "@" global operconstr9_list_opt ")"
+| operconstr0 "%" IDENT
+| operconstr0
+]
+
+appl_arg_list_opt: [
+| appl_arg_list_opt appl_arg
+| empty
+]
+
+operconstr9_list_opt: [
+| operconstr9_list_opt operconstr9
+| empty
+]
+
+operconstr0: [
+| atomic_constr
+| match_constr
+| "(" operconstr200 ")"
+| "{|" record_declaration bar_cbrace
+| "{" binder_constr "}"
+| "`{" operconstr200 "}"
+| "`(" operconstr200 ")"
+| "ltac" ":" "(" ltac_expr ")"
+]
+
+record_declaration: [
+| record_fields
+]
+
+record_fields: [
+| record_field_declaration ";" record_fields
+| record_field_declaration
+| empty
+| record_field ";" record_fields
+| record_field ";"
+| record_field
+]
+
+record_field_declaration: [
+| global binders ":=" lconstr
+]
+
+binder_constr: [
+| "forall" open_binders "," operconstr200
+| "fun" open_binders "=>" operconstr200
+| "let" name binders type_cstr ":=" operconstr200 "in" operconstr200
+| "let" single_fix "in" operconstr200
+| "let" name_alt return_type ":=" operconstr200 "in" operconstr200
+| "let" "'" pattern200 ":=" operconstr200 "in" operconstr200
+| "let" "'" pattern200 ":=" operconstr200 case_type "in" operconstr200
+| "let" "'" pattern200 "in" pattern200 ":=" operconstr200 case_type "in" operconstr200
+| "if" operconstr200 return_type "then" operconstr200 "else" operconstr200
+| fix_constr
+| "if" operconstr200 "is" ssr_dthen ssr_else      (* ssr plugin *)
+| "if" operconstr200 "isn't" ssr_dthen ssr_else      (* ssr plugin *)
+| "let" ":" ssr_mpat ":=" lconstr "in" lconstr      (* ssr plugin *)
+| "let" ":" ssr_mpat ":=" lconstr ssr_rtype "in" lconstr      (* ssr plugin *)
+| "let" ":" ssr_mpat "in" pattern200 ":=" lconstr ssr_rtype "in" lconstr      (* ssr plugin *)
+]
+
+name_alt: [
+| "(" name_list_comma_opt ")"
+| "()"
+]
+
+name_list_comma_opt: [
+| name_list_comma
+| empty
+]
+
+name_list_comma: [
+| name_list_comma "," name
+| name
+]
+
+name_list_opt: [
+| name_list_opt name
+| empty
+]
+
+name_list: [
+| name_list name
+| name
+]
+
+appl_arg: [
+| lpar_id_coloneq lconstr ")"
+| operconstr9
+]
+
+atomic_constr: [
+| global instance
+| sort
+| NUMERAL
+| string
+| "_"
+| "?" "[" ident "]"
+| "?" "[" "?" ident "]"
+| "?" ident evar_instance
+]
+
+inst: [
+| ident ":=" lconstr
+]
+
+evar_instance: [
+| "@{" inst_list_semi "}"
+| empty
+]
+
+inst_list_semi: [
+| inst_list_semi ";" inst
+| inst
+]
+
+instance: [
+| "@{" universe_level_list_opt "}"
+| empty
+]
+
+universe_level_list_opt: [
+| universe_level_list_opt universe_level
+| empty
+]
+
+universe_level: [
+| "Set"
+| "Prop"
+| "Type"
+| "_"
+| global
+]
+
+fix_constr: [
+| single_fix
+| single_fix "with" fix_decl_list "for" ident
+]
+
+fix_decl_list: [
+| fix_decl_list "with" fix_decl
+| fix_decl
+]
+
+single_fix: [
+| fix_kw fix_decl
+]
+
+fix_kw: [
+| "fix"
+| "cofix"
+]
+
+fix_decl: [
+| ident binders_fixannot type_cstr ":=" operconstr200
+]
+
+match_constr: [
+| "match" case_item_list_comma case_type_opt "with" branches "end"
+]
+
+case_item_list_comma: [
+| case_item_list_comma "," case_item
+| case_item
+]
+
+case_type_opt: [
+| case_type
+| empty
+]
+
+case_item: [
+| operconstr100 as_opt in_opt
+]
+
+as_opt2: [
+| as_opt case_type
+| empty
+]
+
+in_opt: [
+| "in" pattern200
+| empty
+]
+
+case_type: [
+| "return" operconstr100
+]
+
+return_type: [
+| as_opt2
+]
+
+as_opt3: [
+| "as" dirpath
+| empty
+]
+
+branches: [
+| or_opt eqn_list_or_opt
+]
+
+mult_pattern: [
+| pattern200_list_comma
+]
+
+pattern200_list_comma: [
+| pattern200_list_comma "," pattern200
+| pattern200
+]
+
+eqn: [
+| mult_pattern_list_or "=>" lconstr
+]
+
+mult_pattern_list_or: [
+| mult_pattern_list_or "|" mult_pattern
+| mult_pattern
+]
+
+record_pattern: [
+| global ":=" pattern200
+]
+
+record_patterns: [
+| record_pattern ";" record_patterns
+| record_pattern ";"
+| record_pattern
+| empty
+]
+
+pattern200: [
+| pattern100
+]
+
+pattern100: [
+| pattern99 ":" binder_constr
+| pattern99 ":" operconstr100
+| pattern99
+]
+
+pattern99: [
+| pattern90
+]
+
+pattern90: [
+| pattern10
+]
+
+pattern10: [
+| pattern1 "as" name
+| pattern1 pattern1_list
+| "@" reference pattern1_list_opt
+| pattern1
+]
+
+pattern1_list: [
+| pattern1_list pattern1
+| pattern1
+]
+
+pattern1_list_opt: [
+| pattern1_list_opt pattern1
+| empty
+]
+
+pattern1: [
+| pattern0 "%" IDENT
+| pattern0
+]
+
+pattern0: [
+| reference
+| "{|" record_patterns bar_cbrace
+| "_"
+| "(" pattern200 ")"
+| "(" pattern200 "|" pattern200_list_or ")"
+| NUMERAL
+| string
+]
+
+pattern200_list_or: [
+| pattern200_list_or "|" pattern200
+| pattern200
+]
+
+impl_ident_tail: [
+| "}"
+| name_list ":" lconstr "}"
+| name_list "}"
+| ":" lconstr "}"
+]
+
+fixannot: [
+| "{" "struct" ident "}"
+| "{" "wf" term ident "}"
+| "{" "measure" term ident_opt term_opt "}"
+| "{" "struct" name "}"
+| empty
+]
+
+term_opt: [
+| term
+| empty
+]
+
+impl_name_head: [
+| empty
+]
+
+binders_fixannot: [
+| impl_name_head impl_ident_tail binders_fixannot
+| fixannot
+| binder binders_fixannot
+| empty
+]
+
+open_binders: [
+| name name_list_opt ":" lconstr
+| name name_list_opt binders
+| name ".." name
+| closed_binder binders
+]
+
+binders: [
+| binder_list_opt
+]
+
+binder_list_opt: [
+| binder_list_opt binder
+| empty
+]
+
+binder: [
+| name
+| closed_binder
+]
+
+typeclass_constraint: [
+| "!" operconstr200
+| "{" name "}" ":" exclam_opt operconstr200
+| name_colon exclam_opt operconstr200
+| operconstr200
+]
+
+type_cstr: [
+| lconstr_opt
+| ":" lconstr
+| empty
+]
+
+preident: [
+| IDENT
+]
+
+pattern_identref: [
+| "?" ident
+]
+
+var: [
+| ident
+]
+
+field: [
+| FIELD
+]
+
+fields: [
+| field fields
+| field
+]
+
+fullyqualid: [
+| ident fields
+| ident
+]
+
+basequalid: [
+| ident fields
+| ident
+]
+
+name: [
+| "_"
+| ident
+]
+
+reference: [
+| ident fields
+| ident
+]
+
+by_notation: [
+| ne_string IDENT_opt
+]
+
+IDENT_opt: [
+| "%" IDENT
+| empty
+]
+
+smart_global: [
+| reference
+| by_notation
+]
+
+qualid: [
+| basequalid
+]
+
+ne_string: [
+| STRING
+]
+
+ne_lstring: [
+| ne_string
+]
+
+dirpath: [
+| ident field_list_opt
+]
+
+field_list_opt: [
+| field_list_opt field
+| empty
+]
+
+string: [
+| STRING
+]
+
+lstring: [
+| string
+]
+
+integer: [
+| NUMERAL
+| "-" NUMERAL
+]
+
+natural: [
+| NUMERAL
+]
+
+bigint: [
+| NUMERAL
+]
+
+bar_cbrace: [
+| "|" "}"
+]
+
+vernac_control: [
+| "Time" vernac_control
+| "Redirect" ne_string vernac_control
+| "Timeout" natural vernac_control
+| "Fail" vernac_control
+| decorated_vernac
+]
+
+decorated_vernac: [
+| quoted_attributes_list_opt vernac
+]
+
+quoted_attributes_list_opt: [
+| quoted_attributes_list_opt quoted_attributes
+| empty
+]
+
+quoted_attributes: [
+| "#[" attribute_list_comma_opt "]"
+]
+
+attribute_list_comma_opt: [
+| attribute_list_comma
+| empty
+]
+
+attribute_list_comma: [
+| attribute_list_comma "," attribute
+| attribute
+]
+
+attribute: [
+| ident attribute_value
+]
+
+attribute_value: [
+| "=" string
+| "(" attribute_list_comma_opt ")"
+| empty
+]
+
+vernac: [
+| "Local" vernac_poly
+| "Global" vernac_poly
+| vernac_poly
+]
+
+vernac_poly: [
+| "Polymorphic" vernac_aux
+| "Monomorphic" vernac_aux
+| vernac_aux
+]
+
+vernac_aux: [
+| "Program" gallina "."
+| "Program" gallina_ext "."
+| gallina "."
+| gallina_ext "."
+| command "."
+| syntax "."
+| subprf
+| command_entry
+]
+
+noedit_mode: [
+| query_command
+]
+
+subprf: [
+| BULLET
+| "{"
+| "}"
+]
+
+gallina: [
+| thm_token ident_decl binders ":" lconstr with_list_opt
+| assumption_token inline assum_list
+| assumptions_token inline assum_list
+| def_token ident_decl def_body
+| "Let" ident def_body
+| cumulativity_token_opt private_token finite_token inductive_definition_list
+| "Fixpoint" rec_definition_list
+| "Let" "Fixpoint" rec_definition_list
+| "CoFixpoint" corec_definition_list
+| "Let" "CoFixpoint" corec_definition_list
+| "Scheme" scheme_list
+| "Combined" "Scheme" ident "from" ident_list_comma
+| "Register" global "as" qualid
+| "Register" "Inline" global
+| "Primitive" ident lconstr_opt ":=" register_token
+| "Universe" ident_list
+| "Universes" ident_list
+| "Constraint" univ_constraint_list_comma
+]
+
+with_list_opt: [
+| with_list_opt "with" ident_decl binders ":" lconstr
+| empty
+]
+
+cumulativity_token_opt: [
+| cumulativity_token
+| empty
+]
+
+inductive_definition_list: [
+| inductive_definition_list "with" inductive_definition
+| inductive_definition
+]
+
+rec_definition_list: [
+| rec_definition_list "with" rec_definition
+| rec_definition
+]
+
+corec_definition_list: [
+| corec_definition_list "with" corec_definition
+| corec_definition
+]
+
+scheme_list: [
+| scheme_list "with" scheme
+| scheme
+]
+
+ident_list_comma: [
+| ident_list_comma "," ident
+| ident
+]
+
+univ_constraint_list_comma: [
+| univ_constraint_list_comma "," univ_constraint
+| univ_constraint
+]
+
+lconstr_opt2: [
+| ":=" lconstr
+| empty
+]
+
+register_token: [
+| register_prim_token
+| register_type_token
+]
+
+register_type_token: [
+| "#int63_type"
+]
+
+register_prim_token: [
+| "#int63_head0"
+| "#int63_tail0"
+| "#int63_add"
+| "#int63_sub"
+| "#int63_mul"
+| "#int63_div"
+| "#int63_mod"
+| "#int63_lsr"
+| "#int63_lsl"
+| "#int63_land"
+| "#int63_lor"
+| "#int63_lxor"
+| "#int63_addc"
+| "#int63_subc"
+| "#int63_addcarryc"
+| "#int63_subcarryc"
+| "#int63_mulc"
+| "#int63_diveucl"
+| "#int63_div21"
+| "#int63_addmuldiv"
+| "#int63_eq"
+| "#int63_lt"
+| "#int63_le"
+| "#int63_compare"
+]
+
+thm_token: [
+| "Theorem"
+| "Lemma"
+| "Fact"
+| "Remark"
+| "Corollary"
+| "Proposition"
+| "Property"
+]
+
+def_token: [
+| "Definition"
+| "Example"
+| "SubClass"
+]
+
+assumption_token: [
+| "Hypothesis"
+| "Variable"
+| "Axiom"
+| "Parameter"
+| "Conjecture"
+]
+
+assumptions_token: [
+| "Hypotheses"
+| "Variables"
+| "Axioms"
+| "Parameters"
+| "Conjectures"
+]
+
+inline: [
+| "Inline" "(" natural ")"
+| "Inline"
+| empty
+]
+
+univ_constraint: [
+| universe_name lt_alt universe_name
+]
+
+lt_alt: [
+| "<"
+| "="
+| "<="
+]
+
+univ_decl: [
+| "@{" ident_list_opt plus_opt univ_constraint_alt
+]
+
+plus_opt: [
+| "+"
+| empty
+]
+
+univ_constraint_alt: [
+| "|" univ_constraint_list_comma_opt plus_opt "}"
+| rbrace_alt
+]
+
+univ_constraint_list_comma_opt: [
+| univ_constraint_list_comma
+| empty
+]
+
+rbrace_alt: [
+| "}"
+| bar_cbrace
+]
+
+ident_decl: [
+| ident univ_decl_opt
+]
+
+finite_token: [
+| "Inductive"
+| "CoInductive"
+| "Variant"
+| "Record"
+| "Structure"
+| "Class"
+]
+
+cumulativity_token: [
+| "Cumulative"
+| "NonCumulative"
+]
+
+private_token: [
+| "Private"
+| empty
+]
+
+def_body: [
+| binders ":=" reduce lconstr
+| binders ":" lconstr ":=" reduce lconstr
+| binders ":" lconstr
+]
+
+reduce: [
+| "Eval" red_expr "in"
+| empty
+]
+
+one_decl_notation: [
+| ne_lstring ":=" term IDENT_opt2
+]
+
+IDENT_opt2: [
+| ":" IDENT
+| empty
+]
+
+decl_sep: [
+| "and"
+]
+
+decl_notation: [
+| "where" one_decl_notation_list
+| empty
+]
+
+one_decl_notation_list: [
+| one_decl_notation_list decl_sep one_decl_notation
+| one_decl_notation
+]
+
+opt_constructors_or_fields: [
+| ":=" constructor_list_or_record_decl
+| empty
+]
+
+inductive_definition: [
+| opt_coercion ident_decl binders lconstr_opt opt_constructors_or_fields decl_notation
+]
+
+constructor_list_or_record_decl: [
+| "|" constructor_list_or
+| ident constructor_type "|" constructor_list_or_opt
+| ident constructor_type
+| ident "{" record_fields "}"
+| "{" record_fields "}"
+| empty
+]
+
+constructor_list_or: [
+| constructor_list_or "|" constructor
+| constructor
+]
+
+constructor_list_or_opt: [
+| constructor_list_or
+| empty
+]
+
+opt_coercion: [
+| ">"
+| empty
+]
+
+rec_definition: [
+| ident_decl binders_fixannot type_cstr lconstr_opt2 decl_notation
+]
+
+corec_definition: [
+| ident_decl binders type_cstr lconstr_opt2 decl_notation
+]
+
+lconstr_opt: [
+| ":" lconstr
+| empty
+]
+
+scheme: [
+| scheme_kind
+| ident ":=" scheme_kind
+]
+
+scheme_kind: [
+| "Induction" "for" smart_global "Sort" sort_family
+| "Minimality" "for" smart_global "Sort" sort_family
+| "Elimination" "for" smart_global "Sort" sort_family
+| "Case" "for" smart_global "Sort" sort_family
+| "Equality" "for" smart_global
+]
+
+record_field: [
+| quoted_attributes_list_opt record_binder natural_opt2 decl_notation
+]
+
+record_binder_body: [
+| binders of_type_with_opt_coercion lconstr
+| binders of_type_with_opt_coercion lconstr ":=" lconstr
+| binders ":=" lconstr
+]
+
+record_binder: [
+| name
+| name record_binder_body
+]
+
+assum_list: [
+| assum_coe_list
+| simple_assum_coe
+]
+
+assum_coe_list: [
+| assum_coe_list assum_coe
+| assum_coe
+]
+
+assum_coe: [
+| "(" simple_assum_coe ")"
+]
+
+simple_assum_coe: [
+| ident_decl_list of_type_with_opt_coercion lconstr
+]
+
+ident_decl_list: [
+| ident_decl_list ident_decl
+| ident_decl
+]
+
+constructor_type: [
+| binders of_type_with_opt_coercion_opt
+]
+
+of_type_with_opt_coercion_opt: [
+| of_type_with_opt_coercion lconstr
+| empty
+]
+
+constructor: [
+| ident constructor_type
+]
+
+of_type_with_opt_coercion: [
+| ":>>"
+| ":>" ">"
+| ":>"
+| ":" ">" ">"
+| ":" ">"
+| ":"
+]
+
+gallina_ext: [
+| "Module" export_token ident module_binder_list_opt of_module_type is_module_expr
+| "Module" "Type" ident module_binder_list_opt check_module_types is_module_type
+| "Declare" "Module" export_token ident module_binder_list_opt ":" module_type_inl
+| "Section" ident
+| "Chapter" ident
+| "End" ident
+| "Collection" ident ":=" section_subset_expr
+| "Require" export_token global_list
+| "From" global "Require" export_token global_list
+| "Import" global_list
+| "Export" global_list
+| "Include" module_type_inl ext_module_expr_list_opt
+| "Include" "Type" module_type_inl ext_module_type_list_opt
+| "Transparent" smart_global_list
+| "Opaque" smart_global_list
+| "Strategy" strategy_level_list
+| "Canonical" Structure_opt global univ_decl_opt2
+| "Canonical" Structure_opt by_notation
+| "Coercion" global univ_decl_opt def_body
+| "Identity" "Coercion" ident ":" class_rawexpr ">->" class_rawexpr
+| "Coercion" global ":" class_rawexpr ">->" class_rawexpr
+| "Coercion" by_notation ":" class_rawexpr ">->" class_rawexpr
+| "Context" binder_list
+| "Instance" instance_name ":" operconstr200 hint_info record_declaration_opt
+| "Existing" "Instance" global hint_info
+| "Existing" "Instances" global_list natural_opt2
+| "Existing" "Class" global
+| "Arguments" smart_global argument_spec_block_list_opt more_implicits_block_opt arguments_modifier_opt
+| "Implicit" "Type" reserv_list
+| "Implicit" "Types" reserv_list
+| "Generalizable" All_alt
+| "Export" "Set" option_table option_setting
+| "Export" "Unset" option_table
+| "Import" "Prenex" "Implicits"      (* ssr plugin *)
+]
+
+module_binder_list_opt: [
+| module_binder_list_opt module_binder
+| empty
+]
+
+ext_module_expr_list_opt: [
+| ext_module_expr_list_opt ext_module_expr
+| empty
+]
+
+ext_module_type_list_opt: [
+| ext_module_type_list_opt ext_module_type
+| empty
+]
+
+strategy_level_list: [
+| strategy_level_list strategy_level "[" smart_global_list "]"
+| strategy_level "[" smart_global_list "]"
+]
+
+Structure_opt: [
+| "Structure"
+| empty
+]
+
+univ_decl_opt: [
+| univ_decl
+| empty
+]
+
+binder_list: [
+| binder_list binder
+| binder
+]
+
+record_declaration_opt: [
+| ":=" "{" record_declaration "}"
+| ":=" lconstr
+| empty
+]
+
+natural_opt: [
+| natural
+| empty
+]
+
+argument_spec_block_list_opt: [
+| argument_spec_block_list_opt argument_spec_block
+| empty
+]
+
+more_implicits_block_opt: [
+| "," more_implicits_block_list_comma
+| empty
+]
+
+more_implicits_block_list_comma: [
+| more_implicits_block_list_comma "," more_implicits_block_list_opt
+| more_implicits_block_list_opt
+]
+
+arguments_modifier_opt: [
+| ":" arguments_modifier_list_comma
+| empty
+]
+
+arguments_modifier_list_comma: [
+| arguments_modifier_list_comma "," arguments_modifier
+| arguments_modifier
+]
+
+All_alt: [
+| "All" "Variables"
+| "No" "Variables"
+| Variable_alt ident_list
+]
+
+Variable_alt: [
+| "Variable"
+| "Variables"
+]
+
+more_implicits_block_list_opt: [
+| more_implicits_block_list_opt more_implicits_block
+| empty
+]
+
+univ_decl_opt2: [
+| univ_decl_opt def_body
+| empty
+]
+
+export_token: [
+| "Import"
+| "Export"
+| empty
+]
+
+ext_module_type: [
+| "<+" module_type_inl
+]
+
+ext_module_expr: [
+| "<+" module_expr_inl
+]
+
+check_module_type: [
+| "<:" module_type_inl
+]
+
+check_module_types: [
+| check_module_type_list_opt
+]
+
+check_module_type_list_opt: [
+| check_module_type_list_opt check_module_type
+| empty
+]
+
+of_module_type: [
+| ":" module_type_inl
+| check_module_types
+]
+
+is_module_type: [
+| ":=" module_type_inl ext_module_type_list_opt
+| empty
+]
+
+is_module_expr: [
+| ":=" module_expr_inl ext_module_expr_list_opt
+| empty
+]
+
+functor_app_annot: [
+| "[" "inline" "at" "level" natural "]"
+| "[" "no" "inline" "]"
+| empty
+]
+
+module_expr_inl: [
+| "!" module_expr
+| module_expr functor_app_annot
+]
+
+module_type_inl: [
+| "!" module_type
+| module_type functor_app_annot
+]
+
+module_binder: [
+| "(" export_token ident_list ":" module_type_inl ")"
+]
+
+module_expr: [
+| module_expr_atom
+| module_expr module_expr_atom
+]
+
+module_expr_atom: [
+| qualid
+| "(" module_expr ")"
+]
+
+with_declaration: [
+| "Definition" fullyqualid univ_decl_opt ":=" lconstr
+| "Module" fullyqualid ":=" qualid
+]
+
+module_type: [
+| qualid
+| "(" module_type ")"
+| module_type module_expr_atom
+| module_type "with" with_declaration
+]
+
+section_subset_expr: [
+| starredidentref_list_opt
+| ssexpr35
+]
+
+starredidentref_list_opt: [
+| starredidentref_list_opt starredidentref
+| empty
+]
+
+starredidentref: [
+| ident
+| ident "*"
+| "Type"
+| "Type" "*"
+]
+
+ssexpr35: [
+| "-" ssexpr50
+| ssexpr50
+]
+
+ssexpr50: [
+| ssexpr0 "-" ssexpr0
+| ssexpr0 "+" ssexpr0
+| ssexpr0
+]
+
+ssexpr0: [
+| starredidentref
+| "(" starredidentref_list_opt ")"
+| "(" starredidentref_list_opt ")" "*"
+| "(" ssexpr35 ")"
+| "(" ssexpr35 ")" "*"
+]
+
+arguments_modifier: [
+| "simpl" "nomatch"
+| "simpl" "never"
+| "default" "implicits"
+| "clear" "implicits"
+| "clear" "scopes"
+| "clear" "bidirectionality" "hint"
+| "rename"
+| "assert"
+| "extra" "scopes"
+| "clear" "scopes" "and" "implicits"
+| "clear" "implicits" "and" "scopes"
+]
+
+scope: [
+| "%" IDENT
+]
+
+argument_spec: [
+| exclam_opt name scope_opt
+]
+
+exclam_opt: [
+| "!"
+| empty
+]
+
+scope_opt: [
+| scope
+| empty
+]
+
+argument_spec_block: [
+| argument_spec
+| "/"
+| "&"
+| "(" argument_spec_list ")" scope_opt
+| "[" argument_spec_list "]" scope_opt
+| "{" argument_spec_list "}" scope_opt
+]
+
+argument_spec_list: [
+| argument_spec_list argument_spec
+| argument_spec
+]
+
+more_implicits_block: [
+| name
+| "[" name_list "]"
+| "{" name_list "}"
+]
+
+strategy_level: [
+| "expand"
+| "opaque"
+| integer
+| "transparent"
+]
+
+instance_name: [
+| ident_decl binders
+| empty
+]
+
+hint_info: [
+| "|" natural_opt constr_pattern_opt
+| empty
+]
+
+reserv_list: [
+| reserv_tuple_list
+| simple_reserv
+]
+
+reserv_tuple_list: [
+| reserv_tuple_list reserv_tuple
+| reserv_tuple
+]
+
+reserv_tuple: [
+| "(" simple_reserv ")"
+]
+
+simple_reserv: [
+| ident_list ":" lconstr
+]
+
+command: [
+| "Comments" comment_list_opt
+| "Declare" "Instance" ident_decl binders ":" operconstr200 hint_info
+| "Declare" "Scope" IDENT
+| "Pwd"
+| "Cd"
+| "Cd" ne_string
+| "Load" Verbose_opt ne_string_alt
+| "Declare" "ML" "Module" ne_string_list
+| "Locate" locatable
+| "Add" "LoadPath" ne_string as_dirpath
+| "Add" "Rec" "LoadPath" ne_string as_dirpath
+| "Remove" "LoadPath" ne_string
+| "AddPath" ne_string "as" as_dirpath
+| "AddRecPath" ne_string "as" as_dirpath
+| "DelPath" ne_string
+| "Type" lconstr
+| "Print" printable
+| "Print" smart_global univ_name_list_opt
+| "Print" "Module" "Type" global
+| "Print" "Module" global
+| "Print" "Namespace" dirpath
+| "Inspect" natural
+| "Add" "ML" "Path" ne_string
+| "Add" "Rec" "ML" "Path" ne_string
+| "Set" option_table option_setting
+| "Unset" option_table
+| "Print" "Table" option_table
+| "Add" IDENT IDENT option_ref_value_list
+| "Add" IDENT option_ref_value_list
+| "Test" option_table "for" option_ref_value_list
+| "Test" option_table
+| "Remove" IDENT IDENT option_ref_value_list
+| "Remove" IDENT option_ref_value_list
+| "Write" "State" IDENT
+| "Write" "State" ne_string
+| "Restore" "State" IDENT
+| "Restore" "State" ne_string
+| "Reset" "Initial"
+| "Reset" ident
+| "Back"
+| "Back" natural
+| "BackTo" natural
+| "Debug" "On"
+| "Debug" "Off"
+| "Declare" "Reduction" IDENT; ":=" red_expr
+| "Declare" "Custom" "Entry" IDENT
+| "Goal" lconstr
+| "Proof"
+| "Proof" "Mode" string
+| "Proof" lconstr
+| "Abort"
+| "Abort" "All"
+| "Abort" ident
+| "Existential" natural constr_body
+| "Admitted"
+| "Qed"
+| "Save" ident
+| "Defined"
+| "Defined" ident
+| "Restart"
+| "Undo"
+| "Undo" natural
+| "Undo" "To" natural
+| "Focus"
+| "Focus" natural
+| "Unfocus"
+| "Unfocused"
+| "Show"
+| "Show" natural
+| "Show" ident
+| "Show" "Existentials"
+| "Show" "Universes"
+| "Show" "Conjectures"
+| "Show" "Proof"
+| "Show" "Intro"
+| "Show" "Intros"
+| "Show" "Match" reference
+| "Guarded"
+| "Create" "HintDb" IDENT discriminated_opt
+| "Remove" "Hints" global_list opt_hintbases
+| "Hint" hint opt_hintbases
+| "Obligation" integer "of" ident ":" lglob withtac
+| "Obligation" integer "of" ident withtac
+| "Obligation" integer ":" lglob withtac
+| "Obligation" integer withtac
+| "Next" "Obligation" "of" ident withtac
+| "Next" "Obligation" withtac
+| "Solve" "Obligation" integer "of" ident "with" tactic
+| "Solve" "Obligation" integer "with" tactic
+| "Solve" "Obligations" "of" ident "with" tactic
+| "Solve" "Obligations" "with" tactic
+| "Solve" "Obligations"
+| "Solve" "All" "Obligations" "with" tactic
+| "Solve" "All" "Obligations"
+| "Admit" "Obligations" "of" ident
+| "Admit" "Obligations"
+| "Obligation" "Tactic" ":=" tactic
+| "Show" "Obligation" "Tactic"
+| "Obligations" "of" ident
+| "Obligations"
+| "Preterm" "of" ident
+| "Preterm"
+| "Hint" "Rewrite" orient term_list ":" preident_list_opt
+| "Hint" "Rewrite" orient term_list "using" tactic ":" preident_list_opt
+| "Hint" "Rewrite" orient term_list
+| "Hint" "Rewrite" orient term_list "using" tactic
+| "Derive" "Inversion_clear" ident "with" term "Sort" sort_family
+| "Derive" "Inversion_clear" ident "with" term
+| "Derive" "Inversion" ident "with" term "Sort" sort_family
+| "Derive" "Inversion" ident "with" term
+| "Derive" "Dependent" "Inversion" ident "with" term "Sort" sort_family
+| "Derive" "Dependent" "Inversion_clear" ident "with" term "Sort" sort_family
+| "Declare" "Left" "Step" term
+| "Declare" "Right" "Step" term
+| "Grab" "Existential" "Variables"
+| "Unshelve"
+| "Declare" "Equivalent" "Keys" term term
+| "Print" "Equivalent" "Keys"
+| "Optimize" "Proof"
+| "Optimize" "Heap"
+| "Reset" "Ltac" "Profile"
+| "Show" "Ltac" "Profile"
+| "Show" "Ltac" "Profile" "CutOff" int
+| "Show" "Ltac" "Profile" string
+| "Hint" "Cut" "[" hints_path "]" opthints
+| "Typeclasses" "Transparent" reference_list_opt
+| "Typeclasses" "Opaque" reference_list_opt
+| "Typeclasses" "eauto" ":=" debug eauto_search_strategy int_opt
+| "Add" "Relation" term term "reflexivity" "proved" "by" term "symmetry" "proved" "by" term "as" ident
+| "Add" "Relation" term term "reflexivity" "proved" "by" term "as" ident
+| "Add" "Relation" term term "as" ident
+| "Add" "Relation" term term "symmetry" "proved" "by" term "as" ident
+| "Add" "Relation" term term "symmetry" "proved" "by" term "transitivity" "proved" "by" term "as" ident
+| "Add" "Relation" term term "reflexivity" "proved" "by" term "transitivity" "proved" "by" term "as" ident
+| "Add" "Relation" term term "reflexivity" "proved" "by" term "symmetry" "proved" "by" term "transitivity" "proved" "by" term "as" ident
+| "Add" "Relation" term term "transitivity" "proved" "by" term "as" ident
+| "Add" "Parametric" "Relation" binders ":" term term "reflexivity" "proved" "by" term "symmetry" "proved" "by" term "as" ident
+| "Add" "Parametric" "Relation" binders ":" term term "reflexivity" "proved" "by" term "as" ident
+| "Add" "Parametric" "Relation" binders ":" term term "as" ident
+| "Add" "Parametric" "Relation" binders ":" term term "symmetry" "proved" "by" term "as" ident
+| "Add" "Parametric" "Relation" binders ":" term term "symmetry" "proved" "by" term "transitivity" "proved" "by" term "as" ident
+| "Add" "Parametric" "Relation" binders ":" term term "reflexivity" "proved" "by" term "transitivity" "proved" "by" term "as" ident
+| "Add" "Parametric" "Relation" binders ":" term term "reflexivity" "proved" "by" term "symmetry" "proved" "by" term "transitivity" "proved" "by" term "as" ident
+| "Add" "Parametric" "Relation" binders ":" term term "transitivity" "proved" "by" term "as" ident
+| "Add" "Setoid" term term term "as" ident
+| "Add" "Parametric" "Setoid" binders ":" term term term "as" ident
+| "Add" "Morphism" term ":" ident
+| "Declare" "Morphism" term ":" ident
+| "Add" "Morphism" term "with" "signature" lconstr "as" ident
+| "Add" "Parametric" "Morphism" binders ":" term "with" "signature" lconstr "as" ident
+| "Print" "Rewrite" "HintDb" preident
+| "Proof" "with" tactic using_opt
+| "Proof" "using" section_subset_expr with_opt
+| "Tactic" "Notation" ltac_tactic_level_opt ltac_production_item_list ":=" tactic
+| "Print" "Ltac" reference
+| "Locate" "Ltac" reference
+| "Ltac" ltac_tacdef_body_list
+| "Print" "Ltac" "Signatures"
+| "String" "Notation" reference reference reference ":" ident
+| "Set" "Firstorder" "Solver" tactic
+| "Print" "Firstorder" "Solver"
+| "Numeral" "Notation" reference reference reference ":" ident numnotoption
+| "Derive" ident "SuchThat" term "As" ident      (* derive plugin *)
+| "Extraction" global      (* extraction plugin *)
+| "Recursive" "Extraction" global_list      (* extraction plugin *)
+| "Extraction" string global_list      (* extraction plugin *)
+| "Extraction" "TestCompile" global_list      (* extraction plugin *)
+| "Separate" "Extraction" global_list      (* extraction plugin *)
+| "Extraction" "Library" ident      (* extraction plugin *)
+| "Recursive" "Extraction" "Library" ident      (* extraction plugin *)
+| "Extraction" "Language" language      (* extraction plugin *)
+| "Extraction" "Inline" global_list      (* extraction plugin *)
+| "Extraction" "NoInline" global_list      (* extraction plugin *)
+| "Print" "Extraction" "Inline"      (* extraction plugin *)
+| "Reset" "Extraction" "Inline"      (* extraction plugin *)
+| "Extraction" "Implicit" global "[" int_or_id_list_opt "]"      (* extraction plugin *)
+| "Extraction" "Blacklist" ident_list      (* extraction plugin *)
+| "Print" "Extraction" "Blacklist"      (* extraction plugin *)
+| "Reset" "Extraction" "Blacklist"      (* extraction plugin *)
+| "Extract" "Constant" global string_list_opt "=>" mlname      (* extraction plugin *)
+| "Extract" "Inlined" "Constant" global "=>" mlname      (* extraction plugin *)
+| "Extract" "Inductive" global "=>" mlname "[" mlname_list_opt "]" string_opt      (* extraction plugin *)
+| "Show" "Extraction"      (* extraction plugin *)
+| "Function" function_rec_definition_loc_list      (* funind plugin *)
+| "Functional" "Scheme" fun_scheme_arg_list      (* funind plugin *)
+| "Functional" "Case" fun_scheme_arg      (* funind plugin *)
+| "Generate" "graph" "for" reference      (* funind plugin *)
+| "Add" "Ring" ident ":" term ring_mods_opt      (* setoid_ring plugin *)
+| "Print" "Rings"      (* setoid_ring plugin *)
+| "Add" "Field" ident ":" term field_mods_opt      (* setoid_ring plugin *)
+| "Print" "Fields"      (* setoid_ring plugin *)
+| "Prenex" "Implicits" global_list      (* ssr plugin *)
+| "Search" ssr_search_arg ssr_modlocs      (* ssr plugin *)
+| "Print" "Hint" "View" ssrviewpos      (* ssr plugin *)
+| "Hint" "View" ssrviewposspc ssrhintref_list      (* ssr plugin *)
+]
+
+comment_list_opt: [
+| comment_list_opt comment
+| empty
+]
+
+Verbose_opt: [
+| "Verbose"
+| empty
+]
+
+ne_string_alt: [
+| ne_string
+| IDENT
+]
+
+ne_string_list: [
+| ne_string_list ne_string
+| ne_string
+]
+
+univ_name_list_opt: [
+| univ_name_list
+| empty
+]
+
+option_ref_value_list: [
+| option_ref_value_list option_ref_value
+| option_ref_value
+]
+
+discriminated_opt: [
+| "discriminated"
+| empty
+]
+
+global_list: [
+| global_list global
+| global
+]
+
+preident_list_opt: [
+| preident_list_opt preident
+| empty
+]
+
+reference_list_opt: [
+| reference_list_opt reference
+| empty
+]
+
+int_opt: [
+| int
+| empty
+]
+
+using_opt: [
+| "using" section_subset_expr
+| empty
+]
+
+with_opt: [
+| "with" tactic
+| empty
+]
+
+ltac_tactic_level_opt: [
+| ltac_tactic_level
+| empty
+]
+
+ltac_production_item_list: [
+| ltac_production_item_list ltac_production_item
+| ltac_production_item
+]
+
+ltac_tacdef_body_list: [
+| ltac_tacdef_body_list "with" ltac_tacdef_body
+| ltac_tacdef_body
+]
+
+int_or_id_list_opt: [
+| int_or_id_list_opt int_or_id
+| empty
+]
+
+ident_list: [
+| ident_list ident
+| ident
+]
+
+string_list_opt: [
+| string_list_opt string
+| empty
+]
+
+mlname_list_opt: [
+| mlname_list_opt mlname
+| empty
+]
+
+string_opt: [
+| string
+| empty
+]
+
+function_rec_definition_loc_list: [
+| function_rec_definition_loc_list "with" function_rec_definition_loc
+| function_rec_definition_loc
+]
+
+fun_scheme_arg_list: [
+| fun_scheme_arg_list "with" fun_scheme_arg
+| fun_scheme_arg
+]
+
+ring_mods_opt: [
+| ring_mods
+| empty
+]
+
+field_mods_opt: [
+| field_mods
+| empty
+]
+
+ssrhintref_list: [
+| ssrhintref_list ssrhintref
+| ssrhintref
+]
+
+query_command: [
+| "Eval" red_expr "in" lconstr "."
+| "Compute" lconstr "."
+| "Check" lconstr "."
+| "About" smart_global univ_name_list_opt "."
+| "SearchHead" constr_pattern in_or_out_modules "."
+| "SearchPattern" constr_pattern in_or_out_modules "."
+| "SearchRewrite" constr_pattern in_or_out_modules "."
+| "Search" searchabout_query searchabout_queries "."
+| "SearchAbout" searchabout_query searchabout_queries "."
+| "SearchAbout" "[" searchabout_query_list "]" in_or_out_modules "."
+]
+
+searchabout_query_list: [
+| searchabout_query_list searchabout_query
+| searchabout_query
+]
+
+printable: [
+| "Term" smart_global univ_name_list_opt
+| "All"
+| "Section" global
+| "Grammar" IDENT
+| "Custom" "Grammar" IDENT
+| "LoadPath" dirpath_opt
+| "Modules"
+| "Libraries"
+| "ML" "Path"
+| "ML" "Modules"
+| "Debug" "GC"
+| "Graph"
+| "Classes"
+| "TypeClasses"
+| "Instances" smart_global
+| "Coercions"
+| "Coercion" "Paths" class_rawexpr class_rawexpr
+| "Canonical" "Projections"
+| "Tables"
+| "Options"
+| "Hint"
+| "Hint" smart_global
+| "Hint" "*"
+| "HintDb" IDENT
+| "Scopes"
+| "Scope" IDENT
+| "Visibility" IDENT_opt3
+| "Implicit" smart_global
+| Sorted_opt "Universes" printunivs_subgraph_opt ne_string_opt
+| "Assumptions" smart_global
+| "Opaque" "Dependencies" smart_global
+| "Transparent" "Dependencies" smart_global
+| "All" "Dependencies" smart_global
+| "Strategy" smart_global
+| "Strategies"
+| "Registered"
+]
+
+dirpath_opt: [
+| dirpath
+| empty
+]
+
+IDENT_opt3: [
+| IDENT
+| empty
+]
+
+Sorted_opt: [
+| "Sorted"
+| empty
+]
+
+printunivs_subgraph_opt: [
+| printunivs_subgraph
+| empty
+]
+
+ne_string_opt: [
+| ne_string
+| empty
+]
+
+printunivs_subgraph: [
+| "Subgraph" "(" reference_list_opt ")"
+]
+
+class_rawexpr: [
+| "Funclass"
+| "Sortclass"
+| smart_global
+]
+
+locatable: [
+| smart_global
+| "Term" smart_global
+| "File" ne_string
+| "Library" global
+| "Module" global
+]
+
+option_setting: [
+| empty
+| integer
+| STRING
+]
+
+option_ref_value: [
+| global
+| STRING
+]
+
+option_table: [
+| IDENT_list
+]
+
+as_dirpath: [
+| as_opt3
+]
+
+as_opt: [
+| "as" name
+| empty
+]
+
+ne_in_or_out_modules: [
+| "inside" global_list
+| "outside" global_list
+]
+
+in_or_out_modules: [
+| ne_in_or_out_modules
+| empty
+]
+
+comment: [
+| term
+| STRING
+| natural
+]
+
+positive_search_mark: [
+| "-"
+| empty
+]
+
+searchabout_query: [
+| positive_search_mark ne_string scope_opt
+| positive_search_mark constr_pattern
+]
+
+searchabout_queries: [
+| ne_in_or_out_modules
+| searchabout_query searchabout_queries
+| empty
+]
+
+univ_name_list: [
+| "@{" name_list_opt "}"
+]
+
+syntax: [
+| "Open" "Scope" IDENT
+| "Close" "Scope" IDENT
+| "Delimit" "Scope" IDENT; "with" IDENT
+| "Undelimit" "Scope" IDENT
+| "Bind" "Scope" IDENT; "with" class_rawexpr_list
+| "Infix" ne_lstring ":=" term syntax_modifier_opt IDENT_opt2
+| "Notation" ident ident_list_opt ":=" term only_parsing
+| "Notation" lstring ":=" term syntax_modifier_opt IDENT_opt2
+| "Format" "Notation" STRING STRING STRING
+| "Reserved" "Infix" ne_lstring syntax_modifier_opt
+| "Reserved" "Notation" ne_lstring syntax_modifier_opt
+]
+
+class_rawexpr_list: [
+| class_rawexpr_list class_rawexpr
+| class_rawexpr
+]
+
+syntax_modifier_opt: [
+| "(" syntax_modifier_list_comma ")"
+| empty
+]
+
+syntax_modifier_list_comma: [
+| syntax_modifier_list_comma "," syntax_modifier
+| syntax_modifier
+]
+
+only_parsing: [
+| "(" "only" "parsing" ")"
+| "(" "compat" STRING ")"
+| empty
+]
+
+level: [
+| "level" natural
+| "next" "level"
+]
+
+syntax_modifier: [
+| "at" "level" natural
+| "in" "custom" IDENT
+| "in" "custom" IDENT; "at" "level" natural
+| "left" "associativity"
+| "right" "associativity"
+| "no" "associativity"
+| "only" "printing"
+| "only" "parsing"
+| "compat" STRING
+| "format" STRING STRING_opt
+| IDENT; "," IDENT_list_comma "at" level
+| IDENT; "at" level
+| IDENT; "at" level constr_as_binder_kind
+| IDENT constr_as_binder_kind
+| IDENT syntax_extension_type
+]
+
+STRING_opt: [
+| STRING
+| empty
+]
+
+IDENT_list_comma: [
+| IDENT_list_comma "," IDENT
+| IDENT
+]
+
+syntax_extension_type: [
+| "ident"
+| "global"
+| "bigint"
+| "binder"
+| "constr"
+| "constr" at_level_opt constr_as_binder_kind_opt
+| "pattern"
+| "pattern" "at" "level" natural
+| "strict" "pattern"
+| "strict" "pattern" "at" "level" natural
+| "closed" "binder"
+| "custom" IDENT at_level_opt constr_as_binder_kind_opt
+]
+
+at_level_opt: [
+| at_level
+| empty
+]
+
+constr_as_binder_kind_opt: [
+| constr_as_binder_kind
+| empty
+]
+
+at_level: [
+| "at" level
+]
+
+constr_as_binder_kind: [
+| "as" "ident"
+| "as" "pattern"
+| "as" "strict" "pattern"
+]
+
+opt_hintbases: [
+| empty
+| ":" IDENT_list
+]
+
+IDENT_list: [
+| IDENT_list IDENT
+| IDENT
+]
+
+reference_or_constr: [
+| global
+| term
+]
+
+hint: [
+| "Resolve" reference_or_constr_list hint_info
+| "Resolve" "->" global_list natural_opt
+| "Resolve" "<-" global_list natural_opt
+| "Immediate" reference_or_constr_list
+| "Variables" "Transparent"
+| "Variables" "Opaque"
+| "Constants" "Transparent"
+| "Constants" "Opaque"
+| "Transparent" global_list
+| "Opaque" global_list
+| "Mode" global mode
+| "Unfold" global_list
+| "Constructors" global_list
+| "Extern" natural constr_pattern_opt "=>" tactic
+]
+
+reference_or_constr_list: [
+| reference_or_constr_list reference_or_constr
+| reference_or_constr
+]
+
+natural_opt2: [
+| "|" natural
+| empty
+]
+
+constr_pattern_opt: [
+| constr_pattern
+| empty
+]
+
+constr_body: [
+| ":=" lconstr
+| ":" lconstr ":=" lconstr
+]
+
+mode: [
+| plus_list
+]
+
+plus_list: [
+| plus_list plus_alt
+| plus_alt
+]
+
+plus_alt: [
+| "+"
+| "!"
+| "-"
+]
+
+vernac_toplevel: [
+| "Drop" "."
+| "Quit" "."
+| "Backtrack" natural natural natural "."
+| "Show" "Goal" natural "at" natural "."
+| vernac_control
+]
+
+orient: [
+| "->"
+| "<-"
+| empty
+]
+
+occurrences: [
+| integer_list
+| var
+]
+
+integer_list: [
+| integer_list integer
+| integer
+]
+
+glob: [
+| term
+]
+
+lglob: [
+| lconstr
+]
+
+casted_constr: [
+| term
+]
+
+hloc: [
+| empty
+| "in" "|-" "*"
+| "in" ident
+| "in" "(" "Type" "of" ident ")"
+| "in" "(" "Value" "of" ident ")"
+| "in" "(" "type" "of" ident ")"
+| "in" "(" "value" "of" ident ")"
+]
+
+rename: [
+| ident "into" ident
+]
+
+by_arg_tac: [
+| "by" ltac_expr3
+| empty
+]
+
+in_clause: [
+| in_clause
+| "*" occs
+| "*" "|-" concl_occ
+| hypident_occ_list_comma_opt "|-" concl_occ
+| hypident_occ_list_comma_opt
+]
+
+hypident_occ_list_comma_opt: [
+| hypident_occ_list_comma
+| empty
+]
+
+hypident_occ_list_comma: [
+| hypident_occ_list_comma "," hypident_occ
+| hypident_occ
+]
+
+test_lpar_id_colon: [
+| empty
+]
+
+withtac: [
+| "with" tactic
+| empty
+]
+
+closed_binder: [
+| "(" name name_list ":" lconstr ")"
+| "(" name ":" lconstr ")"
+| "(" name ":=" lconstr ")"
+| "(" name ":" lconstr ":=" lconstr ")"
+| "{" name "}"
+| "{" name name_list ":" lconstr "}"
+| "{" name ":" lconstr "}"
+| "{" name name_list "}"
+| "`(" typeclass_constraint_list_comma ")"
+| "`{" typeclass_constraint_list_comma "}"
+| "'" pattern0
+| of_alt operconstr99      (* ssr plugin *)
+| "(" "_" ":" lconstr "|" lconstr ")"
+]
+
+typeclass_constraint_list_comma: [
+| typeclass_constraint_list_comma "," typeclass_constraint
+| typeclass_constraint
+]
+
+of_alt: [
+| "of"
+| "&"
+]
+
+simple_tactic: [
+| "reflexivity"
+| "exact" casted_constr
+| "assumption"
+| "etransitivity"
+| "cut" term
+| "exact_no_check" term
+| "vm_cast_no_check" term
+| "native_cast_no_check" term
+| "casetype" term
+| "elimtype" term
+| "lapply" term
+| "transitivity" term
+| "left"
+| "eleft"
+| "left" "with" bindings
+| "eleft" "with" bindings
+| "right"
+| "eright"
+| "right" "with" bindings
+| "eright" "with" bindings
+| "constructor"
+| "constructor" int_or_var
+| "constructor" int_or_var "with" bindings
+| "econstructor"
+| "econstructor" int_or_var
+| "econstructor" int_or_var "with" bindings
+| "specialize" constr_with_bindings
+| "specialize" constr_with_bindings "as" simple_intropattern
+| "symmetry"
+| "symmetry" "in" in_clause
+| "split"
+| "esplit"
+| "split" "with" bindings
+| "esplit" "with" bindings
+| "exists"
+| "exists" bindings_list_comma
+| "eexists"
+| "eexists" bindings_list_comma
+| "intros" "until" quantified_hypothesis
+| "intro"
+| "intro" ident
+| "intro" ident "at" "top"
+| "intro" ident "at" "bottom"
+| "intro" ident "after" var
+| "intro" ident "before" var
+| "intro" "at" "top"
+| "intro" "at" "bottom"
+| "intro" "after" var
+| "intro" "before" var
+| "move" var "at" "top"
+| "move" var "at" "bottom"
+| "move" var "after" var
+| "move" var "before" var
+| "rename" rename_list_comma
+| "revert" var_list
+| "simple" "induction" quantified_hypothesis
+| "simple" "destruct" quantified_hypothesis
+| "double" "induction" quantified_hypothesis quantified_hypothesis
+| "admit"
+| "fix" ident natural
+| "cofix" ident
+| "clear" var_list_opt
+| "clear" "-" var_list
+| "clearbody" var_list
+| "generalize" "dependent" term
+| "replace" uconstr "with" term clause_dft_concl by_arg_tac
+| "replace" "->" uconstr clause_dft_concl
+| "replace" "<-" uconstr clause_dft_concl
+| "replace" uconstr clause_dft_concl
+| "simplify_eq"
+| "simplify_eq" destruction_arg
+| "esimplify_eq"
+| "esimplify_eq" destruction_arg
+| "discriminate"
+| "discriminate" destruction_arg
+| "ediscriminate"
+| "ediscriminate" destruction_arg
+| "injection"
+| "injection" destruction_arg
+| "einjection"
+| "einjection" destruction_arg
+| "injection" "as" simple_intropattern_list_opt
+| "injection" destruction_arg "as" simple_intropattern_list_opt
+| "einjection" "as" simple_intropattern_list_opt
+| "einjection" destruction_arg "as" simple_intropattern_list_opt
+| "simple" "injection"
+| "simple" "injection" destruction_arg
+| "dependent" "rewrite" orient term
+| "dependent" "rewrite" orient term "in" var
+| "cutrewrite" orient term
+| "cutrewrite" orient term "in" var
+| "decompose" "sum" term
+| "decompose" "record" term
+| "absurd" term
+| "contradiction" constr_with_bindings_opt
+| "autorewrite" "with" preident_list clause_dft_concl
+| "autorewrite" "with" preident_list clause_dft_concl "using" tactic
+| "autorewrite" "*" "with" preident_list clause_dft_concl
+| "autorewrite" "*" "with" preident_list clause_dft_concl "using" tactic
+| "rewrite" "*" orient uconstr "in" var "at" occurrences by_arg_tac
+| "rewrite" "*" orient uconstr "at" occurrences "in" var by_arg_tac
+| "rewrite" "*" orient uconstr "in" var by_arg_tac
+| "rewrite" "*" orient uconstr "at" occurrences by_arg_tac
+| "rewrite" "*" orient uconstr by_arg_tac
+| "refine" uconstr
+| "simple" "refine" uconstr
+| "notypeclasses" "refine" uconstr
+| "simple" "notypeclasses" "refine" uconstr
+| "solve_constraints"
+| "subst" var_list
+| "subst"
+| "simple" "subst"
+| "evar" test_lpar_id_colon "(" ident ":" lconstr ")"
+| "evar" term
+| "instantiate" "(" ident ":=" lglob ")"
+| "instantiate" "(" integer ":=" lglob ")" hloc
+| "instantiate"
+| "stepl" term "by" tactic
+| "stepl" term
+| "stepr" term "by" tactic
+| "stepr" term
+| "generalize_eqs" var
+| "dependent" "generalize_eqs" var
+| "generalize_eqs_vars" var
+| "dependent" "generalize_eqs_vars" var
+| "specialize_eqs" var
+| "hresolve_core" "(" ident ":=" term ")" "at" int_or_var "in" term
+| "hresolve_core" "(" ident ":=" term ")" "in" term
+| "hget_evar" int_or_var
+| "destauto"
+| "destauto" "in" var
+| "transparent_abstract" ltac_expr3
+| "transparent_abstract" ltac_expr3 "using" ident
+| "constr_eq" term term
+| "constr_eq_strict" term term
+| "constr_eq_nounivs" term term
+| "is_evar" term
+| "has_evar" term
+| "is_var" term
+| "is_fix" term
+| "is_cofix" term
+| "is_ind" term
+| "is_constructor" term
+| "is_proj" term
+| "is_const" term
+| "shelve"
+| "shelve_unifiable"
+| "unshelve" ltac_expr1
+| "give_up"
+| "cycle" int_or_var
+| "swap" int_or_var int_or_var
+| "revgoals"
+| "guard" test
+| "decompose" "[" term_list "]" term
+| "optimize_heap"
+| "start" "ltac" "profiling"
+| "stop" "ltac" "profiling"
+| "reset" "ltac" "profile"
+| "show" "ltac" "profile"
+| "show" "ltac" "profile" "cutoff" int
+| "show" "ltac" "profile" string
+| "restart_timer" string_opt
+| "finish_timing" string_opt
+| "finish_timing" "(" string ")" string_opt
+| "eassumption"
+| "eexact" term
+| "trivial" auto_using hintbases
+| "info_trivial" auto_using hintbases
+| "debug" "trivial" auto_using hintbases
+| "auto" int_or_var_opt auto_using hintbases
+| "info_auto" int_or_var_opt auto_using hintbases
+| "debug" "auto" int_or_var_opt auto_using hintbases
+| "prolog" "[" uconstr_list_opt "]" int_or_var
+| "eauto" int_or_var_opt int_or_var_opt auto_using hintbases
+| "new" "auto" int_or_var_opt auto_using hintbases
+| "debug" "eauto" int_or_var_opt int_or_var_opt auto_using hintbases
+| "info_eauto" int_or_var_opt int_or_var_opt auto_using hintbases
+| "dfs" "eauto" int_or_var_opt auto_using hintbases
+| "autounfold" hintbases clause_dft_concl
+| "autounfold_one" hintbases "in" var
+| "autounfold_one" hintbases
+| "unify" term term
+| "unify" term term "with" preident
+| "convert_concl_no_check" term
+| "typeclasses" "eauto" "bfs" int_or_var_opt "with" preident_list
+| "typeclasses" "eauto" int_or_var_opt "with" preident_list
+| "typeclasses" "eauto" int_or_var_opt
+| "head_of_constr" ident term
+| "not_evar" term
+| "is_ground" term
+| "autoapply" term "using" preident
+| "autoapply" term "with" preident
+| "progress_evars" tactic
+| "rewrite_strat" rewstrategy "in" var
+| "rewrite_strat" rewstrategy
+| "rewrite_db" preident "in" var
+| "rewrite_db" preident
+| "substitute" orient glob_constr_with_bindings
+| "setoid_rewrite" orient glob_constr_with_bindings
+| "setoid_rewrite" orient glob_constr_with_bindings "in" var
+| "setoid_rewrite" orient glob_constr_with_bindings "at" occurrences
+| "setoid_rewrite" orient glob_constr_with_bindings "at" occurrences "in" var
+| "setoid_rewrite" orient glob_constr_with_bindings "in" var "at" occurrences
+| "setoid_symmetry"
+| "setoid_symmetry" "in" var
+| "setoid_reflexivity"
+| "setoid_transitivity" term
+| "setoid_etransitivity"
+| "decide" "equality"
+| "compare" term term
+| "intros" intropattern_list_opt
+| "eintros" intropattern_list_opt
+| "apply" constr_with_bindings_arg_list_comma in_hyp_as
+| "eapply" constr_with_bindings_arg_list_comma in_hyp_as
+| "simple" "apply" constr_with_bindings_arg_list_comma in_hyp_as
+| "simple" "eapply" constr_with_bindings_arg_list_comma in_hyp_as
+| "elim" constr_with_bindings_arg eliminator_opt
+| "eelim" constr_with_bindings_arg eliminator_opt
+| "case" induction_clause_list
+| "ecase" induction_clause_list
+| "fix" ident natural "with" fixdecl_list
+| "cofix" ident "with" cofixdecl_list
+| "pose" bindings_with_parameters
+| "pose" term as_name
+| "epose" bindings_with_parameters
+| "epose" term as_name
+| "set" bindings_with_parameters clause_dft_concl
+| "set" term as_name clause_dft_concl
+| "eset" bindings_with_parameters clause_dft_concl
+| "eset" term as_name clause_dft_concl
+| "remember" term as_name eqn_ipat clause_dft_all
+| "eremember" term as_name eqn_ipat clause_dft_all
+| "assert" "(" ident ":=" lconstr ")"
+| "eassert" "(" ident ":=" lconstr ")"
+| "assert" test_lpar_id_colon "(" ident ":" lconstr ")" by_tactic
+| "eassert" test_lpar_id_colon "(" ident ":" lconstr ")" by_tactic
+| "enough" test_lpar_id_colon "(" ident ":" lconstr ")" by_tactic
+| "eenough" test_lpar_id_colon "(" ident ":" lconstr ")" by_tactic
+| "assert" term as_ipat by_tactic
+| "eassert" term as_ipat by_tactic
+| "pose" "proof" lconstr as_ipat
+| "epose" "proof" lconstr as_ipat
+| "enough" term as_ipat by_tactic
+| "eenough" term as_ipat by_tactic
+| "generalize" term
+| "generalize" term term_list
+| "generalize" term occs as_name pattern_occ_list_opt
+| "induction" induction_clause_list
+| "einduction" induction_clause_list
+| "destruct" induction_clause_list
+| "edestruct" induction_clause_list
+| "rewrite" oriented_rewriter_list_comma clause_dft_concl by_tactic
+| "erewrite" oriented_rewriter_list_comma clause_dft_concl by_tactic
+| "dependent" simple_alt quantified_hypothesis as_or_and_ipat with_opt2
+| "simple" "inversion" quantified_hypothesis as_or_and_ipat in_hyp_list
+| "inversion" quantified_hypothesis as_or_and_ipat in_hyp_list
+| "inversion_clear" quantified_hypothesis as_or_and_ipat in_hyp_list
+| "inversion" quantified_hypothesis "using" term in_hyp_list
+| "red" clause_dft_concl
+| "hnf" clause_dft_concl
+| "simpl" delta_flag ref_or_pattern_occ_opt clause_dft_concl
+| "cbv" strategy_flag clause_dft_concl
+| "cbn" strategy_flag clause_dft_concl
+| "lazy" strategy_flag clause_dft_concl
+| "compute" delta_flag clause_dft_concl
+| "vm_compute" ref_or_pattern_occ_opt clause_dft_concl
+| "native_compute" ref_or_pattern_occ_opt clause_dft_concl
+| "unfold" unfold_occ_list_comma clause_dft_concl
+| "fold" term_list clause_dft_concl
+| "pattern" pattern_occ_list_comma clause_dft_concl
+| "change" conversion clause_dft_concl
+| "change_no_check" conversion clause_dft_concl
+| "btauto"
+| "rtauto"
+| "congruence"
+| "congruence" integer
+| "congruence" "with" term_list
+| "congruence" integer "with" term_list
+| "f_equal"
+| "firstorder" tactic_opt firstorder_using
+| "firstorder" tactic_opt "with" preident_list
+| "firstorder" tactic_opt firstorder_using "with" preident_list
+| "gintuition" tactic_opt
+| "functional" "inversion" quantified_hypothesis reference_opt      (* funind plugin *)
+| "functional" "induction" term_list fun_ind_using with_names      (* funind plugin *)
+| "soft" "functional" "induction" term_list fun_ind_using with_names      (* funind plugin *)
+| "myred"      (* micromega plugin *)
+| "psatz_Z" int_or_var tactic      (* micromega plugin *)
+| "psatz_Z" tactic      (* micromega plugin *)
+| "xlia" tactic      (* micromega plugin *)
+| "xnlia" tactic      (* micromega plugin *)
+| "xnra" tactic      (* micromega plugin *)
+| "xnqa" tactic      (* micromega plugin *)
+| "sos_Z" tactic      (* micromega plugin *)
+| "sos_Q" tactic      (* micromega plugin *)
+| "sos_R" tactic      (* micromega plugin *)
+| "lra_Q" tactic      (* micromega plugin *)
+| "lra_R" tactic      (* micromega plugin *)
+| "psatz_R" int_or_var tactic      (* micromega plugin *)
+| "psatz_R" tactic      (* micromega plugin *)
+| "psatz_Q" int_or_var tactic      (* micromega plugin *)
+| "psatz_Q" tactic      (* micromega plugin *)
+| "nsatz_compute" term      (* nsatz plugin *)
+| "omega"      (* omega plugin *)
+| "omega" "with" ident_list      (* omega plugin *)
+| "omega" "with" "*"      (* omega plugin *)
+| "protect_fv" string "in" ident      (* setoid_ring plugin *)
+| "protect_fv" string      (* setoid_ring plugin *)
+| "ring_lookup" ltac_expr0 "[" term_list_opt "]" term_list      (* setoid_ring plugin *)
+| "field_lookup" tactic "[" term_list_opt "]" term_list      (* setoid_ring plugin *)
+| "YouShouldNotTypeThis" ssrintrosarg      (* ssr plugin *)
+| "by" ssrhintarg      (* ssr plugin *)
+| "YouShouldNotTypeThis" "do"      (* ssr plugin *)
+| "YouShouldNotTypeThis" ssrtclarg ssrseqarg      (* ssr plugin *)
+| "clear" natural      (* ssr plugin *)
+| "move" ssrmovearg ssrrpat      (* ssr plugin *)
+| "move" ssrmovearg ssrclauses      (* ssr plugin *)
+| "move" ssrrpat      (* ssr plugin *)
+| "move"      (* ssr plugin *)
+| "case" ssrcasearg ssrclauses      (* ssr plugin *)
+| "case"      (* ssr plugin *)
+| "elim" ssrarg ssrclauses      (* ssr plugin *)
+| "elim"      (* ssr plugin *)
+| "apply" ssrapplyarg      (* ssr plugin *)
+| "apply"      (* ssr plugin *)
+| "exact" ssrexactarg      (* ssr plugin *)
+| "exact"      (* ssr plugin *)
+| "exact" "<:" lconstr      (* ssr plugin *)
+| "congr" ssrcongrarg      (* ssr plugin *)
+| "ssrinstancesofruleL2R" ssrterm      (* ssr plugin *)
+| "ssrinstancesofruleR2L" ssrterm      (* ssr plugin *)
+| "rewrite" ssrrwargs ssrclauses      (* ssr plugin *)
+| "unlock" ssrunlockargs ssrclauses      (* ssr plugin *)
+| "pose" ssrfixfwd      (* ssr plugin *)
+| "pose" ssrcofixfwd      (* ssr plugin *)
+| "pose" ssrfwdid ssrposefwd      (* ssr plugin *)
+| "set" ssrfwdid ssrsetfwd ssrclauses      (* ssr plugin *)
+| "abstract" ssrdgens      (* ssr plugin *)
+| "have" ssrhavefwdwbinders      (* ssr plugin *)
+| "have" "suff" ssrhpats_nobs ssrhavefwd      (* ssr plugin *)
+| "have" "suffices" ssrhpats_nobs ssrhavefwd      (* ssr plugin *)
+| "suff" "have" ssrhpats_nobs ssrhavefwd      (* ssr plugin *)
+| "suffices" "have" ssrhpats_nobs ssrhavefwd      (* ssr plugin *)
+| "suff" ssrsufffwd      (* ssr plugin *)
+| "suffices" ssrsufffwd      (* ssr plugin *)
+| "wlog" ssrhpats_nobs ssrwlogfwd ssrhint      (* ssr plugin *)
+| "wlog" "suff" ssrhpats_nobs ssrwlogfwd ssrhint      (* ssr plugin *)
+| "wlog" "suffices" ssrhpats_nobs ssrwlogfwd ssrhint      (* ssr plugin *)
+| "without" "loss" ssrhpats_nobs ssrwlogfwd ssrhint      (* ssr plugin *)
+| "without" "loss" "suff" ssrhpats_nobs ssrwlogfwd ssrhint      (* ssr plugin *)
+| "without" "loss" "suffices" ssrhpats_nobs ssrwlogfwd ssrhint      (* ssr plugin *)
+| "gen" "have" ssrclear ssr_idcomma ssrhpats_nobs ssrwlogfwd ssrhint      (* ssr plugin *)
+| "generally" "have" ssrclear ssr_idcomma ssrhpats_nobs ssrwlogfwd ssrhint      (* ssr plugin *)
+| "under" ssrrwarg      (* ssr plugin *)
+| "under" ssrrwarg ssrintros_ne      (* ssr plugin *)
+| "under" ssrrwarg ssrintros_ne "do" ssrhint3arg      (* ssr plugin *)
+| "under" ssrrwarg "do" ssrhint3arg      (* ssr plugin *)
+| "ssrinstancesoftpat" cpattern      (* ssrmatching plugin *)
+]
+
+var_list: [
+| var_list var
+| var
+]
+
+var_list_opt: [
+| var_list_opt var
+| empty
+]
+
+constr_with_bindings_opt: [
+| constr_with_bindings
+| empty
+]
+
+int_or_var_opt: [
+| int_or_var
+| empty
+]
+
+uconstr_list_opt: [
+| uconstr_list_opt uconstr
+| empty
+]
+
+constr_with_bindings_arg_list_comma: [
+| constr_with_bindings_arg_list_comma "," constr_with_bindings_arg
+| constr_with_bindings_arg
+]
+
+fixdecl_list: [
+| fixdecl_list fixdecl
+| fixdecl
+]
+
+cofixdecl_list: [
+| cofixdecl_list cofixdecl
+| cofixdecl
+]
+
+pattern_occ_list_opt: [
+| pattern_occ_list_opt "," pattern_occ as_name
+| empty
+]
+
+oriented_rewriter_list_comma: [
+| oriented_rewriter_list_comma "," oriented_rewriter
+| oriented_rewriter
+]
+
+simple_alt: [
+| "simple" "inversion"
+| "inversion"
+| "inversion_clear"
+]
+
+with_opt2: [
+| "with" term
+| empty
+]
+
+tactic_opt: [
+| tactic
+| empty
+]
+
+reference_opt: [
+| reference
+| empty
+]
+
+bindings_list_comma: [
+| bindings_list_comma "," bindings
+| bindings
+]
+
+rename_list_comma: [
+| rename_list_comma "," rename
+| rename
+]
+
+orient_string: [
+| orient preident
+]
+
+comparison: [
+| "="
+| "<"
+| "<="
+| ">"
+| ">="
+]
+
+test: [
+| int_or_var comparison int_or_var
+]
+
+hintbases: [
+| "with" "*"
+| "with" preident_list
+| empty
+]
+
+preident_list: [
+| preident_list preident
+| preident
+]
+
+auto_using: [
+| "using" uconstr_list_comma
+| empty
+]
+
+uconstr_list_comma: [
+| uconstr_list_comma "," uconstr
+| uconstr
+]
+
+hints_path_atom: [
+| global_list
+| "_"
+]
+
+hints_path: [
+| "(" hints_path ")"
+| hints_path "*"
+| "emp"
+| "eps"
+| hints_path "|" hints_path
+| hints_path_atom
+| hints_path hints_path
+]
+
+opthints: [
+| ":" preident_list
+| empty
+]
+
+debug: [
+| "debug"
+| empty
+]
+
+eauto_search_strategy: [
+| "(bfs)"
+| "(dfs)"
+| empty
+]
+
+glob_constr_with_bindings: [
+| constr_with_bindings
+]
+
+rewstrategy: [
+| glob
+| "<-" term
+| "subterms" rewstrategy
+| "subterm" rewstrategy
+| "innermost" rewstrategy
+| "outermost" rewstrategy
+| "bottomup" rewstrategy
+| "topdown" rewstrategy
+| "id"
+| "fail"
+| "refl"
+| "progress" rewstrategy
+| "try" rewstrategy
+| "any" rewstrategy
+| "repeat" rewstrategy
+| rewstrategy ";" rewstrategy
+| "(" rewstrategy ")"
+| "choice" rewstrategy rewstrategy
+| "old_hints" preident
+| "hints" preident
+| "terms" term_list_opt
+| "eval" red_expr
+| "fold" term
+]
+
+term_list_opt: [
+| term_list_opt term
+| empty
+]
+
+int_or_var: [
+| integer
+| ident
+]
+
+nat_or_var: [
+| natural
+| ident
+]
+
+id_or_meta: [
+| ident
+]
+
+open_constr: [
+| term
+]
+
+uconstr: [
+| term
+]
+
+destruction_arg: [
+| natural
+| constr_with_bindings
+| constr_with_bindings_arg
+]
+
+constr_with_bindings_arg: [
+| ">" constr_with_bindings
+| constr_with_bindings
+]
+
+quantified_hypothesis: [
+| ident
+| natural
+]
+
+conversion: [
+| term
+| term "with" term
+| term "at" occs_nums "with" term
+]
+
+occs_nums: [
+| nat_or_var_list
+| "-" nat_or_var int_or_var_list_opt
+]
+
+nat_or_var_list: [
+| nat_or_var_list nat_or_var
+| nat_or_var
+]
+
+int_or_var_list_opt: [
+| int_or_var_list_opt int_or_var
+| empty
+]
+
+occs: [
+| "at" occs_nums
+| empty
+]
+
+pattern_occ: [
+| term occs
+]
+
+ref_or_pattern_occ: [
+| smart_global occs
+| term occs
+]
+
+unfold_occ: [
+| smart_global occs
+]
+
+intropattern_list_opt: [
+| intropattern_list_opt intropattern
+| empty
+]
+
+or_and_intropattern: [
+| "[" intropattern_or_list_or "]"
+| "(" simple_intropattern_list_comma_opt ")"
+| "(" simple_intropattern "&" simple_intropattern_list_ ")"
+]
+
+simple_intropattern_list_comma_opt: [
+| simple_intropattern_list_comma
+| empty
+]
+
+simple_intropattern_list_comma: [
+| simple_intropattern_list_comma "," simple_intropattern
+| simple_intropattern
+]
+
+simple_intropattern_list_: [
+| simple_intropattern_list_ "&" simple_intropattern
+| simple_intropattern
+]
+
+intropattern_or_list_or: [
+| intropattern_or_list_or "|" intropattern_list_opt
+| intropattern_list_opt
+]
+
+simple_intropattern_list_opt: [
+| simple_intropattern_list_opt simple_intropattern
+| empty
+]
+
+equality_intropattern: [
+| "->"
+| "<-"
+| "[=" intropattern_list_opt "]"
+]
+
+naming_intropattern: [
+| "?" ident
+| "?"
+| ident
+]
+
+intropattern: [
+| simple_intropattern
+| "*"
+| "**"
+]
+
+simple_intropattern: [
+| simple_intropattern_closed operconstr0_list_opt
+]
+
+operconstr0_list_opt: [
+| operconstr0_list_opt "%" operconstr0
+| empty
+]
+
+simple_intropattern_closed: [
+| or_and_intropattern
+| equality_intropattern
+| "_"
+| naming_intropattern
+]
+
+simple_binding: [
+| "(" ident ":=" lconstr ")"
+| "(" natural ":=" lconstr ")"
+]
+
+bindings: [
+| simple_binding_list
+| term_list
+]
+
+simple_binding_list: [
+| simple_binding_list simple_binding
+| simple_binding
+]
+
+term_list: [
+| term_list term
+| term
+]
+
+constr_with_bindings: [
+| term with_bindings
+]
+
+with_bindings: [
+| "with" bindings
+| empty
+]
+
+red_flags: [
+| "beta"
+| "iota"
+| "match"
+| "fix"
+| "cofix"
+| "zeta"
+| "delta" delta_flag
+]
+
+delta_flag: [
+| "-" "[" smart_global_list "]"
+| "[" smart_global_list "]"
+| empty
+]
+
+smart_global_list: [
+| smart_global_list smart_global
+| smart_global
+]
+
+strategy_flag: [
+| red_flags_list
+| delta_flag
+]
+
+red_flags_list: [
+| red_flags_list red_flags
+| red_flags
+]
+
+red_expr: [
+| "red"
+| "hnf"
+| "simpl" delta_flag ref_or_pattern_occ_opt
+| "cbv" strategy_flag
+| "cbn" strategy_flag
+| "lazy" strategy_flag
+| "compute" delta_flag
+| "vm_compute" ref_or_pattern_occ_opt
+| "native_compute" ref_or_pattern_occ_opt
+| "unfold" unfold_occ_list_comma
+| "fold" term_list
+| "pattern" pattern_occ_list_comma
+| IDENT
+]
+
+ref_or_pattern_occ_opt: [
+| ref_or_pattern_occ
+| empty
+]
+
+unfold_occ_list_comma: [
+| unfold_occ_list_comma "," unfold_occ
+| unfold_occ
+]
+
+pattern_occ_list_comma: [
+| pattern_occ_list_comma "," pattern_occ
+| pattern_occ
+]
+
+hypident: [
+| id_or_meta
+| "(" "type" "of" id_or_meta ")"
+| "(" "value" "of" id_or_meta ")"
+| "(" "type" "of" ident ")"      (* ssr plugin *)
+| "(" "value" "of" ident ")"      (* ssr plugin *)
+]
+
+hypident_occ: [
+| hypident occs
+]
+
+clause_dft_concl: [
+| "in" in_clause
+| occs
+| empty
+]
+
+clause_dft_all: [
+| "in" in_clause
+| empty
+]
+
+opt_clause: [
+| "in" in_clause
+| "at" occs_nums
+| empty
+]
+
+concl_occ: [
+| "*" occs
+| empty
+]
+
+in_hyp_list: [
+| "in" id_or_meta_list
+| empty
+]
+
+id_or_meta_list: [
+| id_or_meta_list id_or_meta
+| id_or_meta
+]
+
+in_hyp_as: [
+| "in" id_or_meta as_ipat
+| empty
+]
+
+simple_binder: [
+| name
+| "(" name_list ":" lconstr ")"
+]
+
+fixdecl: [
+| "(" ident simple_binder_list_opt fixannot ":" lconstr ")"
+]
+
+cofixdecl: [
+| "(" ident simple_binder_list_opt ":" lconstr ")"
+]
+
+bindings_with_parameters: [
+| "(" ident simple_binder_list_opt ":=" lconstr ")"
+]
+
+simple_binder_list_opt: [
+| simple_binder_list_opt simple_binder
+| empty
+]
+
+eliminator: [
+| "using" constr_with_bindings
+]
+
+as_ipat: [
+| "as" simple_intropattern
+| empty
+]
+
+or_and_intropattern_loc: [
+| or_and_intropattern
+| ident
+]
+
+as_or_and_ipat: [
+| "as" or_and_intropattern_loc
+| empty
+]
+
+eqn_ipat: [
+| "eqn" ":" naming_intropattern
+| "_eqn" ":" naming_intropattern
+| "_eqn"
+| empty
+]
+
+as_name: [
+| "as" ident
+| empty
+]
+
+by_tactic: [
+| "by" ltac_expr3
+| empty
+]
+
+rewriter: [
+| "!" constr_with_bindings_arg
+| qmark_alt constr_with_bindings_arg
+| natural "!" constr_with_bindings_arg
+| natural qmark_alt constr_with_bindings_arg
+| natural constr_with_bindings_arg
+| constr_with_bindings_arg
+]
+
+qmark_alt: [
+| "?"
+| "?"
+]
+
+oriented_rewriter: [
+| orient rewriter
+]
+
+induction_clause: [
+| destruction_arg as_or_and_ipat eqn_ipat opt_clause
+]
+
+induction_clause_list: [
+| induction_clause_list_comma eliminator_opt opt_clause
+]
+
+induction_clause_list_comma: [
+| induction_clause_list_comma "," induction_clause
+| induction_clause
+]
+
+eliminator_opt: [
+| eliminator
+| empty
+]
+
+ltac_expr: [
+| binder_tactic
+| ltac_expr4
+]
+
+binder_tactic: [
+| "fun" input_fun_list "=>" ltac_expr
+| "let" rec_opt let_clause_list "in" ltac_expr
+| "info" ltac_expr
+]
+
+input_fun_list: [
+| input_fun_list input_fun
+| input_fun
+]
+
+input_fun: [
+| "_"
+| ident
+]
+
+rec_opt: [
+| "rec"
+| empty
+]
+
+let_clause_list: [
+| let_clause_list "with" let_clause
+| let_clause
+]
+
+let_clause: [
+| ident ":=" ltac_expr
+| "_" ":=" ltac_expr
+| ident input_fun_list ":=" ltac_expr
+]
+
+ltac_expr4: [
+| ltac_expr3 ";" binder_tactic
+| ltac_expr3 ";" ltac_expr3
+| ltac_expr3 ";" "[" gt_opt tactic_then_gen "]"
+| ltac_expr3
+| ltac_expr ";" "first" ssr_first_else      (* ssr plugin *)
+| ltac_expr ";" "first" ssrseqarg      (* ssr plugin *)
+| ltac_expr ";" "last" ssrseqarg      (* ssr plugin *)
+]
+
+gt_opt: [
+| ">"
+| empty
+]
+
+tactic_then_gen: [
+| ltac_expr_opt "|" tactic_then_gen
+| ltac_expr_opt ".." or_opt ltac_expr_list2
+| ltac_expr
+| empty
+]
+
+ltac_expr_opt: [
+| ltac_expr
+| empty
+]
+
+ltac_expr_list_or2_opt: [
+| ltac_expr_list_or2
+| empty
+]
+
+ltac_expr_list_or2: [
+| ltac_expr_list_or2 "|" ltac_expr_opt
+| ltac_expr_opt
+]
+
+ltac_expr3: [
+| "try" ltac_expr3
+| "do" int_or_var ltac_expr3
+| "timeout" int_or_var ltac_expr3
+| "time" string_opt ltac_expr3
+| "repeat" ltac_expr3
+| "progress" ltac_expr3
+| "once" ltac_expr3
+| "exactly_once" ltac_expr3
+| "infoH" ltac_expr3
+| "abstract" ltac_expr2
+| "abstract" ltac_expr2 "using" ident
+| selector ltac_expr3
+| "do" ssrmmod ssrdotac ssrclauses      (* ssr plugin *)
+| "do" ssrortacarg ssrclauses      (* ssr plugin *)
+| "do" int_or_var ssrmmod ssrdotac ssrclauses      (* ssr plugin *)
+| "abstract" ssrdgens      (* ssr plugin *)
+| ltac_expr2
+]
+
+tactic_mode: [
+| toplevel_selector_opt query_command
+| toplevel_selector_opt "{"
+| toplevel_selector_opt ltac_info_opt tactic ltac_use_default
+| "par" ":" ltac_info_opt tactic ltac_use_default
+]
+
+toplevel_selector_opt: [
+| toplevel_selector
+| empty
+]
+
+toplevel_selector: [
+| selector_body ":"
+| "!" ":"
+| "all" ":"
+]
+
+selector: [
+| "only" selector_body ":"
+]
+
+selector_body: [
+| range_selector_list_comma
+| "[" ident "]"
+]
+
+range_selector_list_comma: [
+| range_selector_list_comma "," range_selector
+| range_selector
+]
+
+range_selector: [
+| natural "-" natural
+| natural
+]
+
+ltac_expr2: [
+| ltac_expr1 "+" binder_tactic
+| ltac_expr1 "+" ltac_expr2
+| "tryif" ltac_expr "then" ltac_expr "else" ltac_expr2
+| ltac_expr1 "||" binder_tactic
+| ltac_expr1 "||" ltac_expr2
+| ltac_expr1
+]
+
+ltac_expr1: [
+| match_key reverse_opt "goal" "with" match_context_list "end"
+| match_key ltac_expr "with" match_list "end"
+| "first" "[" ltac_expr_list_or_opt "]"
+| "solve" "[" ltac_expr_list_or_opt "]"
+| "idtac" message_token_list_opt
+| failkw int_or_var_opt message_token_list_opt
+| simple_tactic
+| tactic_arg
+| reference tactic_arg_compat_list_opt
+| ltac_expr ssrintros_ne      (* ssr plugin *)
+| ltac_expr0
+]
+
+match_key: [
+| "match"
+| "lazymatch"
+| "multimatch"
+]
+
+reverse_opt: [
+| "reverse"
+| empty
+]
+
+ltac_expr_list_or_opt: [
+| ltac_expr_list_or
+| empty
+]
+
+ltac_expr_list_or: [
+| ltac_expr_list_or "|" ltac_expr
+| ltac_expr
+]
+
+match_context_list: [
+| or_opt match_context_rule_list_or
+]
+
+match_context_rule_list_or: [
+| match_context_rule_list_or "|" match_context_rule
+| match_context_rule
+]
+
+or_opt: [
+| "|"
+| empty
+]
+
+eqn_list_or_opt: [
+| eqn_list_or
+| empty
+]
+
+eqn_list_or: [
+| eqn_list_or "|" eqn
+| eqn
+]
+
+match_context_rule: [
+| match_hyps_list_comma_opt "|-" match_pattern "=>" ltac_expr
+| "[" match_hyps_list_comma_opt "|-" match_pattern "]" "=>" ltac_expr
+| "_" "=>" ltac_expr
+]
+
+match_hyps_list_comma_opt: [
+| match_hyps_list_comma
+| empty
+]
+
+match_hyps_list_comma: [
+| match_hyps_list_comma "," match_hyps
+| match_hyps
+]
+
+match_hyps: [
+| name ":" match_pattern
+| name ":=" match_pattern_opt match_pattern
+]
+
+match_pattern: [
+| "context" ident_opt "[" lconstr_pattern "]"
+| lconstr_pattern
+]
+
+ident_opt: [
+| ident
+| empty
+]
+
+lconstr_pattern: [
+| lconstr
+]
+
+match_pattern_opt: [
+| "[" match_pattern "]" ":"
+| empty
+]
+
+match_list: [
+| or_opt match_rule_list_or
+]
+
+match_rule_list_or: [
+| match_rule_list_or "|" match_rule
+| match_rule
+]
+
+match_rule: [
+| match_pattern "=>" ltac_expr
+| "_" "=>" ltac_expr
+]
+
+message_token_list_opt: [
+| message_token_list_opt message_token
+| empty
+]
+
+message_token: [
+| ident
+| STRING
+| integer
+]
+
+failkw: [
+| "fail"
+| "gfail"
+]
+
+tactic_arg: [
+| "eval" red_expr "in" term
+| "context" ident "[" lconstr "]"
+| "type" "of" term
+| "fresh" fresh_id_list_opt
+| "type_term" uconstr
+| "numgoals"
+]
+
+fresh_id_list_opt: [
+| fresh_id_list_opt fresh_id
+| empty
+]
+
+fresh_id: [
+| STRING
+| qualid
+]
+
+tactic_arg_compat_list_opt: [
+| tactic_arg_compat_list_opt tactic_arg_compat
+| empty
+]
+
+tactic_arg_compat: [
+| tactic_arg
+| term
+| "()"
+]
+
+ltac_expr0: [
+| "(" ltac_expr ")"
+| "[" ">" tactic_then_gen "]"
+| tactic_atom
+| ssrparentacarg      (* ssr plugin *)
+]
+
+tactic_atom: [
+| integer
+| reference
+| "()"
+]
+
+constr_may_eval: [
+| "eval" red_expr "in" term
+| "context" ident "[" lconstr "]"
+| "type" "of" term
+| term
+]
+
+ltac_def_kind: [
+| ":="
+| "::="
+]
+
+tacdef_body: [
+| global input_fun_list ltac_def_kind ltac_expr
+| global ltac_def_kind ltac_expr
+]
+
+tactic: [
+| ltac_expr
+]
+
+ltac_info_opt: [
+| ltac_info
+| empty
+]
+
+ltac_info: [
+| "Info" natural
+]
+
+ltac_use_default: [
+| "."
+| "..."
+]
+
+ltac_tactic_level: [
+| "(" "at" "level" natural ")"
+]
+
+ltac_production_sep: [
+| "," string
+]
+
+ltac_production_item: [
+| string
+| ident "(" ident ltac_production_sep_opt ")"
+| ident
+]
+
+ltac_production_sep_opt: [
+| ltac_production_sep
+| empty
+]
+
+ltac_tacdef_body: [
+| tacdef_body
+]
+
+firstorder_using: [
+| "using" reference
+| "using" reference "," reference_list_comma
+| "using" reference reference reference_list_opt
+| empty
+]
+
+reference_list_comma: [
+| reference_list_comma "," reference
+| reference
+]
+
+numnotoption: [
+| empty
+| "(" "warning" "after" bigint ")"
+| "(" "abstract" "after" bigint ")"
+]
+
+mlname: [
+| preident      (* extraction plugin *)
+| string      (* extraction plugin *)
+]
+
+int_or_id: [
+| preident      (* extraction plugin *)
+| integer      (* extraction plugin *)
+]
+
+language: [
+| "Ocaml"      (* extraction plugin *)
+| "OCaml"      (* extraction plugin *)
+| "Haskell"      (* extraction plugin *)
+| "Scheme"      (* extraction plugin *)
+| "JSON"      (* extraction plugin *)
+]
+
+fun_ind_using: [
+| "using" constr_with_bindings      (* funind plugin *)
+| empty      (* funind plugin *)
+]
+
+with_names: [
+| "as" simple_intropattern      (* funind plugin *)
+| empty      (* funind plugin *)
+]
+
+constr_comma_sequence': [
+| term "," constr_comma_sequence'      (* funind plugin *)
+| term      (* funind plugin *)
+]
+
+auto_using': [
+| "using" constr_comma_sequence'      (* funind plugin *)
+| empty      (* funind plugin *)
+]
+
+function_rec_definition_loc: [
+| rec_definition      (* funind plugin *)
+]
+
+fun_scheme_arg: [
+| ident ":=" "Induction" "for" reference "Sort" sort_family      (* funind plugin *)
+]
+
+ring_mod: [
+| "decidable" term      (* setoid_ring plugin *)
+| "abstract"      (* setoid_ring plugin *)
+| "morphism" term      (* setoid_ring plugin *)
+| "constants" "[" tactic "]"      (* setoid_ring plugin *)
+| "closed" "[" global_list "]"      (* setoid_ring plugin *)
+| "preprocess" "[" tactic "]"      (* setoid_ring plugin *)
+| "postprocess" "[" tactic "]"      (* setoid_ring plugin *)
+| "setoid" term term      (* setoid_ring plugin *)
+| "sign" term      (* setoid_ring plugin *)
+| "power" term "[" global_list "]"      (* setoid_ring plugin *)
+| "power_tac" term "[" tactic "]"      (* setoid_ring plugin *)
+| "div" term      (* setoid_ring plugin *)
+]
+
+ring_mods: [
+| "(" ring_mod_list_comma ")"      (* setoid_ring plugin *)
+]
+
+ring_mod_list_comma: [
+| ring_mod_list_comma "," ring_mod
+| ring_mod
+]
+
+field_mod: [
+| ring_mod      (* setoid_ring plugin *)
+| "completeness" term      (* setoid_ring plugin *)
+]
+
+field_mods: [
+| "(" field_mod_list_comma ")"      (* setoid_ring plugin *)
+]
+
+field_mod_list_comma: [
+| field_mod_list_comma "," field_mod
+| field_mod
+]
+
+ssrtacarg: [
+| ltac_expr      (* ssr plugin *)
+]
+
+ssrtac3arg: [
+| ltac_expr3      (* ssr plugin *)
+]
+
+ssrtclarg: [
+| ssrtacarg      (* ssr plugin *)
+]
+
+ssrhyp: [
+| ident      (* ssr plugin *)
+]
+
+ssrhoi_hyp: [
+| ident      (* ssr plugin *)
+]
+
+ssrhoi_id: [
+| ident      (* ssr plugin *)
+]
+
+ssrsimpl_ne: [
+| "//="      (* ssr plugin *)
+| "/="      (* ssr plugin *)
+| "/" natural "/" natural "="      (* ssr plugin *)
+| "/" natural "/"      (* ssr plugin *)
+| "/" natural "="      (* ssr plugin *)
+| "/" natural "/="      (* ssr plugin *)
+| "/" natural "/" "="      (* ssr plugin *)
+| "//" natural "="      (* ssr plugin *)
+| "//"      (* ssr plugin *)
+]
+
+ssrclear_ne: [
+| "{" ssrhyp_list "}"      (* ssr plugin *)
+]
+
+ssrclear: [
+| ssrclear_ne      (* ssr plugin *)
+| empty      (* ssr plugin *)
+]
+
+ssrindex: [
+| int_or_var      (* ssr plugin *)
+]
+
+ssrocc: [
+| natural natural_list_opt      (* ssr plugin *)
+| "-" natural_list_opt      (* ssr plugin *)
+| "+" natural_list_opt      (* ssr plugin *)
+]
+
+natural_list_opt: [
+| natural_list_opt natural
+| empty
+]
+
+ssrmmod: [
+| "!"      (* ssr plugin *)
+| "?"      (* ssr plugin *)
+| "?"      (* ssr plugin *)
+]
+
+ssrmult_ne: [
+| natural ssrmmod      (* ssr plugin *)
+| ssrmmod      (* ssr plugin *)
+]
+
+ssrmult: [
+| ssrmult_ne      (* ssr plugin *)
+| empty      (* ssr plugin *)
+]
+
+ssrdocc: [
+| "{" ssrocc "}"      (* ssr plugin *)
+| "{" ssrhyp_list_opt "}"      (* ssr plugin *)
+]
+
+ssrhyp_list_opt: [
+| ssrhyp_list_opt ssrhyp
+| empty
+]
+
+ssrterm: [
+| "YouShouldNotTypeThis" term      (* ssr plugin *)
+| term      (* ssr plugin *)
+]
+
+ast_closure_term: [
+| term      (* ssr plugin *)
+]
+
+ast_closure_lterm: [
+| lconstr      (* ssr plugin *)
+]
+
+ssrbwdview: [
+| "YouShouldNotTypeThis"      (* ssr plugin *)
+| "/" term      (* ssr plugin *)
+| "/" term ssrbwdview      (* ssr plugin *)
+]
+
+ssrfwdview: [
+| "YouShouldNotTypeThis"      (* ssr plugin *)
+| "/" ast_closure_term      (* ssr plugin *)
+| "/" ast_closure_term ssrfwdview      (* ssr plugin *)
+]
+
+ident_no_do: [
+| "YouShouldNotTypeThis" ident      (* ssr plugin *)
+| IDENT      (* ssr plugin *)
+]
+
+ssripat: [
+| "_"      (* ssr plugin *)
+| "*"      (* ssr plugin *)
+| ">"      (* ssr plugin *)
+| ident_no_do      (* ssr plugin *)
+| "?"      (* ssr plugin *)
+| "+"      (* ssr plugin *)
+| "++"      (* ssr plugin *)
+| ssrsimpl_ne      (* ssr plugin *)
+| ssrdocc "->"      (* ssr plugin *)
+| ssrdocc "<-"      (* ssr plugin *)
+| ssrdocc      (* ssr plugin *)
+| "->"      (* ssr plugin *)
+| "<-"      (* ssr plugin *)
+| "-"      (* ssr plugin *)
+| "-/" "="      (* ssr plugin *)
+| "-/="      (* ssr plugin *)
+| "-/" "/"      (* ssr plugin *)
+| "-//"      (* ssr plugin *)
+| "-/" integer "/"      (* ssr plugin *)
+| "-/" "/="      (* ssr plugin *)
+| "-//" "="      (* ssr plugin *)
+| "-//="      (* ssr plugin *)
+| "-/" integer "/="      (* ssr plugin *)
+| "-/" integer "/" integer "="      (* ssr plugin *)
+| ssrfwdview      (* ssr plugin *)
+| "[" ":" ident_list_opt "]"      (* ssr plugin *)
+| "[:" ident_list_opt "]"      (* ssr plugin *)
+| ssrcpat      (* ssr plugin *)
+]
+
+ident_list_opt: [
+| ident_list_opt ident
+| empty
+]
+
+ssripats: [
+| ssripat ssripats      (* ssr plugin *)
+| empty      (* ssr plugin *)
+]
+
+ssriorpat: [
+| ssripats "|" ssriorpat      (* ssr plugin *)
+| ssripats "|-" ">" ssriorpat      (* ssr plugin *)
+| ssripats "|-" ssriorpat      (* ssr plugin *)
+| ssripats "|->" ssriorpat      (* ssr plugin *)
+| ssripats "||" ssriorpat      (* ssr plugin *)
+| ssripats "|||" ssriorpat      (* ssr plugin *)
+| ssripats "||||" ssriorpat      (* ssr plugin *)
+| ssripats      (* ssr plugin *)
+]
+
+ssrcpat: [
+| "YouShouldNotTypeThis" ssriorpat      (* ssr plugin *)
+| "[" hat "]"      (* ssr plugin *)
+| "[" ssriorpat "]"      (* ssr plugin *)
+| "[=" ssriorpat "]"      (* ssr plugin *)
+]
+
+hat: [
+| "^" ident      (* ssr plugin *)
+| "^" "~" ident      (* ssr plugin *)
+| "^" "~" natural      (* ssr plugin *)
+| "^~" ident      (* ssr plugin *)
+| "^~" natural      (* ssr plugin *)
+]
+
+ssripats_ne: [
+| ssripat ssripats      (* ssr plugin *)
+]
+
+ssrhpats: [
+| ssripats      (* ssr plugin *)
+]
+
+ssrhpats_wtransp: [
+| ssripats      (* ssr plugin *)
+| ssripats "@" ssripats      (* ssr plugin *)
+]
+
+ssrhpats_nobs: [
+| ssripats      (* ssr plugin *)
+]
+
+ssrrpat: [
+| "->"      (* ssr plugin *)
+| "<-"      (* ssr plugin *)
+]
+
+ssrintros_ne: [
+| "=>" ssripats_ne      (* ssr plugin *)
+]
+
+ssrintros: [
+| ssrintros_ne      (* ssr plugin *)
+| empty      (* ssr plugin *)
+]
+
+ssrintrosarg: [
+| "YouShouldNotTypeThis" ssrtacarg ssrintros_ne      (* ssr plugin *)
+]
+
+ssrfwdid: [
+| ident      (* ssr plugin *)
+]
+
+ssrortacs: [
+| ssrtacarg "|" ssrortacs      (* ssr plugin *)
+| ssrtacarg "|"      (* ssr plugin *)
+| ssrtacarg      (* ssr plugin *)
+| "|" ssrortacs      (* ssr plugin *)
+| "|"      (* ssr plugin *)
+]
+
+ssrhintarg: [
+| "[" "]"      (* ssr plugin *)
+| "[" ssrortacs "]"      (* ssr plugin *)
+| ssrtacarg      (* ssr plugin *)
+]
+
+ssrhint3arg: [
+| "[" "]"      (* ssr plugin *)
+| "[" ssrortacs "]"      (* ssr plugin *)
+| ssrtac3arg      (* ssr plugin *)
+]
+
+ssrortacarg: [
+| "[" ssrortacs "]"      (* ssr plugin *)
+]
+
+ssrhint: [
+| empty      (* ssr plugin *)
+| "by" ssrhintarg      (* ssr plugin *)
+]
+
+ssrwgen: [
+| ssrclear_ne      (* ssr plugin *)
+| ssrhoi_hyp      (* ssr plugin *)
+| "@" ssrhoi_hyp      (* ssr plugin *)
+| "(" ssrhoi_id ":=" lcpattern ")"      (* ssr plugin *)
+| "(" ssrhoi_id ")"      (* ssr plugin *)
+| "(@" ssrhoi_id ":=" lcpattern ")"      (* ssr plugin *)
+| "(" "@" ssrhoi_id ":=" lcpattern ")"      (* ssr plugin *)
+]
+
+ssrclausehyps: [
+| ssrwgen "," ssrclausehyps      (* ssr plugin *)
+| ssrwgen ssrclausehyps      (* ssr plugin *)
+| ssrwgen      (* ssr plugin *)
+]
+
+ssrclauses: [
+| "in" ssrclausehyps "|-" "*"      (* ssr plugin *)
+| "in" ssrclausehyps "|-"      (* ssr plugin *)
+| "in" ssrclausehyps "*"      (* ssr plugin *)
+| "in" ssrclausehyps      (* ssr plugin *)
+| "in" "|-" "*"      (* ssr plugin *)
+| "in" "*"      (* ssr plugin *)
+| "in" "*" "|-"      (* ssr plugin *)
+| empty      (* ssr plugin *)
+]
+
+ssrfwd: [
+| ":=" ast_closure_lterm      (* ssr plugin *)
+| ":" ast_closure_lterm ":=" ast_closure_lterm      (* ssr plugin *)
+]
+
+ssrbvar: [
+| ident      (* ssr plugin *)
+| "_"      (* ssr plugin *)
+]
+
+ssrbinder: [
+| ssrbvar      (* ssr plugin *)
+| "(" ssrbvar ")"      (* ssr plugin *)
+| "(" ssrbvar ":" lconstr ")"      (* ssr plugin *)
+| "(" ssrbvar ssrbvar_list ":" lconstr ")"      (* ssr plugin *)
+| "(" ssrbvar ":" lconstr ":=" lconstr ")"      (* ssr plugin *)
+| "(" ssrbvar ":=" lconstr ")"      (* ssr plugin *)
+| of_alt operconstr99      (* ssr plugin *)
+]
+
+ssrbvar_list: [
+| ssrbvar_list ssrbvar
+| ssrbvar
+]
+
+ssrstruct: [
+| "{" "struct" ident "}"      (* ssr plugin *)
+| empty      (* ssr plugin *)
+]
+
+ssrposefwd: [
+| ssrbinder_list_opt ssrfwd      (* ssr plugin *)
+]
+
+ssrfixfwd: [
+| "fix" ssrbvar ssrbinder_list_opt ssrstruct ssrfwd      (* ssr plugin *)
+]
+
+ssrcofixfwd: [
+| "cofix" ssrbvar ssrbinder_list_opt ssrfwd      (* ssr plugin *)
+]
+
+ssrbinder_list_opt: [
+| ssrbinder_list_opt ssrbinder
+| empty
+]
+
+ssrsetfwd: [
+| ":" ast_closure_lterm ":=" "{" ssrocc "}" cpattern      (* ssr plugin *)
+| ":" ast_closure_lterm ":=" lcpattern      (* ssr plugin *)
+| ":=" "{" ssrocc "}" cpattern      (* ssr plugin *)
+| ":=" lcpattern      (* ssr plugin *)
+]
+
+ssrhavefwd: [
+| ":" ast_closure_lterm ssrhint      (* ssr plugin *)
+| ":" ast_closure_lterm ":=" ast_closure_lterm      (* ssr plugin *)
+| ":" ast_closure_lterm ":="      (* ssr plugin *)
+| ":=" ast_closure_lterm      (* ssr plugin *)
+]
+
+ssrhavefwdwbinders: [
+| ssrhpats_wtransp ssrbinder_list_opt ssrhavefwd      (* ssr plugin *)
+]
+
+ssrseqarg: [
+| ssrswap      (* ssr plugin *)
+| ssrseqidx ssrortacarg ssrorelse_opt      (* ssr plugin *)
+| ssrseqidx ssrswap      (* ssr plugin *)
+| ltac_expr3      (* ssr plugin *)
+]
+
+ssrorelse_opt: [
+| ssrorelse
+| empty
+]
+
+ssrseqidx: [
+| ident      (* ssr plugin *)
+| natural      (* ssr plugin *)
+]
+
+ssrswap: [
+| "first"      (* ssr plugin *)
+| "last"      (* ssr plugin *)
+]
+
+ssrorelse: [
+| "||" ltac_expr2      (* ssr plugin *)
+]
+
+ident: [
+| IDENT
+]
+
+ssrparentacarg: [
+| "(" ltac_expr ")"      (* ssr plugin *)
+]
+
+ssrdotac: [
+| ltac_expr3      (* ssr plugin *)
+| ssrortacarg      (* ssr plugin *)
+]
+
+ssr_first: [
+| ssr_first ssrintros_ne      (* ssr plugin *)
+| "[" ltac_expr_list_or_opt "]"      (* ssr plugin *)
+]
+
+ssr_first_else: [
+| ssr_first ssrorelse      (* ssr plugin *)
+| ssr_first      (* ssr plugin *)
+]
+
+ssrgen: [
+| ssrdocc cpattern      (* ssr plugin *)
+| cpattern      (* ssr plugin *)
+]
+
+ssrdgens_tl: [
+| "{" ssrhyp_list "}" cpattern ssrdgens_tl      (* ssr plugin *)
+| "{" ssrhyp_list "}"      (* ssr plugin *)
+| "{" ssrocc "}" cpattern ssrdgens_tl      (* ssr plugin *)
+| "/" ssrdgens_tl      (* ssr plugin *)
+| cpattern ssrdgens_tl      (* ssr plugin *)
+| empty      (* ssr plugin *)
+]
+
+ssrdgens: [
+| ":" ssrgen ssrdgens_tl      (* ssr plugin *)
+]
+
+ssreqid: [
+| ssreqpat      (* ssr plugin *)
+| empty      (* ssr plugin *)
+]
+
+ssreqpat: [
+| ident      (* ssr plugin *)
+| "_"      (* ssr plugin *)
+| "?"      (* ssr plugin *)
+| "+"      (* ssr plugin *)
+| ssrdocc "->"      (* ssr plugin *)
+| ssrdocc "<-"      (* ssr plugin *)
+| "->"      (* ssr plugin *)
+| "<-"      (* ssr plugin *)
+]
+
+ssrarg: [
+| ssrfwdview ssreqid ssrdgens ssrintros      (* ssr plugin *)
+| ssrfwdview ssrclear ssrintros      (* ssr plugin *)
+| ssreqid ssrdgens ssrintros      (* ssr plugin *)
+| ssrclear_ne ssrintros      (* ssr plugin *)
+| ssrintros_ne      (* ssr plugin *)
+]
+
+ssrmovearg: [
+| ssrarg      (* ssr plugin *)
+]
+
+ssrcasearg: [
+| ssrarg      (* ssr plugin *)
+]
+
+ssragen: [
+| "{" ssrhyp_list "}" ssrterm      (* ssr plugin *)
+| ssrterm      (* ssr plugin *)
+]
+
+ssrhyp_list: [
+| ssrhyp_list ssrhyp
+| ssrhyp
+]
+
+ssragens: [
+| "{" ssrhyp_list "}" ssrterm ssragens      (* ssr plugin *)
+| "{" ssrhyp_list "}"      (* ssr plugin *)
+| ssrterm ssragens      (* ssr plugin *)
+| empty      (* ssr plugin *)
+]
+
+ssrapplyarg: [
+| ":" ssragen ssragens ssrintros      (* ssr plugin *)
+| ssrclear_ne ssrintros      (* ssr plugin *)
+| ssrintros_ne      (* ssr plugin *)
+| ssrbwdview ":" ssragen ssragens ssrintros      (* ssr plugin *)
+| ssrbwdview ssrclear ssrintros      (* ssr plugin *)
+]
+
+ssrexactarg: [
+| ":" ssragen ssragens      (* ssr plugin *)
+| ssrbwdview ssrclear      (* ssr plugin *)
+| ssrclear_ne      (* ssr plugin *)
+]
+
+ssrcongrarg: [
+| natural term ssrdgens      (* ssr plugin *)
+| natural term      (* ssr plugin *)
+| term ssrdgens      (* ssr plugin *)
+| term      (* ssr plugin *)
+]
+
+ssrrwocc: [
+| "{" ssrhyp_list_opt "}"      (* ssr plugin *)
+| "{" ssrocc "}"      (* ssr plugin *)
+| empty      (* ssr plugin *)
+]
+
+ssrrule_ne: [
+| ssrterm_alt      (* ssr plugin *)
+| ssrsimpl_ne      (* ssr plugin *)
+]
+
+ssrterm_alt: [
+| "/" ssrterm
+| ssrterm
+| ssrsimpl_ne
+]
+
+ssrrule: [
+| ssrrule_ne      (* ssr plugin *)
+| empty      (* ssr plugin *)
+]
+
+ssrpattern_squarep: [
+| "[" rpattern "]"      (* ssr plugin *)
+| empty      (* ssr plugin *)
+]
+
+ssrpattern_ne_squarep: [
+| "[" rpattern "]"      (* ssr plugin *)
+]
+
+ssrrwarg: [
+| "-" ssrmult ssrrwocc ssrpattern_squarep ssrrule_ne      (* ssr plugin *)
+| "-/" ssrterm      (* ssr plugin *)
+| ssrmult_ne ssrrwocc ssrpattern_squarep ssrrule_ne      (* ssr plugin *)
+| "{" ssrhyp_list "}" ssrpattern_ne_squarep ssrrule_ne      (* ssr plugin *)
+| "{" ssrhyp_list "}" ssrrule      (* ssr plugin *)
+| "{" ssrocc "}" ssrpattern_squarep ssrrule_ne      (* ssr plugin *)
+| "{" "}" ssrpattern_squarep ssrrule_ne      (* ssr plugin *)
+| ssrpattern_ne_squarep ssrrule_ne      (* ssr plugin *)
+| ssrrule_ne      (* ssr plugin *)
+]
+
+ssrrwargs: [
+| ssrrwarg_list      (* ssr plugin *)
+]
+
+ssrrwarg_list: [
+| ssrrwarg_list ssrrwarg
+| ssrrwarg
+]
+
+ssrunlockarg: [
+| "{" ssrocc "}" ssrterm      (* ssr plugin *)
+| ssrterm      (* ssr plugin *)
+]
+
+ssrunlockargs: [
+| ssrunlockarg_list_opt      (* ssr plugin *)
+]
+
+ssrunlockarg_list_opt: [
+| ssrunlockarg_list_opt ssrunlockarg
+| empty
+]
+
+ssrsufffwd: [
+| ssrhpats ssrbinder_list_opt ":" ast_closure_lterm ssrhint      (* ssr plugin *)
+]
+
+ssrwlogfwd: [
+| ":" ssrwgen_list_opt "/" ast_closure_lterm      (* ssr plugin *)
+]
+
+ssrwgen_list_opt: [
+| ssrwgen_list_opt ssrwgen
+| empty
+]
+
+ssr_idcomma: [
+| empty      (* ssr plugin *)
+| IDENT_alt ","      (* ssr plugin *)
+]
+
+IDENT_alt: [
+| IDENT
+| "_"
+]
+
+ssr_rtype: [
+| "return" operconstr100      (* ssr plugin *)
+]
+
+ssr_mpat: [
+| pattern200      (* ssr plugin *)
+]
+
+ssr_dpat: [
+| ssr_mpat "in" pattern200 ssr_rtype      (* ssr plugin *)
+| ssr_mpat ssr_rtype      (* ssr plugin *)
+| ssr_mpat      (* ssr plugin *)
+]
+
+ssr_dthen: [
+| ssr_dpat "then" lconstr      (* ssr plugin *)
+]
+
+ssr_elsepat: [
+| "else"      (* ssr plugin *)
+]
+
+ssr_else: [
+| ssr_elsepat lconstr      (* ssr plugin *)
+]
+
+ssr_search_item: [
+| string      (* ssr plugin *)
+| string "%" preident      (* ssr plugin *)
+| constr_pattern      (* ssr plugin *)
+]
+
+ssr_search_arg: [
+| "-" ssr_search_item ssr_search_arg      (* ssr plugin *)
+| ssr_search_item ssr_search_arg      (* ssr plugin *)
+| empty      (* ssr plugin *)
+]
+
+ssr_modlocs: [
+| empty      (* ssr plugin *)
+| "in" modloc_list      (* ssr plugin *)
+]
+
+modloc_list: [
+| modloc_list modloc
+| modloc
+]
+
+modloc: [
+| "-" global      (* ssr plugin *)
+| global      (* ssr plugin *)
+]
+
+ssrhintref: [
+| term      (* ssr plugin *)
+| term "|" natural      (* ssr plugin *)
+]
+
+ssrviewpos: [
+| "for" "move" "/"      (* ssr plugin *)
+| "for" "apply" "/"      (* ssr plugin *)
+| "for" "apply" "/" "/"      (* ssr plugin *)
+| "for" "apply" "//"      (* ssr plugin *)
+| empty      (* ssr plugin *)
+]
+
+ssrviewposspc: [
+| ssrviewpos      (* ssr plugin *)
+]
+
+rpattern: [
+| lconstr      (* ssrmatching plugin *)
+| "in" lconstr      (* ssrmatching plugin *)
+| lconstr "in" lconstr      (* ssrmatching plugin *)
+| "in" lconstr "in" lconstr      (* ssrmatching plugin *)
+| lconstr "in" lconstr "in" lconstr      (* ssrmatching plugin *)
+| lconstr "as" lconstr "in" lconstr      (* ssrmatching plugin *)
+]
+
+cpattern: [
+| "Qed" term      (* ssrmatching plugin *)
+| term      (* ssrmatching plugin *)
+]
+
+lcpattern: [
+| "Qed" lconstr      (* ssrmatching plugin *)
+| lconstr      (* ssrmatching plugin *)
+]
+
+ssrpatternarg: [
+| rpattern      (* ssrmatching plugin *)
+]
+
+empty: [
+|
+]
+
+lpar_id_coloneq: [
+| "(" IDENT; ":="
+]
+
+name_colon: [
+| IDENT; ":"
+| "_" ":"
+]
+
+int: [
+| integer
+]
+
+command_entry: [
+| noedit_mode
+]
+
diff --git a/doc/tools/docgram/prodn.edit_mlg b/doc/tools/docgram/prodn.edit_mlg
new file mode 100644
index 0000000000..a28d07636a
--- /dev/null
+++ b/doc/tools/docgram/prodn.edit_mlg
@@ -0,0 +1,14 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2019       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+(* Defines additional productions and edits for use in documentation.  Not compiled into Coq *)
+(* Contents used to generate prodn in doc *)
+
+DOC_GRAMMAR
diff --git a/doc/tools/docgram/productionlist.edit_mlg b/doc/tools/docgram/productionlist.edit_mlg
new file mode 100644
index 0000000000..84acd07075
--- /dev/null
+++ b/doc/tools/docgram/productionlist.edit_mlg
@@ -0,0 +1,25 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2019       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+(* Defines additional productions and edits for use in documentation.  Not compiled into Coq *)
+(* Contents used to generate productionlists in doc *)
+
+DOC_GRAMMAR
+
+EXPAND: [ | ]
+
+(* ugh todo: try to handle before expansion *)
+tactic_then_gen : [
+| REPLACE ltac_expr_opt ".." ltac_expr_opt2
+| WITH ltac_expr_opt ".." or_opt ltac_expr_list2
+]
+
+ltac_expr_opt2 : [ | DELETENT ]
+ltac_expr_list2_opt : [ | DELETENT ]