Update grammar in the Terms section of Gallina chapter

Update doc_grammar tool

The grammar in the doc is generated semi-automatically with doc_grammar:
- the grammar is automatically extracted from the mlg files
- developer-prepared editing scripts *.mlg_edit modify the extracted
  grammar for clarity, simplicity and ordering of productions
- chunks of the resulting grammar are automatically inserted into the
  rsts using instructions embedded in the rsts

Running doc_grammar is currently a manual step.

The grammar updates in the rst files have been manually reviewed.

7 files changed, 2537 insertions, 3495 deletions

diff --git a/doc/tools/docgram/README.md b/doc/tools/docgram/README.md
index 98fdc38ca7..a0a1809133 100644
--- a/doc/tools/docgram/README.md
+++ b/doc/tools/docgram/README.md
@@ -186,6 +186,9 @@ that appear in the specified production:
 | WITH <newprod>
 ```
 
+* `PRINT` <nonterminal> - prints the nonterminal definition at that point in
+  applying the edits.  Most useful when the edits get a bit complicated to follow.
+
 * (any other nonterminal name) - adds a new production (and possibly a new nonterminal)
 to the grammar.
 
diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg
index ea94e21ff3..06b49a0a18 100644
--- a/doc/tools/docgram/common.edit_mlg
+++ b/doc/tools/docgram/common.edit_mlg
@@ -12,41 +12,10 @@
 
 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
-]
-
+(* renames to eliminate qualified names
+   put other renames at the end *)
 RENAME: [
   (* map missing names for rhs *)
-| _binders binders
 | Constr.constr term
 | Constr.constr_pattern constr_pattern
 | Constr.global global
@@ -54,58 +23,52 @@ RENAME: [
 | 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
+| Pltac.tactic_expr tactic_expr5
 | 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
+(* written in OCaml *)
+impl_ident_head: [
+| "{" ident
 ]
 
+lpar_id_coloneq: [
+| "(" ident; ":="
+]
+
+(* lookahead symbols *)
 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_colon
+| test_lpar_id_coloneq  (* todo: grammar seems incorrect, repeats the "(" IDENT ":=" *)
 | test_lpar_id_rpar
 | test_lpar_idnum_coloneq
+| test_nospace_pipe_closedcurly
 | test_show_goal
 
   (* SSR *)
 (* | ssr_null_entry *)
+(*
 | ssrtermkind  (* todo: rename as "test..." *)
 | term_annotation  (* todo: rename as "test..." *)
 | test_idcomma
@@ -122,48 +85,410 @@ DELETE: [
 | test_ident_no_do
 | ssrdoarg  (* todo: this and the next one should be removed from the grammar? *)
 | ssrseqdir
+*)
+
+(* unused *)
+| constr_comma_sequence'
+| auto_using'
+| constr_may_eval
 ]
 
-ident: [
-| DELETE IDENT ssr_null_entry
+(* ssrintrosarg: [ | DELETENT ] *)
+
+(* additional nts to be spliced *)
+
+hyp: [
+| var
 ]
 
-natural: [
-| DELETE _natural
+empty: [
+|
 ]
 
+or_opt: [
+| "|"
+| empty
+]
 
-  (* added productions *)
+ltac_expr_opt: [
+| tactic_expr5
+| empty
+]
 
-empty: [  (* todo: (bug) this is getting converted to empty -> empty *)
-|
+ltac_expr_opt_list_or: [
+| ltac_expr_opt_list_or "|" ltac_expr_opt
+| ltac_expr_opt
 ]
 
-lpar_id_coloneq: [
-| "(" IDENT; ":="
+tactic_then_gen: [
+| EDIT ADD_OPT tactic_expr5 "|" tactic_then_gen
+| EDIT ADD_OPT tactic_expr5 ".." tactic_then_last
+| REPLACE OPT tactic_expr5 ".." tactic_then_last
+| WITH ltac_expr_opt ".." or_opt ltac_expr_opt_list_or
 ]
 
-name_colon: [
-| IDENT; ":"
-| "_" ":"  (* todo: should "_" be a keyword or an identifier? *)
+ltac_expr_opt_list_or: [
+| ltac_expr_opt_list_or "|" OPT tactic_expr5
+| OPT tactic_expr5
 ]
 
-int: [ (* todo: probably should be NUMERAL *)
-| integer
+reference: [ | DELETENT ]
+
+reference: [
+| qualid
 ]
 
-command_entry: [
-| noedit_mode
+fullyqualid: [ | DELETENT ]
+
+fullyqualid: [
+| qualid
+]
+
+
+field: [ | DELETENT ]
+
+field: [
+| "." ident
+]
+
+basequalid: [
+| REPLACE ident fields
+| WITH qualid field
+]
+
+fields: [ | DELETENT ]
+
+dirpath: [
+| REPLACE ident LIST0 field
+| WITH ident
+| dirpath field
 ]
 
 binders: [
 | DELETE Pcoq.Constr.binders  (* todo: not sure why there are 2 "binders:" *)
 ]
 
-(* edits to simplify *)
+lconstr: [
+| DELETE l_constr
+]
+
+let_type_cstr: [
+| DELETE OPT [ ":" lconstr ]
+| rec_type_cstr
+]
+
+as_name_opt: [
+| "as" name
+| empty
+]
+
+(* rename here because we want to use "return_type" for something else *)
+RENAME: [
+| return_type as_return_type_opt
+]
+
+as_return_type_opt: [
+| REPLACE OPT [ OPT [ "as" name ] case_type ]
+| WITH as_name_opt case_type
+| empty
+]
+
+case_item: [
+| REPLACE operconstr100 OPT [ "as" name ] OPT [ "in" pattern200 ]
+| WITH operconstr100 as_name_opt OPT [ "in" pattern200 ]
+]
+
+as_dirpath: [
+| DELETE OPT [ "as" dirpath ]
+| "as" dirpath
+| empty
+]
+
+binder_constr: [
+| MOVETO term_let "let" name binders let_type_cstr ":=" operconstr200 "in" operconstr200
+| MOVETO term_let "let" single_fix "in" operconstr200
+| MOVETO term_let "let" [ "(" LIST0 name SEP "," ")" | "()" ] as_return_type_opt ":=" operconstr200 "in" operconstr200
+| MOVETO term_let "let" "'" pattern200 ":=" operconstr200 "in" operconstr200
+| MOVETO term_let "let" "'" pattern200 ":=" operconstr200 case_type "in" operconstr200
+| MOVETO term_let "let" "'" pattern200 "in" pattern200 ":=" operconstr200 case_type "in" operconstr200
+]
+
+term_let: [
+| REPLACE "let" name binders let_type_cstr ":=" operconstr200 "in" operconstr200
+| WITH "let" name let_type_cstr ":=" operconstr200 "in" operconstr200
+| "let" name LIST1 binder let_type_cstr ":=" operconstr200 "in" operconstr200
+(* Don't need to document that "( )" is equivalent to "()" *)
+| REPLACE "let" [ "(" LIST0 name SEP "," ")" | "()" ] as_return_type_opt ":=" operconstr200 "in" operconstr200
+| WITH "let" [ "(" LIST1 name SEP "," ")" | "()" ] as_return_type_opt ":=" operconstr200 "in" operconstr200
+| REPLACE "let" "'" pattern200 ":=" operconstr200 "in" operconstr200
+| WITH  "let" "'" pattern200 ":=" operconstr200 OPT case_type "in" operconstr200
+| DELETE "let" "'" pattern200 ":=" operconstr200 case_type "in" operconstr200
+]
+
+atomic_constr: [
+(* @Zimmi48: "string" used only for notations, but keep to be consistent with patterns *)
+(* | DELETE string *)
+| REPLACE "?" "[" ident "]"
+| WITH "?[" ident "]"
+| MOVETO term_evar "?[" ident "]"
+| REPLACE "?" "[" pattern_ident "]"
+| WITH "?[" pattern_ident "]"
+| MOVETO term_evar "?[" pattern_ident "]"
+| MOVETO term_evar pattern_ident evar_instance
+]
+
+tactic_expr0: [
+| REPLACE "[" ">" tactic_then_gen "]"
+| WITH "[>" tactic_then_gen "]"
+]
+
+operconstr100: [
+| MOVETO term_cast operconstr99 "<:" operconstr200
+| MOVETO term_cast operconstr99 "<<:" operconstr200
+| MOVETO term_cast operconstr99 ":" operconstr200
+| MOVETO term_cast operconstr99 ":>"
+]
+
+operconstr10: [
+(* fixme: add in as a prodn somewhere *)
+| MOVETO dangling_pattern_extension_rule "@" pattern_identref LIST1 identref
+| DELETE dangling_pattern_extension_rule
+]
+
+operconstr9: [
+(* @Zimmi48: Special token .. is for use in the Notation command. (see bug_3304.v) *)
+| DELETE ".." operconstr0 ".."
+]
+
+arg_list: [
+| arg_list appl_arg
+| appl_arg
+]
+
+arg_list_opt: [
+| arg_list
+| empty
+]
+
+operconstr1: [
+| REPLACE operconstr0 ".(" global LIST0 appl_arg ")"
+| WITH operconstr0 ".(" global arg_list_opt ")"
+| MOVETO term_projection operconstr0 ".(" global arg_list_opt ")"
+| MOVETO term_projection operconstr0 ".(" "@" global LIST0 ( operconstr9 ) ")"
+]
+
+operconstr0: [
+(* @Zimmi48: This rule is a hack, according to Hugo, and should not be shown in the manual. *)
+| DELETE "{" binder_constr "}"
+]
+
+single_fix: [
+| DELETE fix_kw fix_decl
+| "fix" fix_decl
+| "cofix" fix_decl
+]
+
+fix_kw: [ | DELETENT ]
+
+binders_fixannot: [
+(*
+| REPLACE impl_name_head impl_ident_tail binders_fixannot
+| WITH impl_name_head impl_ident_tail "}" binders_fixannot
+*)
+(* Omit this complex detail.  See https://github.com/coq/coq/pull/10614#discussion_r344118146 *)
+| DELETE impl_name_head impl_ident_tail binders_fixannot
+
+| DELETE fixannot
+| DELETE binder binders_fixannot
+| DELETE (* empty *)
+
+| LIST0 binder OPT fixannot
+]
 
-ltac_expr1: [
+impl_ident_tail: [
+| DELETENT
+(*
+| REPLACE "}"
+| WITH empty
+| REPLACE LIST1 name ":" lconstr "}"
+| WITH LIST1 name ":" lconstr
+| REPLACE LIST1 name "}"
+| WITH LIST1 name
+| REPLACE ":" lconstr "}"
+| WITH ":" lconstr
+*)
+]
+
+of_type_with_opt_coercion: [
+| DELETE ":>" ">"
+| DELETE ":" ">" ">"
+| DELETE ":" ">"
+]
+
+binder: [
+| DELETE name
+]
+
+open_binders: [
+| REPLACE name LIST0 name ":" lconstr
+| WITH LIST1 name ":" lconstr
+(* @Zimmi48: Special token .. is for use in the Notation command. (see bug_3304.v) *)
+| DELETE name ".." name
+| REPLACE name LIST0 name binders
+| WITH LIST1 binder
+| DELETE closed_binder binders
+]
+
+closed_binder: [
+| name
+
+| REPLACE "(" name LIST1 name ":" lconstr ")"
+| WITH "(" LIST1 name ":" lconstr ")"
+| DELETE "(" name ":" lconstr ")"
+
+| DELETE "(" name ":=" lconstr ")"
+| REPLACE "(" name ":" lconstr ":=" lconstr ")"
+| WITH "(" name rec_type_cstr ":=" lconstr ")"
+
+| DELETE "{" name LIST1 name "}"
+
+| REPLACE "{" name LIST1 name ":" lconstr "}"
+| WITH "{" LIST1 name rec_type_cstr "}"
+| DELETE "{" name ":" lconstr  "}"
+]
+
+typeclass_constraint: [
+| EDIT ADD_OPT "!" operconstr200
+]
+
+(* ?? From the grammar, Prim.name seems to be only "_" but ident is also accepted "*)
+Prim.name: [
+| REPLACE "_"
+| WITH name
+]
+
+oriented_rewriter: [
+| REPLACE orient_rw rewriter
+| WITH orient rewriter
+]
+
+DELETE: [
+| orient_rw
+]
+
+pattern1_list: [
+| pattern1_list pattern1
+| pattern1
+]
+
+pattern1_list_opt: [
+| pattern1_list
+| empty
+]
+
+pattern10: [
+| REPLACE pattern1 LIST1 pattern1
+| WITH LIST1 pattern1
+| REPLACE "@" reference LIST0 pattern1
+| WITH "@" reference pattern1_list_opt
+]
+
+pattern0: [
+| REPLACE "(" pattern200 ")"
+| WITH "(" LIST1 pattern200 SEP "|" ")"
+| DELETE "(" pattern200 "|" LIST1 pattern200 SEP "|" ")"
+]
+
+patterns_comma: [
+| patterns_comma "," pattern100
+| pattern100
+]
+
+patterns_comma_list_or: [
+| patterns_comma_list_or "|" patterns_comma
+| patterns_comma
+]
+
+eqn: [
+| REPLACE LIST1 mult_pattern SEP "|" "=>" lconstr
+| WITH patterns_comma_list_or "=>" lconstr
+]
+
+record_patterns: [
+| REPLACE record_pattern ";" record_patterns
+| WITH record_patterns ";" record_pattern
+]
+
+(* todo: binders should be binders_opt *)
+
+
+(* lexer stuff *)
+bigint: [
+| DELETE NUMERAL
+| num
+]
+
+ident: [
+| DELETENT
+]
+
+IDENT: [
+| ident
+]
+
+integer: [ | DELETENT ]
+RENAME: [
+| integer int (* todo: review uses in .mlg files, some should be "natural" *)
+]
+
+LEFTQMARK: [
+| "?"
+]
+
+natural: [ | DELETENT ]
+natural: [
+| num  (* todo: or should it be "nat"? *)
+]
+
+NUMERAL: [
+| numeral
+]
+
+(* todo: QUOTATION only used in a test suite .mlg files, is it documented/useful? *)
+
+string: [ | DELETENT ]
+STRING: [
+| string
+]
+
+
+(* todo: is "bigint" useful?? *)
+(* todo: "check_int" in g_prim.mlg should be "check_num" *)
+
+  (* added productions *)
+
+name_colon: [
+| name ":"
+]
+
+command_entry: [
+| noedit_mode
+]
+
+tactic_expr1: [
 | EDIT match_key ADD_OPT "reverse" "goal" "with" match_context_list "end"
+| MOVETO ltac_match_goal match_key OPT "reverse" "goal" "with" match_context_list "end"
+| MOVETO ltac_match_term match_key tactic_expr5 "with" match_list "end"
+]
+
+DELETE: [
+| tactic_then_locality
+]
+
+tactic_expr4: [
+| REPLACE tactic_expr3 ";" tactic_then_gen "]"
+| WITH tactic_expr3 ";" "[" tactic_then_gen "]"
+| tactic_expr3 ";" "[" ">" tactic_then_gen "]"
 ]
 
 match_context_list: [
@@ -180,35 +505,37 @@ match_list: [
 | EDIT ADD_OPT "|" LIST1 match_rule SEP "|"
 ]
 
+match_rule: [
+| REPLACE match_pattern "=>" tactic_expr5
+| WITH [ match_pattern | "_" ] "=>" tactic_expr5
+| DELETE "_" "=>" tactic_expr5
+]
+
 
 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
-]
+range_selector_or_nth: [ | DELETENT ]
 
 simple_tactic: [
 | DELETE "intros"
 | REPLACE "intros" ne_intropatterns
-| WITH "intros" intropattern_list_opt
+| WITH "intros" intropatterns
 | DELETE "eintros"
 | REPLACE "eintros" ne_intropatterns
-| WITH "eintros" intropattern_list_opt
+| WITH "eintros" intropatterns
 ]
 
-intropattern_list_opt: [
+intropatterns: [
 | DELETE LIST0 intropattern
-| intropattern_list_opt intropattern
+| intropatterns intropattern
 | empty
 ]
 
-
-ne_intropatterns: [
-| DELETENT  (* todo: don't use DELETENT for this *)
-]
+(* todo: don't use DELETENT for this *)
+ne_intropatterns: [ | DELETENT ]
 
 
 or_and_intropattern: [
@@ -216,5 +543,181 @@ or_and_intropattern: [
 | 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 "|" "]"
+| EDIT "[" USE_NT intropattern_or LIST1 intropatterns SEP "|" "]"
 ]
+
+bar_cbrace: [
+| REPLACE "|" "}"
+| WITH "|}"
+]
+
+(* todo: is this really correct? Search for "Pvernac.register_proof_mode" *)
+(* consider tactic_command vs tac2mode *)
+vernac_aux: [
+| tactic_mode "."
+]
+
+SPLICE: [
+| noedit_mode
+| command_entry
+| bigint
+| match_list
+| match_context_list
+| IDENT
+| LEFTQMARK
+| natural
+| NUMERAL
+| STRING
+| hyp
+| var
+| identref
+| pattern_ident
+| constr_eval  (* splices as multiple prods *)
+| tactic_then_last  (* todo: dependency on c.edit_mlg edit?? really useful? *)
+| Prim.name
+| ltac_selector
+| Constr.ident
+| attribute_list
+| operconstr99
+| operconstr90
+| operconstr9
+| operconstr8
+| pattern200
+| pattern99
+| pattern90
+| ne_lstring
+| ne_string
+| lstring
+| basequalid
+| fullyqualid
+| global
+| reference
+| bar_cbrace
+| lconstr
+| impl_name_head
+
+(*
+| ast_closure_term
+| ast_closure_lterm
+| ident_no_do
+| ssrterm
+| ssrtacarg
+| ssrtac3arg
+| ssrtclarg
+| ssrhyp
+| ssrhoi_hyp
+| ssrhoi_id
+| ssrindex
+| ssrhpats
+| ssrhpats_nobs
+| ssrfwdid
+| ssrmovearg
+| ssrcasearg
+| ssrrwargs
+| ssrviewposspc
+| ssrpatternarg
+| ssr_elsepat
+| ssr_mpat
+| ssrunlockargs
+| ssrcofixfwd
+| ssrfixfwd
+| ssrhavefwdwbinders
+| ssripats_ne
+| ssrparentacarg
+| ssrposefwd
+*)
+
+| preident
+| lpar_id_coloneq
+| binders
+| casted_constr
+| check_module_types
+| constr_pattern
+| decl_sep
+| function_rec_definition_loc (* loses funind annotation *)
+| glob
+| glob_constr_with_bindings
+| id_or_meta
+| lconstr_pattern
+| lglob
+| ltac_tacdef_body
+| mode
+| mult_pattern
+| open_constr
+| option_table
+| record_declaration
+| register_type_token
+| tactic
+| uconstr
+| impl_ident_head
+| argument_spec
+| at_level
+| branches
+| check_module_type
+| decorated_vernac
+| ext_module_expr
+| ext_module_type
+| pattern_identref
+| test
+| binder_constr
+| atomic_constr
+| let_type_cstr
+| name_colon
+| closed_binder
+| binders_fixannot
+]
+
+RENAME: [
+| clause clause_dft_concl
+| in_clause' in_clause
+
+| 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
+
+(* | nonsimple_intropattern intropattern (* ltac2 *) *)
+| intropatterns intropattern_list_opt
+
+| operconstr200 term   (* historical name *)
+| operconstr100 term100
+| operconstr10 term10
+| operconstr1 term1
+| operconstr0 term0
+| pattern100 pattern
+| match_constr term_match
+(*| impl_ident_tail impl_ident*)
+| ssexpr35 ssexpr (* strange in mlg, ssexpr50 is after this *)
+
+| tactic_then_gen multi_goal_tactics
+| selector only_selector
+| selector_body selector
+| input_fun fun_var
+| match_hyps match_hyp
+
+| BULLET bullet
+| nat_or_var num_or_var
+| fix_decl fix_body
+| instance universe_annot_opt
+| rec_type_cstr colon_term_opt
+| fix_constr term_fix
+| constr term1_extended
+| case_type return_type
+| appl_arg arg
+| record_patterns record_patterns_opt
+| universe_increment universe_increment_opt
+| rec_definition fix_definition
+| corec_definition cofix_definition
+| record_field_instance field_def
+| record_fields_instance fields_def
+| evar_instance evar_bindings_opt
+| inst evar_binding
+]
+
+
+(* todo: ssrreflect*.rst ref to fix_body is incorrect *)
diff --git a/doc/tools/docgram/doc_grammar.ml b/doc/tools/docgram/doc_grammar.ml
index eb86bab37e..70976e705e 100644
--- a/doc/tools/docgram/doc_grammar.ml
+++ b/doc/tools/docgram/doc_grammar.ml
@@ -48,6 +48,9 @@ let default_args = {
   verify = false;
 }
 
+let start_symbols = ["vernac_toplevel"]
+let tokens = [ "bullet"; "ident"; "int"; "num"; "numeral"; "string" ]
+
 (* translated symbols *)
 
 type doc_symbol =
@@ -128,8 +131,8 @@ module DocGram = struct
     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 g_add_after g ?(update=true) ins_after nt prods =
+    if (not update) && 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
@@ -143,6 +146,11 @@ module DocGram = struct
     g := { order = insert_nt !g.order [];
            map = NTMap.add nt prods !g.map }
 
+  let g_add_prod_after g ins_after nt prod =
+    let prods = try NTMap.find nt !g.map with Not_found -> [] in
+    (* todo: add check for duplicates *)
+    g_add_after g ~update:true ins_after nt (prods @ [prod])
+
   (* replace the map and order *)
   let g_reorder g map order =
     let order_nts = StringSet.of_list order in
@@ -188,13 +196,13 @@ let rec output_prod plist need_semi = function
     | 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 ->
+    | Sprod sym_list_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))
+        sym_list_list))
     | Sedit s -> sprintf "%s" s
     (* todo: make PLUGIN info output conditional on the set of prods? *)
     | Sedit2 ("PLUGIN", plugin) ->
@@ -213,6 +221,8 @@ let rec output_prod plist need_semi = function
 
 and prod_to_str_r plist prod =
   match prod with
+  | Sterm s :: Snterm "ident" :: tl when List.mem s ["?"; "."] && plist ->
+    (sprintf "%s`ident`" s) :: (prod_to_str_r plist tl)
   | p :: tl ->
     let need_semi =
       match prod with
@@ -258,6 +268,15 @@ and output_sep sep =
 
 and prod_to_prodn prod = String.concat " " (List.map output_prodn prod)
 
+let pr_prods nt prods = (* duplicative *)
+  Printf.printf "%s: [\n" nt;
+  List.iter (fun prod ->
+      let str = prod_to_str ~plist:false prod in
+      let pfx = if str = "" then "|" else "| " in
+      Printf.printf "%s%s\n" pfx str)
+    prods;
+  Printf.printf "]\n\n"
+
 type fmt = [`MLG | `PRODLIST | `PRODN ]
 
 (* print a subset of the grammar with nts in the specified order *)
@@ -313,6 +332,8 @@ let cvt_ext prod =
  in
  List.map from_ext prod
 
+let keywords = ref StringSet.empty
+
 let rec cvt_gram_sym = function
   | GSymbString s -> Sterm s
   | GSymbQualid (s, level) ->
@@ -352,6 +373,10 @@ and cvt_gram_sym_list l =
     (Sedit2 ("NOTE", s2)) :: cvt_gram_sym_list tl
   | GSymbQualid ("USE_NT", _) :: GSymbQualid (s2, l) :: tl ->
     (Sedit2 ("USE_NT", s2)) :: cvt_gram_sym_list tl
+  | GSymbString s :: tl ->
+    (* todo: not seeing "(bfs)" here for some reason *)
+    keywords := StringSet.add s !keywords;
+    cvt_gram_sym (GSymbString s) :: cvt_gram_sym_list tl
   | hd :: tl ->
     cvt_gram_sym hd :: cvt_gram_sym_list tl
   | [] -> []
@@ -453,6 +478,7 @@ 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 locals = ref StringSet.empty in
   let add_prods nt prods =
     if not is_edit then
       add_symdef nt file symdef_map;
@@ -478,6 +504,8 @@ let read_mlg is_edit ast file level_renames symdef_map =
           let len = List.length ent.gentry_rules in
           List.iteri (fun i rule ->
               let nt = ent.gentry_name in
+              if not (List.mem nt grammar_ext.gramext_globals) then
+                locals := StringSet.add nt !locals;
               let level = (get_label rule.grule_label) in
               let level = if level <> "" then level else
                 match ent.gentry_pos with
@@ -528,7 +556,7 @@ let read_mlg is_edit ast file level_renames symdef_map =
   in
 
   List.iter prod_loop ast;
-  List.rev !res
+  List.rev !res, !locals
 
 let dir s = "doc/tools/docgram/" ^ s
 
@@ -536,7 +564,8 @@ 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 prods, _ = read_mlg true (parse_file fdir) fdir level_renames symdef_map in
+  prods
 
 let add_rule g nt prods file =
   let ent = try NTMap.find nt !g.map with Not_found -> [] in
@@ -555,9 +584,12 @@ let read_mlg_files g args symdef_map =
   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 rules, locals = 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
+        if NTMap.mem nt !g.map && (StringSet.mem nt locals) &&
+            StringSet.cardinal (StringSet.of_list (StringMap.find nt !symdef_map)) > 1 then
+          warn "%s: local nonterminal '%s' already defined\n" file nt;
         add_rule g nt prods file;
         num + List.length prods)
       0 rules
@@ -572,18 +604,74 @@ let read_mlg_files g args symdef_map =
   !level_renames
 
 
+ (* 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 -> if List.mem s tokens then [] else [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))
+
+let get_refdef_nts g =
+  let rec get_nts_r refd defd bindings =
+    match bindings with
+    | [] -> refd, defd
+    | (nt, prods) :: tl ->
+      get_nts_r (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 toks = StringSet.of_list tokens in
+   get_nts_r toks toks (NTMap.bindings !g.map)
+
+
 (*** global editing ops ***)
 
-let create_edit_map edits =
+let create_edit_map g op edits =
   let rec aux edits map =
     match edits with
     | [] -> map
     | edit :: tl ->
       let (key, binding) = edit in
+      let all_nts_ref, all_nts_def = get_refdef_nts g in
+      (match op with
+      (* todo: messages should tell you which edit file causes the error *)
+      | "SPLICE" ->
+        if not (StringSet.mem key all_nts_def) then
+          error "Undefined nt `%s` in SPLICE\n" key
+      | "DELETE" ->
+        if not (StringSet.mem key all_nts_ref || (StringSet.mem key all_nts_def)) then
+          error "Unused/undefined nt `%s` in DELETE\n" key;
+      | "RENAME" ->
+        if not (StringSet.mem key all_nts_ref || (StringSet.mem key all_nts_def)) then
+          error "Unused/undefined  nt `%s` in RENAME\n" key;
+(*      todo: could not get the following codeto type check
+        (match binding with
+        | _ :: Snterm new_nt :: _ ->
+          if not (StringSet.mem new_nt all_nts_ref) then
+            error "nt `%s` already exists in %s\n" new_nt op
+        | _ -> ())
+*)
+      | _ -> ());
       aux tl (StringMap.add key binding map)
   in
   aux edits StringMap.empty
 
+let remove_Sedit2 p =
+  List.filter (fun sym -> match sym with | Sedit2 _ -> false | _ -> true) p
+
 (* 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 =
@@ -596,8 +684,8 @@ let rec edit_prod g top edit_map prod =
           try let splice_prods = NTMap.find nt !g.map in
             match splice_prods with
             | [] -> assert false
-            | [p] -> List.rev p
-            | _ -> [Sprod splice_prods]
+            | [p] -> List.rev (remove_Sedit2 p)
+            | _ -> [Sprod (List.map remove_Sedit2 splice_prods)]
           with Not_found -> error "Missing nt '%s' for splice\n" nt; [Snterm nt]
         end
       | _ -> [Snterm binding]
@@ -654,16 +742,22 @@ and edit_rule g edit_map nt rule =
 
 (*** splice: replace a reference to a nonterminal with its definition ***)
 
-(* todo: create a better splice routine, handle recursive case *)
+(* todo: create a better splice routine *)
 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)
+      let (nt0, prods0) = b in
+      let rec splice_loop nt prods cnt =
+        let max_cnt = 10 in
+        let (nt', prods') = edit_rule g splice_map nt prods in
+        if cnt > max_cnt then
+          error "Splice for '%s' not done after %d iterations\n" nt0 max_cnt;
+        if nt' = nt && prods' = prods then
+          (nt', prods')
+        else
+          splice_loop nt' prods' (cnt+1)
+      in
+      let (nt', prods') = splice_loop nt0 prods0 0 in
+      g_update_prods g nt' prods')
     (NTMap.bindings !g.map);
   List.iter (fun b ->
       let (nt, op) = b in
@@ -678,7 +772,7 @@ 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;
+      error "Can't find '%s' in edit for '%s'\n" (prod_to_str edit) nt;
       raise Not_found
     | prod :: tl ->
       if ematch prod edit then i
@@ -906,7 +1000,7 @@ let edit_all_prods g op eprods =
             op (prod_to_str eprod) num;
         aux tl res
     in
-    let map = create_edit_map (aux eprods []) in
+    let map = create_edit_map g op (aux eprods []) in
     if op = "SPLICE" then
       apply_splice g map
     else (* RENAME/DELETE *)
@@ -960,6 +1054,13 @@ let edit_single_prod g edit0 prods nt =
   in
   edit_single_prod_r edit0 prods nt []
 
+let report_undef_nts g prod rec_nt =
+  let nts = nts_in_prod prod in
+  List.iter (fun nt ->
+      if not (NTMap.mem nt !g.map) && not (List.mem nt tokens) && nt <> rec_nt then
+        error "Undefined nonterminal `%s` in edit: %s\n" nt (prod_to_str prod))
+    nts
+
 let apply_edit_file g edits =
   List.iter (fun b ->
       let (nt, eprod) = b in
@@ -970,11 +1071,26 @@ let apply_edit_file g edits =
           | (Snterm "DELETE" :: oprod) :: tl ->
             aux tl (remove_prod oprod prods nt) add_nt
           | (Snterm "DELETENT" :: _) :: tl ->  (* note this doesn't remove references *)
+            if not (NTMap.mem nt !g.map) then
+              error "DELETENT for undefined nonterminal `%s`\n" nt;
             g_remove g nt;
             aux tl prods false
+          | (Snterm "MOVETO" :: Snterm nt2 :: oprod) :: tl ->
+            g_add_prod_after g (Some nt) nt2 oprod;
+            let prods' = (try
+              let posn = find_first oprod prods nt in
+              let prods = insert_after posn [[Snterm nt2]] prods in  (* insert new prod *)
+              remove_prod oprod prods nt      (* remove orig prod *)
+              with Not_found -> prods)
+            in
+            aux tl prods' add_nt
+          | (Snterm "PRINT" :: _) :: tl ->
+            pr_prods nt (NTMap.find nt !g.map);
+            aux tl prods add_nt
           | (Snterm "EDIT" :: oprod) :: tl ->
             aux tl (edit_single_prod g oprod prods nt) add_nt
           | (Snterm "REPLACE" :: oprod) :: (Snterm "WITH" :: rprod) :: tl ->
+            report_undef_nts g rprod "";
             let prods' = (try
               let posn = find_first oprod prods nt in
               let prods = insert_after posn [rprod] prods in  (* insert new prod *)
@@ -985,10 +1101,12 @@ let apply_edit_file g edits =
           | (Snterm "REPLACE" :: _ as eprod) :: tl ->
             error "Missing WITH after '%s' in '%s'\n" (prod_to_str eprod) nt;
             aux tl prods add_nt
+          (* todo: check for unmatched editing keywords here *)
           | prod :: tl ->
             (* add a production *)
             if has_match prod prods then
               error "Duplicate production '%s' for %s\n" (prod_to_str prod) nt;
+            report_undef_nts g prod nt;
             aux tl (prods @ [prod]) add_nt
         in
         let prods, add_nt =
@@ -1001,25 +1119,6 @@ let apply_edit_file g 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 special tokens in the grammar *)
 let print_special_tokens g =
   let rec traverse set = function
@@ -1129,24 +1228,156 @@ let print_chunks g out fmt () =
 
     (*seen := StringSet.diff !seen (StringSet.of_list ssr_tops);*)
     (*print_chunk out g seen fmt "vernac_toplevel" ["vernac_toplevel"] [];*)
+let index_of str list =
+  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
+  index_of_r str list 0
 
-let start_symbols = ["vernac_toplevel"]
-(* don't report tokens as undefined *)
-let tokens = [ "bullet"; "field"; "ident"; "int"; "num"; "numeral"; "string" ]
+exception IsNone
 
-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
+(* todo: raise exception for bad n? *)
+let rec nthcdr n list = if n <= 0 then list else nthcdr (n-1) (List.tl list)
+
+let pfx n list =
+  let rec pfx_r n res = function
+    | item :: tl -> if n < 0 then res else pfx_r (n-1) (item :: res) tl
+    | [] -> res
+  in
+  List.rev (pfx_r n [] list)
+
+(* todo: adjust Makefile to include Option.ml/mli *)
+let get_opt = function
+  | Some y -> y
+  | _ -> raise IsNone
+
+let get_range g start end_ =
+  let starti, endi = get_opt (index_of start !g.order), get_opt (index_of end_ !g.order) in
+  pfx (endi - starti) (nthcdr starti !g.order)
+
+let get_rangeset g start end_ = StringSet.of_list (get_range g start end_)
+
+let print_dominated g =
+  let info nt rangeset exclude =
+    let reachable = StringSet.of_list (nt_closure g nt exclude) in
+    let unreachable = StringSet.of_list (nt_closure g (List.hd start_symbols) (nt::exclude)) in
+    let dominated = StringSet.diff reachable unreachable in
+    Printf.printf "For %s, 'attribute' is: reachable = %b, unreachable = %b, dominated = %b\n" nt
+        (StringSet.mem "attribute" reachable)
+        (StringSet.mem "attribute" unreachable)
+        (StringSet.mem "attribute" dominated);
+    Printf.printf "  rangeset = %b excluded = %b\n"
+        (StringSet.mem "attribute" rangeset)
+        (List.mem "attribute" exclude);
+    reachable, dominated
+  in
+  let pr3 nt rangeset reachable dominated =
+    let missing = StringSet.diff dominated rangeset in
+    if not (StringSet.is_empty missing) then begin
+      Printf.printf "\nMissing in range for '%s':\n" nt;
+      StringSet.iter (fun nt -> Printf.printf "  %s\n" nt) missing
+    end;
+
+    let unneeded = StringSet.diff rangeset reachable in
+    if not (StringSet.is_empty unneeded) then begin
+      Printf.printf "\nUnneeded in range for '%s':\n" nt;
+      StringSet.iter (fun nt -> Printf.printf "  %s\n" nt) unneeded
+    end;
   in
-  let all_nts_ref, all_nts_def =
-    get_nts (StringSet.of_list tokens) (StringSet.of_list tokens) (NTMap.bindings !g.map) in
+  let pr2 nt rangeset exclude =
+    let reachable, dominated = info nt rangeset exclude in
+    pr3 nt rangeset reachable dominated
+  in
+  let pr nt end_ = pr2 nt (get_rangeset g nt end_) [] in
+
+  let ssr_ltac = ["ssr_first_else"; "ssrmmod"; "ssrdotac"; "ssrortacarg";
+      "ssrparentacarg"] in
+  let ssr_tac = ["ssrintrosarg"; "ssrhintarg"; "ssrtclarg"; "ssrseqarg"; "ssrmovearg";
+      "ssrrpat"; "ssrclauses"; "ssrcasearg"; "ssrarg"; "ssrapplyarg"; "ssrexactarg";
+      "ssrcongrarg"; "ssrterm"; "ssrrwargs"; "ssrunlockargs"; "ssrfixfwd"; "ssrcofixfwd";
+      "ssrfwdid"; "ssrposefwd"; "ssrsetfwd"; "ssrdgens"; "ssrhavefwdwbinders"; "ssrhpats_nobs";
+      "ssrhavefwd"; "ssrsufffwd"; "ssrwlogfwd"; "ssrhint"; "ssrclear"; "ssr_idcomma";
+      "ssrrwarg"; "ssrintros_ne"; "ssrhint3arg" ] @ ssr_ltac in
+  let ssr_cmd = ["ssr_modlocs"; "ssr_search_arg"; "ssrhintref"; "ssrhintref_list";
+      "ssrviewpos"; "ssrviewposspc"] in
+  let ltac = ["ltac_expr"; "ltac_expr0"; "ltac_expr1"; "ltac_expr2"; "ltac_expr3"] in
+  let term = ["term"; "term0"; "term1"; "term10"; "term100"; "term9";
+      "pattern"; "pattern0"; "pattern1"; "pattern10"] in
+
+  pr "term" "constr";
+
+  let ltac_rangeset = List.fold_left StringSet.union StringSet.empty
+                            [(get_rangeset g "ltac_expr" "tactic_atom");
+                            (get_rangeset g "toplevel_selector" "range_selector");
+                            (get_rangeset g "ltac_match_term" "match_pattern");
+                            (get_rangeset g "ltac_match_goal" "match_pattern_opt")] in
+  pr2 "ltac_expr" ltac_rangeset ("simple_tactic" :: ssr_tac);
+
+  let dec_vern_rangeset = get_rangeset g "decorated_vernac" "opt_coercion" in
+  let dev_vern_excl =
+      ["gallina_ext"; "command"; "tactic_mode"; "syntax"; "command_entry"] @ term @ ltac @ ssr_tac in
+  pr2 "decorated_vernac" dec_vern_rangeset dev_vern_excl;
+
+  let simp_tac_range = get_rangeset g "simple_tactic" "hypident_occ_list_comma" in
+  let simp_tac_excl = ltac @ ssr_tac in
+  pr2 "simple_tactic" simp_tac_range simp_tac_excl;
+
+  let cmd_range = get_rangeset g "command" "int_or_id_list_opt" in
+  let cmd_excl = ssr_tac @ ssr_cmd in
+  pr2 "command" cmd_range cmd_excl;
+
+  let syn_range = get_rangeset g "syntax" "constr_as_binder_kind" in
+  let syn_excl = ssr_tac @ ssr_cmd in
+  pr2 "syntax" syn_range syn_excl;
+
+  let gext_range = get_rangeset g "gallina_ext" "Structure_opt" in
+  let gext_excl = ssr_tac @ ssr_cmd in
+  pr2 "gallina_ext" gext_range gext_excl;
+
+  let qry_range = get_rangeset g "query_command" "searchabout_query_list" in
+  let qry_excl = ssr_tac @ ssr_cmd in
+  pr2 "query_command" qry_range qry_excl
+
+  (* todo: tactic_mode *)
+
+let check_range_consistency g start end_ =
+  let defined_list = get_range g start end_ in
+  let defined = StringSet.of_list defined_list in
+  let referenced = List.fold_left (fun set nt ->
+      let prods = NTMap.find nt !g.map in
+      let refs = List.concat (List.map nts_in_prod prods) in
+      StringSet.union set (StringSet.of_list refs))
+    StringSet.empty defined_list
+  in
+  let undef = StringSet.diff referenced defined in
+  let unused = StringSet.diff defined referenced in
+  if StringSet.cardinal unused > 0 || (StringSet.cardinal undef > 0) then begin
+    Printf.printf "\nFor range '%s' to '%s':\n  External reference:" start end_;
+    StringSet.iter (fun nt -> Printf.printf " %s" nt) undef;
+    Printf.printf "\n";
+    if StringSet.cardinal unused > 0 then begin
+      Printf.printf "  Unreferenced:";
+      StringSet.iter (fun nt -> Printf.printf " %s" nt) unused;
+      Printf.printf "\n"
+    end
+  end
+
+(* print info on symbols with a single production of a single nonterminal *)
+let check_singletons g =
+  NTMap.iter (fun nt prods ->
+      if List.length prods = 1 then
+        if List.length (remove_Sedit2 (List.hd prods)) = 1 then
+          warn "Singleton non-terminal, maybe SPLICE?: %s\n" nt
+        else
+          (*warn "Single production, maybe SPLICE?: %s\n" nt*) ())
+    !g.map
 
+let report_bad_nts g file =
+  let all_nts_ref, all_nts_def = get_refdef_nts g 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);
 
@@ -1287,12 +1518,13 @@ let finish_with_file old_file verify =
   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
+  if !exit_code <> 0 then
+    Sys.remove temp_file
+  else if verify then begin
+    if not (files_eq old_file temp_file) then
+      error "%s is not current\n" old_file;
+    Sys.remove temp_file
+  end else
     Sys.rename temp_file old_file
 
 let open_temp_bin file =
@@ -1342,21 +1574,13 @@ let process_rst g file args seen tac_prods cmd_prods =
   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
+  (* todo: maybe pass end_index? *)
   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
       | [] -> ()
@@ -1390,10 +1614,12 @@ let process_rst g file args seen tac_prods cmd_prods =
         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_;
+      if start_index <> None && end_index <> None then
+        check_range_consistency g start 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_
+          error "%s line %d: '%s' must appear before '%s' in orderedGrammar\n" file !linenum start end_
         else begin
           try
             let line2 = getline() in
@@ -1470,21 +1696,28 @@ let report_omitted_prods entries seen label split =
     end
   in
 
-  let first, last, n = List.fold_left (fun missing nt ->
-      let first, last, n = missing in
+  let first, last, n, total = List.fold_left (fun missing nt ->
+      let first, last, n, total = missing in
       if NTMap.mem nt seen then begin
         maybe_warn first last n;
-        "", "", 0
+        "", "", 0, total
       end else
-        (if first = "" then nt else first), nt, n + 1)
-    ("", "", 0) entries in
-  maybe_warn first last n
+        (if first = "" then nt else first), nt, n + 1, total + 1)
+    ("", "", 0, 0) entries in
+  maybe_warn first last n;
+  if total <> 0 then
+    Printf.eprintf "TOTAL %ss not included = %d\n" label total
 
 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
+  if args.verbose then begin
+    Printf.printf "Keywords:\n";
+    StringSet.iter (fun kw -> Printf.printf "%s " kw) !keywords;
+    Printf.printf "\n\n";
+  end;
 
   (* rename nts with levels *)
   List.iter (fun b -> let (nt, prod) = b in
@@ -1546,6 +1779,8 @@ let process_grammar args =
       print_in_order out g `MLG !g.order StringSet.empty;
       close_out out;
       finish_with_file (dir "orderedGrammar") args.verify;
+      check_singletons g
+(*      print_dominated g*)
     end;
 
     if !exit_code = 0 then begin
@@ -1558,6 +1793,8 @@ let process_grammar args =
       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" "";
+      let out = open_out (dir "updated_rsts") in
+      close_out out;
       if args.check_tacs then
         report_omitted_prods tac_list !seen.tacs "Tactic" "\n                 ";
       if args.check_cmds then
diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar
index a83638dd73..ebaeb392a5 100644
--- a/doc/tools/docgram/fullGrammar
+++ b/doc/tools/docgram/fullGrammar
@@ -73,12 +73,9 @@ operconstr200: [
 ]
 
 operconstr100: [
-| operconstr99 "<:" binder_constr
-| operconstr99 "<:" operconstr100
-| operconstr99 "<<:" binder_constr
-| operconstr99 "<<:" operconstr100
-| operconstr99 ":" binder_constr
-| operconstr99 ":" operconstr100
+| operconstr99 "<:" operconstr200
+| operconstr99 "<<:" operconstr200
+| operconstr99 ":" operconstr200
 | operconstr99 ":>"
 | operconstr99
 ]
@@ -126,26 +123,23 @@ operconstr0: [
 ]
 
 record_declaration: [
-| record_fields
+| record_fields_instance
 ]
 
-record_fields: [
-| record_field_declaration ";" record_fields
-| record_field_declaration
+record_fields_instance: [
+| record_field_instance ";" record_fields_instance
+| record_field_instance
 |
-| record_field ";" record_fields
-| record_field ";"
-| record_field
 ]
 
-record_field_declaration: [
+record_field_instance: [
 | global binders ":=" lconstr
 ]
 
 binder_constr: [
 | "forall" open_binders "," operconstr200
 | "fun" open_binders "=>" operconstr200
-| "let" name binders type_cstr ":=" operconstr200 "in" operconstr200
+| "let" name binders let_type_cstr ":=" operconstr200 "in" operconstr200
 | "let" single_fix "in" operconstr200
 | "let" [ "(" LIST0 name SEP "," ")" | "()" ] return_type ":=" operconstr200 "in" operconstr200
 | "let" "'" pattern200 ":=" operconstr200 "in" operconstr200
@@ -153,11 +147,6 @@ binder_constr: [
 | "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: [
@@ -213,7 +202,7 @@ fix_kw: [
 ]
 
 fix_decl: [
-| identref binders_fixannot type_cstr ":=" operconstr200
+| identref binders_fixannot let_type_cstr ":=" operconstr200
 ]
 
 match_constr: [
@@ -250,7 +239,6 @@ record_pattern: [
 
 record_patterns: [
 | record_pattern ";" record_patterns
-| record_pattern ";"
 | record_pattern
 |
 ]
@@ -260,8 +248,7 @@ pattern200: [
 ]
 
 pattern100: [
-| pattern99 ":" binder_constr
-| pattern99 ":" operconstr100
+| pattern99 ":" operconstr200
 | pattern99
 ]
 
@@ -306,8 +293,6 @@ fixannot: [
 | "{" "struct" identref "}"
 | "{" "wf" constr identref "}"
 | "{" "measure" constr OPT identref OPT constr "}"
-| "{" "struct" name "}"
-|
 ]
 
 impl_name_head: [
@@ -350,7 +335,6 @@ closed_binder: [
 | "`(" LIST1 typeclass_constraint SEP "," ")"
 | "`{" LIST1 typeclass_constraint SEP "," "}"
 | "'" pattern0
-| [ "of" | "&" ] operconstr99      (* ssr plugin *)
 ]
 
 typeclass_constraint: [
@@ -360,10 +344,8 @@ typeclass_constraint: [
 | operconstr200
 ]
 
-type_cstr: [
+let_type_cstr: [
 | OPT [ ":" lconstr ]
-| ":" lconstr
-|
 ]
 
 preident: [
@@ -467,14 +449,15 @@ bigint: [
 ]
 
 bar_cbrace: [
-| "|" "}"
+| test_nospace_pipe_closedcurly "|" "}"
 ]
 
 vernac_toplevel: [
 | "Drop" "."
 | "Quit" "."
-| "Backtrack" natural natural natural "."
+| "BackTo" natural "."
 | test_show_goal "Show" "Goal" natural "at" natural "."
+| "Show" "Proof" "Diffs" OPT "removed" "."
 | Pvernac.Vernac_.main_entry
 ]
 
@@ -560,7 +543,6 @@ command: [
 | "Reset" identref
 | "Back"
 | "Back" natural
-| "BackTo" natural
 | "Debug" "On"
 | "Debug" "Off"
 | "Declare" "Reduction" IDENT; ":=" red_expr
@@ -669,14 +651,27 @@ command: [
 | "Show" "Ltac" "Profile"
 | "Show" "Ltac" "Profile" "CutOff" int
 | "Show" "Ltac" "Profile" string
+| "Add" "InjTyp" constr      (* micromega plugin *)
+| "Add" "BinOp" constr      (* micromega plugin *)
+| "Add" "UnOp" constr      (* micromega plugin *)
+| "Add" "CstOp" constr      (* micromega plugin *)
+| "Add" "BinRel" constr      (* micromega plugin *)
+| "Add" "PropOp" constr      (* micromega plugin *)
+| "Add" "PropUOp" constr      (* micromega plugin *)
+| "Add" "Spec" constr      (* micromega plugin *)
+| "Add" "BinOpSpec" constr      (* micromega plugin *)
+| "Add" "UnOpSpec" constr      (* micromega plugin *)
+| "Add" "Saturate" constr      (* micromega plugin *)
+| "Show" "Zify" "InjTyp"      (* micromega plugin *)
+| "Show" "Zify" "BinOp"      (* micromega plugin *)
+| "Show" "Zify" "UnOp"      (* micromega plugin *)
+| "Show" "Zify" "CstOp"      (* micromega plugin *)
+| "Show" "Zify" "BinRel"      (* micromega plugin *)
+| "Show" "Zify" "Spec"      (* micromega plugin *)
 | "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
 ]
@@ -803,6 +798,7 @@ register_token: [
 
 register_type_token: [
 | "#int63_type"
+| "#float64_type"
 ]
 
 register_prim_token: [
@@ -830,6 +826,24 @@ register_prim_token: [
 | "#int63_lt"
 | "#int63_le"
 | "#int63_compare"
+| "#float64_opp"
+| "#float64_abs"
+| "#float64_eq"
+| "#float64_lt"
+| "#float64_le"
+| "#float64_compare"
+| "#float64_classify"
+| "#float64_add"
+| "#float64_sub"
+| "#float64_mul"
+| "#float64_div"
+| "#float64_sqrt"
+| "#float64_of_int63"
+| "#float64_normfr_mantissa"
+| "#float64_frshiftexp"
+| "#float64_ldshiftexp"
+| "#float64_next_up"
+| "#float64_next_down"
 ]
 
 thm_token: [
@@ -949,11 +963,16 @@ opt_coercion: [
 ]
 
 rec_definition: [
-| ident_decl binders_fixannot type_cstr OPT [ ":=" lconstr ] decl_notation
+| ident_decl binders_fixannot rec_type_cstr OPT [ ":=" lconstr ] decl_notation
 ]
 
 corec_definition: [
-| ident_decl binders type_cstr OPT [ ":=" lconstr ] decl_notation
+| ident_decl binders rec_type_cstr OPT [ ":=" lconstr ] decl_notation
+]
+
+rec_type_cstr: [
+| ":" lconstr
+|
 ]
 
 scheme: [
@@ -973,6 +992,13 @@ record_field: [
 | LIST0 quoted_attributes record_binder OPT [ "|" natural ] decl_notation
 ]
 
+record_fields: [
+| record_field ";" record_fields
+| record_field ";"
+| record_field
+|
+]
+
 record_binder_body: [
 | binders of_type_with_opt_coercion lconstr
 | binders of_type_with_opt_coercion lconstr ":=" lconstr
@@ -1048,7 +1074,6 @@ gallina_ext: [
 | "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: [
@@ -1175,21 +1200,21 @@ arguments_modifier: [
 | "clear" "implicits" "and" "scopes"
 ]
 
-scope: [
+scope_delimiter: [
 | "%" IDENT
 ]
 
 argument_spec: [
-| OPT "!" name OPT scope
+| OPT "!" name OPT scope_delimiter
 ]
 
 argument_spec_block: [
 | argument_spec
 | "/"
 | "&"
-| "(" LIST1 argument_spec ")" OPT scope
-| "[" LIST1 argument_spec "]" OPT scope
-| "{" LIST1 argument_spec "}" OPT scope
+| "(" LIST1 argument_spec ")" OPT scope_delimiter
+| "[" LIST1 argument_spec "]" OPT scope_delimiter
+| "{" LIST1 argument_spec "}" OPT scope_delimiter
 ]
 
 more_implicits_block: [
@@ -1260,6 +1285,7 @@ printable: [
 | "Coercions"
 | "Coercion" "Paths" class_rawexpr class_rawexpr
 | "Canonical" "Projections"
+| "Typing" "Flags"
 | "Tables"
 | "Options"
 | "Hint"
@@ -1339,7 +1365,7 @@ positive_search_mark: [
 ]
 
 searchabout_query: [
-| positive_search_mark ne_string OPT scope
+| positive_search_mark ne_string OPT scope_delimiter
 | positive_search_mark constr_pattern
 ]
 
@@ -1725,6 +1751,9 @@ simple_tactic: [
 | "psatz_R" tactic      (* micromega plugin *)
 | "psatz_Q" int_or_var tactic      (* micromega plugin *)
 | "psatz_Q" tactic      (* micromega plugin *)
+| "iter_specs" tactic      (* micromega plugin *)
+| "zify_op"      (* micromega plugin *)
+| "saturate"      (* micromega plugin *)
 | "nsatz_compute" constr      (* nsatz plugin *)
 | "omega"      (* omega plugin *)
 | "omega" "with" LIST1 ident      (* omega plugin *)
@@ -1734,54 +1763,6 @@ simple_tactic: [
 | "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: [
@@ -1891,10 +1872,6 @@ test_lpar_id_colon: [
 | local_test_lpar_id_colon
 ]
 
-orient_string: [
-| orient preident
-]
-
 comparison: [
 | "="
 | "<"
@@ -1977,9 +1954,6 @@ tactic_expr4: [
 | 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: [
@@ -1996,10 +1970,6 @@ tactic_expr3: [
 | "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: [
@@ -2023,14 +1993,12 @@ tactic_expr1: [
 | 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: [
@@ -2422,8 +2390,6 @@ 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: [
@@ -2462,13 +2428,24 @@ in_hyp_as: [
 |
 ]
 
+orient_rw: [
+| "->"
+| "<-"
+|
+]
+
 simple_binder: [
 | name
 | "(" LIST1 name ":" lconstr ")"
 ]
 
 fixdecl: [
-| "(" ident LIST0 simple_binder fixannot ":" lconstr ")"
+| "(" ident LIST0 simple_binder struct_annot ":" lconstr ")"
+]
+
+struct_annot: [
+| "{" "struct" name "}"
+|
 ]
 
 cofixdecl: [
@@ -2525,7 +2502,7 @@ rewriter: [
 ]
 
 oriented_rewriter: [
-| orient rewriter
+| orient_rw rewriter
 ]
 
 induction_clause: [
@@ -2564,608 +2541,6 @@ 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 ")"
diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar
index cd6e11505c..545ccde03a 100644
--- a/doc/tools/docgram/orderedGrammar
+++ b/doc/tools/docgram/orderedGrammar
@@ -3,603 +3,541 @@ 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"
+vernac_toplevel: [
+| "Drop" "."
+| "Quit" "."
+| "BackTo" num "."
+| "Show" "Goal" num "at" num "."
+| "Show" "Proof" "Diffs" removed_opt "."
+| vernac_control
 ]
 
-universe_increment: [
-| "+" natural
+removed_opt: [
+| "removed"
 | empty
 ]
 
-universe_name: [
-| global
-| "Set"
-| "Prop"
+tactic_mode: [
+| toplevel_selector_opt query_command
+| toplevel_selector_opt "{"
+| toplevel_selector_opt ltac_info_opt ltac_expr ltac_use_default
+| "par" ":" ltac_info_opt ltac_expr ltac_use_default
 ]
 
-universe_expr: [
-| universe_name universe_increment
+toplevel_selector_opt: [
+| toplevel_selector
+| empty
 ]
 
-universe: [
-| "max" "(" universe_expr_list_comma ")"
-| universe_expr
+ltac_info_opt: [
+| "Info" num
+| empty
 ]
 
-universe_expr_list_comma: [
-| universe_expr_list_comma "," universe_expr
-| universe_expr
+ltac_use_default: [
+| "."
+| "..."
 ]
 
-lconstr: [
-| operconstr200
-| lconstr
+vernac_control: [
+| "Time" vernac_control
+| "Redirect" string vernac_control
+| "Timeout" num vernac_control
+| "Fail" vernac_control
+| quoted_attributes_list_opt vernac
 ]
 
 term: [
-| operconstr8
-| "@" global instance
+| "forall" open_binders "," term
+| "fun" open_binders "=>" term
+| term_let
+| "if" term as_return_type_opt "then" term "else" term
+| term_fix
+| term100
 ]
 
-operconstr200: [
-| binder_constr
-| operconstr100
+term100: [
+| term_cast
+| term10
 ]
 
-operconstr100: [
-| operconstr99 "<:" binder_constr
-| operconstr99 "<:" operconstr100
-| operconstr99 "<<:" binder_constr
-| operconstr99 "<<:" operconstr100
-| operconstr99 ":" binder_constr
-| operconstr99 ":" operconstr100
-| operconstr99 ":>"
-| operconstr99
+term10: [
+| term1 args
+| "@" qualid universe_annot_opt term1_list_opt
+| term1
 ]
 
-operconstr99: [
-| operconstr90
+args: [
+| args arg
+| arg
 ]
 
-operconstr90: [
-| operconstr10
+arg: [
+| "(" ident ":=" term ")"
+| term1
 ]
 
-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
+term1_list_opt: [
+| term1_list_opt term1
+| empty
 ]
 
-operconstr1: [
-| operconstr0 ".(" global appl_arg_list_opt ")"
-| operconstr0 ".(" "@" global operconstr9_list_opt ")"
-| operconstr0 "%" IDENT
-| operconstr0
+empty: [
+|
 ]
 
-appl_arg_list_opt: [
-| appl_arg_list_opt appl_arg
-| empty
+term1: [
+| term_projection
+| term0 "%" ident
+| term0
 ]
 
-operconstr9_list_opt: [
-| operconstr9_list_opt operconstr9
+args_opt: [
+| args
 | empty
 ]
 
-operconstr0: [
-| atomic_constr
-| match_constr
-| "(" operconstr200 ")"
-| "{|" record_declaration bar_cbrace
-| "{" binder_constr "}"
-| "`{" operconstr200 "}"
-| "`(" operconstr200 ")"
+term0: [
+| qualid universe_annot_opt
+| sort
+| numeral
+| string
+| "_"
+| term_evar
+| term_match
+| "(" term ")"
+| "{|" fields_def "|}"
+| "`{" term "}"
+| "`(" term ")"
 | "ltac" ":" "(" ltac_expr ")"
 ]
 
-record_declaration: [
-| record_fields
-]
-
-record_fields: [
-| record_field_declaration ";" record_fields
-| record_field_declaration
+fields_def: [
+| field_def ";" fields_def
+| field_def
 | 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 *)
+field_def: [
+| qualid binders_opt ":=" term
 ]
 
-name_alt: [
-| "(" name_list_comma_opt ")"
-| "()"
+binders_opt: [
+| binders
+| empty
 ]
 
-name_list_comma_opt: [
-| name_list_comma
-| empty
+term_projection: [
+| term0 ".(" qualid args_opt ")"
+| term0 ".(" "@" qualid term1_list_opt ")"
 ]
 
-name_list_comma: [
-| name_list_comma "," name
-| name
+term_evar: [
+| "?[" ident "]"
+| "?[" "?" ident "]"
+| "?" ident evar_bindings_opt
 ]
 
-name_list_opt: [
-| name_list_opt name
+evar_bindings_opt: [
+| "@{" evar_bindings_semi "}"
 | empty
 ]
 
-name_list: [
-| name_list name
-| name
+evar_bindings_semi: [
+| evar_bindings_semi ";" evar_binding
+| evar_binding
 ]
 
-appl_arg: [
-| lpar_id_coloneq lconstr ")"
-| operconstr9
+evar_binding: [
+| ident ":=" term
 ]
 
-atomic_constr: [
-| global instance
-| sort
-| NUMERAL
-| string
-| "_"
-| "?" "[" ident "]"
-| "?" "[" "?" ident "]"
-| "?" ident evar_instance
+dangling_pattern_extension_rule: [
+| "@" "?" ident ident_list
 ]
 
-inst: [
-| ident ":=" lconstr
+ident_list: [
+| ident_list ident
+| ident
 ]
 
-evar_instance: [
-| "@{" inst_list_semi "}"
+record_fields: [
+| record_field ";" record_fields
+| record_field ";"
+| record_field
 | empty
 ]
 
-inst_list_semi: [
-| inst_list_semi ";" inst
-| inst
-]
-
-instance: [
-| "@{" universe_level_list_opt "}"
-| empty
+record_field: [
+| quoted_attributes_list_opt record_binder num_opt2 decl_notation
 ]
 
-universe_level_list_opt: [
-| universe_level_list_opt universe_level
+decl_notation: [
+| "where" one_decl_notation_list
 | 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
+one_decl_notation_list: [
+| one_decl_notation_list "and" one_decl_notation
+| one_decl_notation
 ]
 
-single_fix: [
-| fix_kw fix_decl
+one_decl_notation: [
+| string ":=" term1_extended ident_opt3
 ]
 
-fix_kw: [
-| "fix"
-| "cofix"
+ident_opt3: [
+| ":" ident
+| empty
 ]
 
-fix_decl: [
-| ident binders_fixannot type_cstr ":=" operconstr200
+record_binder: [
+| name
+| name record_binder_body
 ]
 
-match_constr: [
-| "match" case_item_list_comma case_type_opt "with" branches "end"
+record_binder_body: [
+| binders_opt of_type_with_opt_coercion term
+| binders_opt of_type_with_opt_coercion term ":=" term
+| binders_opt ":=" term
 ]
 
-case_item_list_comma: [
-| case_item_list_comma "," case_item
-| case_item
+of_type_with_opt_coercion: [
+| ":>>"
+| ":>"
+| ":"
 ]
 
-case_type_opt: [
-| case_type
+num_opt2: [
+| "|" num
 | empty
 ]
 
-case_item: [
-| operconstr100 as_opt in_opt
-]
-
-as_opt2: [
-| as_opt case_type
+quoted_attributes_list_opt: [
+| quoted_attributes_list_opt "#[" attribute_list_comma_opt "]"
 | empty
 ]
 
-in_opt: [
-| "in" pattern200
+attribute_list_comma_opt: [
+| attribute_list_comma
 | empty
 ]
 
-case_type: [
-| "return" operconstr100
+attribute_list_comma: [
+| attribute_list_comma "," attribute
+| attribute
 ]
 
-return_type: [
-| as_opt2
+attribute: [
+| ident attribute_value
 ]
 
-as_opt3: [
-| "as" dirpath
+attribute_value: [
+| "=" string
+| "(" attribute_list_comma_opt ")"
 | empty
 ]
 
-branches: [
-| or_opt eqn_list_or_opt
-]
-
-mult_pattern: [
-| pattern200_list_comma
-]
-
-pattern200_list_comma: [
-| pattern200_list_comma "," pattern200
-| pattern200
+qualid: [
+| qualid field
+| ident
 ]
 
-eqn: [
-| mult_pattern_list_or "=>" lconstr
+field: [
+| "." ident
 ]
 
-mult_pattern_list_or: [
-| mult_pattern_list_or "|" mult_pattern
-| mult_pattern
+sort: [
+| "Set"
+| "Prop"
+| "SProp"
+| "Type"
+| "Type" "@{" "_" "}"
+| "Type" "@{" universe "}"
 ]
 
-record_pattern: [
-| global ":=" pattern200
+universe: [
+| "max" "(" universe_exprs_comma ")"
+| universe_expr
 ]
 
-record_patterns: [
-| record_pattern ";" record_patterns
-| record_pattern ";"
-| record_pattern
-| empty
+universe_exprs_comma: [
+| universe_exprs_comma "," universe_expr
+| universe_expr
 ]
 
-pattern200: [
-| pattern100
+universe_expr: [
+| universe_name universe_increment_opt
 ]
 
-pattern100: [
-| pattern99 ":" binder_constr
-| pattern99 ":" operconstr100
-| pattern99
+universe_name: [
+| qualid
+| "Set"
+| "Prop"
 ]
 
-pattern99: [
-| pattern90
+universe_increment_opt: [
+| "+" num
+| empty
 ]
 
-pattern90: [
-| pattern10
+universe_annot_opt: [
+| "@{" universe_levels_opt "}"
+| empty
 ]
 
-pattern10: [
-| pattern1 "as" name
-| pattern1 pattern1_list
-| "@" reference pattern1_list_opt
-| pattern1
+universe_levels_opt: [
+| universe_levels_opt universe_level
+| empty
 ]
 
-pattern1_list: [
-| pattern1_list pattern1
-| pattern1
+universe_level: [
+| "Set"
+| "Prop"
+| "Type"
+| "_"
+| qualid
 ]
 
-pattern1_list_opt: [
-| pattern1_list_opt pattern1
-| empty
+term_fix: [
+| single_fix
+| single_fix "with" fix_bodies "for" ident
 ]
 
-pattern1: [
-| pattern0 "%" IDENT
-| pattern0
+single_fix: [
+| "fix" fix_body
+| "cofix" fix_body
 ]
 
-pattern0: [
-| reference
-| "{|" record_patterns bar_cbrace
-| "_"
-| "(" pattern200 ")"
-| "(" pattern200 "|" pattern200_list_or ")"
-| NUMERAL
-| string
+fix_bodies: [
+| fix_bodies "with" fix_body
+| fix_body
 ]
 
-pattern200_list_or: [
-| pattern200_list_or "|" pattern200
-| pattern200
+fix_body: [
+| ident binders_opt fixannot_opt colon_term_opt ":=" term
 ]
 
-impl_ident_tail: [
-| "}"
-| name_list ":" lconstr "}"
-| name_list "}"
-| ":" lconstr "}"
+fixannot_opt: [
+| fixannot
+| empty
 ]
 
 fixannot: [
 | "{" "struct" ident "}"
-| "{" "wf" term ident "}"
-| "{" "measure" term ident_opt term_opt "}"
-| "{" "struct" name "}"
-| empty
+| "{" "wf" term1_extended ident "}"
+| "{" "measure" term1_extended ident_opt term1_extended_opt "}"
 ]
 
-term_opt: [
-| term
-| empty
+term1_extended: [
+| term1
+| "@" qualid universe_annot_opt
 ]
 
-impl_name_head: [
+ident_opt: [
+| ident
 | empty
 ]
 
-binders_fixannot: [
-| impl_name_head impl_ident_tail binders_fixannot
-| fixannot
-| binder binders_fixannot
+term1_extended_opt: [
+| term1_extended
 | empty
 ]
 
-open_binders: [
-| name name_list_opt ":" lconstr
-| name name_list_opt binders
-| name ".." name
-| closed_binder binders
-]
-
-binders: [
-| binder_list_opt
+term_let: [
+| "let" name colon_term_opt ":=" term "in" term
+| "let" name binders colon_term_opt ":=" term "in" term
+| "let" single_fix "in" term
+| "let" names_tuple as_return_type_opt ":=" term "in" term
+| "let" "'" pattern ":=" term return_type_opt "in" term
+| "let" "'" pattern "in" pattern ":=" term return_type "in" term
 ]
 
-binder_list_opt: [
-| binder_list_opt binder
+colon_term_opt: [
+| ":" term
 | empty
 ]
 
-binder: [
-| name
-| closed_binder
+names_tuple: [
+| "(" names_comma ")"
+| "()"
 ]
 
-typeclass_constraint: [
-| "!" operconstr200
-| "{" name "}" ":" exclam_opt operconstr200
-| name_colon exclam_opt operconstr200
-| operconstr200
+names_comma: [
+| names_comma "," name
+| name
 ]
 
-type_cstr: [
-| lconstr_opt
-| ":" lconstr
-| empty
+open_binders: [
+| names ":" term
+| binders
 ]
 
-preident: [
-| IDENT
+names: [
+| names name
+| name
 ]
 
-pattern_identref: [
-| "?" ident
+name: [
+| "_"
+| ident
 ]
 
-var: [
-| ident
+binders: [
+| binders binder
+| binder
 ]
 
-field: [
-| FIELD
+binder: [
+| name
+| "(" names ":" term ")"
+| "(" name colon_term_opt ":=" term ")"
+| "{" name "}"
+| "{" names colon_term_opt "}"
+| "`(" typeclass_constraints_comma ")"
+| "`{" typeclass_constraints_comma "}"
+| "'" pattern0
+| "(" name ":" term "|" term ")"
 ]
 
-fields: [
-| field fields
-| field
+typeclass_constraints_comma: [
+| typeclass_constraints_comma "," typeclass_constraint
+| typeclass_constraint
 ]
 
-fullyqualid: [
-| ident fields
-| ident
+typeclass_constraint: [
+| exclam_opt term
+| "{" name "}" ":" exclam_opt term
+| name ":" exclam_opt term
 ]
 
-basequalid: [
-| ident fields
-| ident
+exclam_opt: [
+| "!"
+| empty
 ]
 
-name: [
-| "_"
-| ident
+term_cast: [
+| term10 "<:" term
+| term10 "<<:" term
+| term10 ":" term
+| term10 ":>"
 ]
 
-reference: [
-| ident fields
-| ident
+term_match: [
+| "match" case_items_comma return_type_opt "with" or_opt eqns_or_opt "end"
 ]
 
-by_notation: [
-| ne_string IDENT_opt
+case_items_comma: [
+| case_items_comma "," case_item
+| case_item
 ]
 
-IDENT_opt: [
-| "%" IDENT
+return_type_opt: [
+| return_type
 | empty
 ]
 
-smart_global: [
-| reference
-| by_notation
+as_return_type_opt: [
+| as_name_opt return_type
+| empty
 ]
 
-qualid: [
-| basequalid
+return_type: [
+| "return" term100
 ]
 
-ne_string: [
-| STRING
+case_item: [
+| term100 as_name_opt in_opt
 ]
 
-ne_lstring: [
-| ne_string
+as_name_opt: [
+| "as" name
+| empty
 ]
 
-dirpath: [
-| ident field_list_opt
+in_opt: [
+| "in" pattern
+| empty
 ]
 
-field_list_opt: [
-| field_list_opt field
+or_opt: [
+| "|"
 | empty
 ]
 
-string: [
-| STRING
+eqns_or_opt: [
+| eqns_or
+| empty
 ]
 
-lstring: [
-| string
+eqns_or: [
+| eqns_or "|" eqn
+| eqn
 ]
 
-integer: [
-| NUMERAL
-| "-" NUMERAL
+eqn: [
+| patterns_comma_list_or "=>" term
 ]
 
-natural: [
-| NUMERAL
+patterns_comma_list_or: [
+| patterns_comma_list_or "|" patterns_comma
+| patterns_comma
 ]
 
-bigint: [
-| NUMERAL
+patterns_comma: [
+| patterns_comma "," pattern
+| pattern
 ]
 
-bar_cbrace: [
-| "|" "}"
+pattern: [
+| pattern10 ":" term
+| pattern10
 ]
 
-vernac_control: [
-| "Time" vernac_control
-| "Redirect" ne_string vernac_control
-| "Timeout" natural vernac_control
-| "Fail" vernac_control
-| decorated_vernac
+pattern10: [
+| pattern1 "as" name
+| pattern1_list
+| "@" qualid pattern1_list_opt
+| pattern1
 ]
 
-decorated_vernac: [
-| quoted_attributes_list_opt vernac
+pattern1_list: [
+| pattern1_list pattern1
+| pattern1
 ]
 
-quoted_attributes_list_opt: [
-| quoted_attributes_list_opt quoted_attributes
+pattern1_list_opt: [
+| pattern1_list
 | empty
 ]
 
-quoted_attributes: [
-| "#[" attribute_list_comma_opt "]"
+pattern1: [
+| pattern0 "%" ident
+| pattern0
 ]
 
-attribute_list_comma_opt: [
-| attribute_list_comma
-| empty
+pattern0: [
+| qualid
+| "{|" record_patterns_opt "|}"
+| "_"
+| "(" patterns_or ")"
+| numeral
+| string
 ]
 
-attribute_list_comma: [
-| attribute_list_comma "," attribute
-| attribute
+patterns_or: [
+| patterns_or "|" pattern
+| pattern
 ]
 
-attribute: [
-| ident attribute_value
+record_patterns_opt: [
+| record_patterns_opt ";" record_pattern
+| record_pattern
+| empty
 ]
 
-attribute_value: [
-| "=" string
-| "(" attribute_list_comma_opt ")"
-| empty
+record_pattern: [
+| qualid ":=" pattern
 ]
 
 vernac: [
@@ -620,44 +558,51 @@ vernac_aux: [
 | gallina "."
 | gallina_ext "."
 | command "."
+| tactic_mode "."
 | syntax "."
 | subprf
-| command_entry
-]
-
-noedit_mode: [
 | query_command
 ]
 
 subprf: [
-| BULLET
+| bullet
 | "{"
 | "}"
 ]
 
 gallina: [
-| thm_token ident_decl binders ":" lconstr with_list_opt
+| thm_token ident_decl binders_opt ":" term 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
+| "Fixpoint" fix_definition_list
+| "Let" "Fixpoint" fix_definition_list
+| "CoFixpoint" cofix_definition_list
+| "Let" "CoFixpoint" cofix_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
+| "Register" qualid "as" qualid
+| "Register" "Inline" qualid
+| "Primitive" ident term_opt ":=" register_token
 | "Universe" ident_list
 | "Universes" ident_list
 | "Constraint" univ_constraint_list_comma
 ]
 
+term_opt: [
+| ":" term
+| empty
+]
+
+univ_constraint_list_comma: [
+| univ_constraint_list_comma "," univ_constraint
+| univ_constraint
+]
+
 with_list_opt: [
-| with_list_opt "with" ident_decl binders ":" lconstr
+| with_list_opt "with" ident_decl binders_opt ":" term
 | empty
 ]
 
@@ -671,14 +616,23 @@ inductive_definition_list: [
 | inductive_definition
 ]
 
-rec_definition_list: [
-| rec_definition_list "with" rec_definition
-| rec_definition
+fix_definition_list: [
+| fix_definition_list "with" fix_definition
+| fix_definition
 ]
 
-corec_definition_list: [
-| corec_definition_list "with" corec_definition
-| corec_definition
+fix_definition: [
+| ident_decl binders_opt fixannot_opt colon_term_opt term_opt2 decl_notation
+]
+
+term_opt2: [
+| ":=" term
+| empty
+]
+
+cofix_definition_list: [
+| cofix_definition_list "with" cofix_definition
+| cofix_definition
 ]
 
 scheme_list: [
@@ -691,23 +645,10 @@ ident_list_comma: [
 | 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"
+| "#float64_type"
 ]
 
 register_prim_token: [
@@ -735,6 +676,24 @@ register_prim_token: [
 | "#int63_lt"
 | "#int63_le"
 | "#int63_compare"
+| "#float64_opp"
+| "#float64_abs"
+| "#float64_eq"
+| "#float64_lt"
+| "#float64_le"
+| "#float64_compare"
+| "#float64_classify"
+| "#float64_add"
+| "#float64_sub"
+| "#float64_mul"
+| "#float64_div"
+| "#float64_sqrt"
+| "#float64_of_int63"
+| "#float64_normfr_mantissa"
+| "#float64_frshiftexp"
+| "#float64_ldshiftexp"
+| "#float64_next_up"
+| "#float64_next_down"
 ]
 
 thm_token: [
@@ -770,7 +729,7 @@ assumptions_token: [
 ]
 
 inline: [
-| "Inline" "(" natural ")"
+| "Inline" "(" num ")"
 | "Inline"
 | empty
 ]
@@ -785,30 +744,6 @@ 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
 ]
@@ -833,9 +768,9 @@ private_token: [
 ]
 
 def_body: [
-| binders ":=" reduce lconstr
-| binders ":" lconstr ":=" reduce lconstr
-| binders ":" lconstr
+| binders_opt ":=" reduce term
+| binders_opt ":" term ":=" reduce term
+| binders_opt ":" term
 ]
 
 reduce: [
@@ -843,27 +778,70 @@ reduce: [
 | empty
 ]
 
-one_decl_notation: [
-| ne_lstring ":=" term IDENT_opt2
+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" term1_extended_list
+| "pattern" pattern_occ_list_comma
+| ident
 ]
 
-IDENT_opt2: [
-| ":" IDENT
-| empty
+strategy_flag: [
+| red_flags_list
+| delta_flag
+]
+
+red_flags_list: [
+| red_flags_list red_flags
+| red_flags
 ]
 
-decl_sep: [
-| "and"
+red_flags: [
+| "beta"
+| "iota"
+| "match"
+| "fix"
+| "cofix"
+| "zeta"
+| "delta" delta_flag
 ]
 
-decl_notation: [
-| "where" one_decl_notation_list
+delta_flag: [
+| "-" "[" smart_global_list "]"
+| "[" smart_global_list "]"
 | empty
 ]
 
-one_decl_notation_list: [
-| one_decl_notation_list decl_sep one_decl_notation
-| one_decl_notation
+ref_or_pattern_occ_opt: [
+| ref_or_pattern_occ
+| empty
+]
+
+ref_or_pattern_occ: [
+| smart_global occs
+| term1_extended occs
+]
+
+unfold_occ_list_comma: [
+| unfold_occ_list_comma "," unfold_occ
+| unfold_occ
+]
+
+unfold_occ: [
+| smart_global occs
+]
+
+pattern_occ_list_comma: [
+| pattern_occ_list_comma "," pattern_occ
+| pattern_occ
 ]
 
 opt_constructors_or_fields: [
@@ -872,7 +850,12 @@ opt_constructors_or_fields: [
 ]
 
 inductive_definition: [
-| opt_coercion ident_decl binders lconstr_opt opt_constructors_or_fields decl_notation
+| opt_coercion ident_decl binders_opt term_opt opt_constructors_or_fields decl_notation
+]
+
+opt_coercion: [
+| ">"
+| empty
 ]
 
 constructor_list_or_record_decl: [
@@ -894,52 +877,6 @@ constructor_list_or_opt: [
 | 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
@@ -955,7 +892,7 @@ assum_coe: [
 ]
 
 simple_assum_coe: [
-| ident_decl_list of_type_with_opt_coercion lconstr
+| ident_decl_list of_type_with_opt_coercion term
 ]
 
 ident_decl_list: [
@@ -964,11 +901,11 @@ ident_decl_list: [
 ]
 
 constructor_type: [
-| binders of_type_with_opt_coercion_opt
+| binders_opt of_type_with_opt_coercion_opt
 ]
 
 of_type_with_opt_coercion_opt: [
-| of_type_with_opt_coercion lconstr
+| of_type_with_opt_coercion term
 | empty
 ]
 
@@ -976,95 +913,135 @@ constructor: [
 | ident constructor_type
 ]
 
-of_type_with_opt_coercion: [
-| ":>>"
-| ":>" ">"
-| ":>"
-| ":" ">" ">"
-| ":" ">"
-| ":"
+cofix_definition: [
+| ident_decl binders_opt colon_term_opt term_opt2 decl_notation
+]
+
+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
+]
+
+sort_family: [
+| "Set"
+| "Prop"
+| "SProp"
+| "Type"
+]
+
+smart_global: [
+| qualid
+| by_notation
+]
+
+by_notation: [
+| string ident_opt2
+]
+
+ident_opt2: [
+| "%" ident
+| empty
 ]
 
 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
+| "Module" "Type" ident module_binder_list_opt module_type_inl_list_opt 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
+| "Require" export_token qualid_list
+| "From" qualid "Require" export_token qualid_list
+| "Import" qualid_list
+| "Export" qualid_list
+| "Include" module_type_inl module_expr_inl_list_opt
+| "Include" "Type" module_type_inl module_type_inl_list_opt
 | "Transparent" smart_global_list
 | "Opaque" smart_global_list
 | "Strategy" strategy_level_list
-| "Canonical" Structure_opt global univ_decl_opt2
+| "Canonical" Structure_opt qualid univ_decl_opt2
 | "Canonical" Structure_opt by_notation
-| "Coercion" global univ_decl_opt def_body
+| "Coercion" qualid univ_decl_opt def_body
 | "Identity" "Coercion" ident ":" class_rawexpr ">->" class_rawexpr
-| "Coercion" global ":" class_rawexpr ">->" class_rawexpr
+| "Coercion" qualid ":" 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
+| "Context" binders
+| "Instance" instance_name ":" term hint_info fields_def_opt
+| "Existing" "Instance" qualid hint_info
+| "Existing" "Instances" qualid_list num_opt2
+| "Existing" "Class" qualid
 | "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 *)
+| "Export" "Set" ident_list option_setting
+| "Export" "Unset" ident_list
 ]
 
-module_binder_list_opt: [
-| module_binder_list_opt module_binder
-| empty
+smart_global_list: [
+| smart_global_list smart_global
+| smart_global
 ]
 
-ext_module_expr_list_opt: [
-| ext_module_expr_list_opt ext_module_expr
+num_opt: [
+| num
 | empty
 ]
 
-ext_module_type_list_opt: [
-| ext_module_type_list_opt ext_module_type
+qualid_list: [
+| qualid_list qualid
+| qualid
+]
+
+option_setting: [
 | empty
+| int
+| string
 ]
 
-strategy_level_list: [
-| strategy_level_list strategy_level "[" smart_global_list "]"
-| strategy_level "[" smart_global_list "]"
+class_rawexpr: [
+| "Funclass"
+| "Sortclass"
+| smart_global
 ]
 
-Structure_opt: [
-| "Structure"
+hint_info: [
+| "|" num_opt term1_extended_opt
 | empty
 ]
 
-univ_decl_opt: [
-| univ_decl
+module_binder_list_opt: [
+| module_binder_list_opt "(" export_token ident_list ":" module_type_inl ")"
 | empty
 ]
 
-binder_list: [
-| binder_list binder
-| binder
+module_type_inl_list_opt: [
+| module_type_inl_list_opt module_type_inl
+| empty
 ]
 
-record_declaration_opt: [
-| ":=" "{" record_declaration "}"
-| ":=" lconstr
+module_expr_inl_list_opt: [
+| module_expr_inl_list_opt module_expr_inl
 | empty
 ]
 
-natural_opt: [
-| natural
+strategy_level_list: [
+| strategy_level_list strategy_level "[" smart_global_list "]"
+| strategy_level "[" smart_global_list "]"
+]
+
+fields_def_opt: [
+| ":=" "{" fields_def "}"
+| ":=" term
 | empty
 ]
 
@@ -1114,50 +1091,54 @@ univ_decl_opt2: [
 | empty
 ]
 
-export_token: [
-| "Import"
-| "Export"
+univ_decl_opt: [
+| "@{" ident_list_opt plus_opt univ_constraint_alt
 | empty
 ]
 
-ext_module_type: [
-| "<+" module_type_inl
+plus_opt: [
+| "+"
+| empty
 ]
 
-ext_module_expr: [
-| "<+" module_expr_inl
+univ_constraint_alt: [
+| "|" univ_constraint_list_comma_opt plus_opt "}"
+| rbrace_alt
 ]
 
-check_module_type: [
-| "<:" module_type_inl
+univ_constraint_list_comma_opt: [
+| univ_constraint_list_comma
+| empty
 ]
 
-check_module_types: [
-| check_module_type_list_opt
+rbrace_alt: [
+| "}"
+| "|}"
 ]
 
-check_module_type_list_opt: [
-| check_module_type_list_opt check_module_type
+export_token: [
+| "Import"
+| "Export"
 | empty
 ]
 
 of_module_type: [
 | ":" module_type_inl
-| check_module_types
+| module_type_inl_list_opt
 ]
 
 is_module_type: [
-| ":=" module_type_inl ext_module_type_list_opt
+| ":=" module_type_inl module_type_inl_list_opt
 | empty
 ]
 
 is_module_expr: [
-| ":=" module_expr_inl ext_module_expr_list_opt
+| ":=" module_expr_inl module_expr_inl_list_opt
 | empty
 ]
 
 functor_app_annot: [
-| "[" "inline" "at" "level" natural "]"
+| "[" "inline" "at" "level" num "]"
 | "[" "no" "inline" "]"
 | empty
 ]
@@ -1172,10 +1153,6 @@ module_type_inl: [
 | module_type functor_app_annot
 ]
 
-module_binder: [
-| "(" export_token ident_list ":" module_type_inl ")"
-]
-
 module_expr: [
 | module_expr_atom
 | module_expr module_expr_atom
@@ -1186,11 +1163,6 @@ module_expr_atom: [
 | "(" module_expr ")"
 ]
 
-with_declaration: [
-| "Definition" fullyqualid univ_decl_opt ":=" lconstr
-| "Module" fullyqualid ":=" qualid
-]
-
 module_type: [
 | qualid
 | "(" module_type ")"
@@ -1198,108 +1170,45 @@ module_type: [
 | 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
+with_declaration: [
+| "Definition" qualid univ_decl_opt ":=" term
+| "Module" qualid ":=" qualid
 ]
 
 argument_spec_block: [
-| argument_spec
+| exclam_opt name scope_delimiter_opt
 | "/"
 | "&"
-| "(" argument_spec_list ")" scope_opt
-| "[" argument_spec_list "]" scope_opt
-| "{" argument_spec_list "}" scope_opt
+| "(" scope_delimiter_list ")" scope_delimiter_opt
+| "[" scope_delimiter_list "]" scope_delimiter_opt
+| "{" scope_delimiter_list "}" scope_delimiter_opt
+]
+
+scope_delimiter_opt: [
+| "%" ident
+| empty
 ]
 
-argument_spec_list: [
-| argument_spec_list argument_spec
-| argument_spec
+scope_delimiter_list: [
+| scope_delimiter_list scope_delimiter_opt
+| scope_delimiter_opt
 ]
 
 more_implicits_block: [
 | name
-| "[" name_list "]"
-| "{" name_list "}"
+| "[" names "]"
+| "{" names "}"
 ]
 
 strategy_level: [
 | "expand"
 | "opaque"
-| integer
+| int
 | "transparent"
 ]
 
 instance_name: [
-| ident_decl binders
-| empty
-]
-
-hint_info: [
-| "|" natural_opt constr_pattern_opt
+| ident_decl binders_opt
 | empty
 ]
 
@@ -1318,64 +1227,83 @@ reserv_tuple: [
 ]
 
 simple_reserv: [
-| ident_list ":" lconstr
+| ident_list ":" term
+]
+
+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"
+]
+
+Structure_opt: [
+| "Structure"
+| empty
 ]
 
 command: [
+| "Goal" term
 | "Comments" comment_list_opt
-| "Declare" "Instance" ident_decl binders ":" operconstr200 hint_info
-| "Declare" "Scope" IDENT
+| "Declare" "Instance" ident_decl binders_opt ":" term hint_info
+| "Declare" "Scope" ident
 | "Pwd"
 | "Cd"
-| "Cd" ne_string
-| "Load" Verbose_opt ne_string_alt
-| "Declare" "ML" "Module" ne_string_list
+| "Cd" string
+| "Load" Verbose_opt string_alt
+| "Declare" "ML" "Module" 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
+| "Add" "LoadPath" string as_dirpath
+| "Add" "Rec" "LoadPath" string as_dirpath
+| "Remove" "LoadPath" string
+| "AddPath" string "as" as_dirpath
+| "AddRecPath" string "as" as_dirpath
+| "DelPath" string
+| "Type" term
 | "Print" printable
 | "Print" smart_global univ_name_list_opt
-| "Print" "Module" "Type" global
-| "Print" "Module" global
+| "Print" "Module" "Type" qualid
+| "Print" "Module" qualid
 | "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
+| "Inspect" num
+| "Add" "ML" "Path" string
+| "Add" "Rec" "ML" "Path" string
+| "Set" ident_list option_setting
+| "Unset" ident_list
+| "Print" "Table" ident_list
+| "Add" ident ident option_ref_value_list
+| "Add" ident option_ref_value_list
+| "Test" ident_list "for" option_ref_value_list
+| "Test" ident_list
+| "Remove" ident ident option_ref_value_list
+| "Remove" ident option_ref_value_list
+| "Write" "State" ident
+| "Write" "State" string
+| "Restore" "State" ident
+| "Restore" "State" string
 | "Reset" "Initial"
 | "Reset" ident
 | "Back"
-| "Back" natural
-| "BackTo" natural
+| "Back" num
 | "Debug" "On"
 | "Debug" "Off"
-| "Declare" "Reduction" IDENT; ":=" red_expr
-| "Declare" "Custom" "Entry" IDENT
-| "Goal" lconstr
+| "Declare" "Reduction" ident ":=" red_expr
+| "Declare" "Custom" "Entry" ident
+| "Derive" ident "SuchThat" term1_extended "As" ident      (* derive plugin *)
 | "Proof"
 | "Proof" "Mode" string
-| "Proof" lconstr
+| "Proof" term
 | "Abort"
 | "Abort" "All"
 | "Abort" ident
-| "Existential" natural constr_body
+| "Existential" num constr_body
 | "Admitted"
 | "Qed"
 | "Save" ident
@@ -1383,14 +1311,14 @@ command: [
 | "Defined" ident
 | "Restart"
 | "Undo"
-| "Undo" natural
-| "Undo" "To" natural
+| "Undo" num
+| "Undo" "To" num
 | "Focus"
-| "Focus" natural
+| "Focus" num
 | "Unfocus"
 | "Unfocused"
 | "Show"
-| "Show" natural
+| "Show" num
 | "Show" ident
 | "Show" "Existentials"
 | "Show" "Universes"
@@ -1398,47 +1326,57 @@ command: [
 | "Show" "Proof"
 | "Show" "Intro"
 | "Show" "Intros"
-| "Show" "Match" reference
+| "Show" "Match" qualid
 | "Guarded"
-| "Create" "HintDb" IDENT discriminated_opt
-| "Remove" "Hints" global_list opt_hintbases
+| "Create" "HintDb" ident discriminated_opt
+| "Remove" "Hints" qualid_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
+| "Obligation" int "of" ident ":" term withtac
+| "Obligation" int "of" ident withtac
+| "Obligation" int ":" term withtac
+| "Obligation" int 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" "Obligation" int "of" ident "with" ltac_expr
+| "Solve" "Obligation" int "with" ltac_expr
+| "Solve" "Obligations" "of" ident "with" ltac_expr
+| "Solve" "Obligations" "with" ltac_expr
 | "Solve" "Obligations"
-| "Solve" "All" "Obligations" "with" tactic
+| "Solve" "All" "Obligations" "with" ltac_expr
 | "Solve" "All" "Obligations"
 | "Admit" "Obligations" "of" ident
 | "Admit" "Obligations"
-| "Obligation" "Tactic" ":=" tactic
+| "Obligation" "Tactic" ":=" ltac_expr
 | "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
+| "Add" "Relation" term1_extended term1_extended "reflexivity" "proved" "by" term1_extended "symmetry" "proved" "by" term1_extended "as" ident
+| "Add" "Relation" term1_extended term1_extended "reflexivity" "proved" "by" term1_extended "as" ident
+| "Add" "Relation" term1_extended term1_extended "as" ident
+| "Add" "Relation" term1_extended term1_extended "symmetry" "proved" "by" term1_extended "as" ident
+| "Add" "Relation" term1_extended term1_extended "symmetry" "proved" "by" term1_extended "transitivity" "proved" "by" term1_extended "as" ident
+| "Add" "Relation" term1_extended term1_extended "reflexivity" "proved" "by" term1_extended "transitivity" "proved" "by" term1_extended "as" ident
+| "Add" "Relation" term1_extended term1_extended "reflexivity" "proved" "by" term1_extended "symmetry" "proved" "by" term1_extended "transitivity" "proved" "by" term1_extended "as" ident
+| "Add" "Relation" term1_extended term1_extended "transitivity" "proved" "by" term1_extended "as" ident
+| "Add" "Parametric" "Relation" binders_opt ":" term1_extended term1_extended "reflexivity" "proved" "by" term1_extended "symmetry" "proved" "by" term1_extended "as" ident
+| "Add" "Parametric" "Relation" binders_opt ":" term1_extended term1_extended "reflexivity" "proved" "by" term1_extended "as" ident
+| "Add" "Parametric" "Relation" binders_opt ":" term1_extended term1_extended "as" ident
+| "Add" "Parametric" "Relation" binders_opt ":" term1_extended term1_extended "symmetry" "proved" "by" term1_extended "as" ident
+| "Add" "Parametric" "Relation" binders_opt ":" term1_extended term1_extended "symmetry" "proved" "by" term1_extended "transitivity" "proved" "by" term1_extended "as" ident
+| "Add" "Parametric" "Relation" binders_opt ":" term1_extended term1_extended "reflexivity" "proved" "by" term1_extended "transitivity" "proved" "by" term1_extended "as" ident
+| "Add" "Parametric" "Relation" binders_opt ":" term1_extended term1_extended "reflexivity" "proved" "by" term1_extended "symmetry" "proved" "by" term1_extended "transitivity" "proved" "by" term1_extended "as" ident
+| "Add" "Parametric" "Relation" binders_opt ":" term1_extended term1_extended "transitivity" "proved" "by" term1_extended "as" ident
+| "Add" "Setoid" term1_extended term1_extended term1_extended "as" ident
+| "Add" "Parametric" "Setoid" binders_opt ":" term1_extended term1_extended term1_extended "as" ident
+| "Add" "Morphism" term1_extended ":" ident
+| "Declare" "Morphism" term1_extended ":" ident
+| "Add" "Morphism" term1_extended "with" "signature" term "as" ident
+| "Add" "Parametric" "Morphism" binders_opt ":" term1_extended "with" "signature" term "as" ident
 | "Grab" "Existential" "Variables"
 | "Unshelve"
-| "Declare" "Equivalent" "Keys" term term
+| "Declare" "Equivalent" "Keys" term1_extended term1_extended
 | "Print" "Equivalent" "Keys"
 | "Optimize" "Proof"
 | "Optimize" "Heap"
@@ -1446,129 +1384,143 @@ command: [
 | "Show" "Ltac" "Profile"
 | "Show" "Ltac" "Profile" "CutOff" int
 | "Show" "Ltac" "Profile" string
+| "Add" "InjTyp" term1_extended      (* micromega plugin *)
+| "Add" "BinOp" term1_extended      (* micromega plugin *)
+| "Add" "UnOp" term1_extended      (* micromega plugin *)
+| "Add" "CstOp" term1_extended      (* micromega plugin *)
+| "Add" "BinRel" term1_extended      (* micromega plugin *)
+| "Add" "PropOp" term1_extended      (* micromega plugin *)
+| "Add" "PropUOp" term1_extended      (* micromega plugin *)
+| "Add" "Spec" term1_extended      (* micromega plugin *)
+| "Add" "BinOpSpec" term1_extended      (* micromega plugin *)
+| "Add" "UnOpSpec" term1_extended      (* micromega plugin *)
+| "Add" "Saturate" term1_extended      (* micromega plugin *)
+| "Show" "Zify" "InjTyp"      (* micromega plugin *)
+| "Show" "Zify" "BinOp"      (* micromega plugin *)
+| "Show" "Zify" "UnOp"      (* micromega plugin *)
+| "Show" "Zify" "CstOp"      (* micromega plugin *)
+| "Show" "Zify" "BinRel"      (* micromega plugin *)
+| "Show" "Zify" "Spec"      (* micromega plugin *)
+| "Add" "Ring" ident ":" term1_extended ring_mods_opt      (* setoid_ring plugin *)
 | "Hint" "Cut" "[" hints_path "]" opthints
-| "Typeclasses" "Transparent" reference_list_opt
-| "Typeclasses" "Opaque" reference_list_opt
+| "Typeclasses" "Transparent" qualid_list_opt
+| "Typeclasses" "Opaque" qualid_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
+| "Print" "Rewrite" "HintDb" ident
+| "Proof" "with" ltac_expr 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
+| "Tactic" "Notation" ltac_tactic_level_opt ltac_production_item_list ":=" ltac_expr
+| "Print" "Ltac" qualid
+| "Locate" "Ltac" qualid
+| "Ltac" tacdef_body_list
 | "Print" "Ltac" "Signatures"
-| "String" "Notation" reference reference reference ":" ident
-| "Set" "Firstorder" "Solver" tactic
+| "Set" "Firstorder" "Solver" ltac_expr
 | "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" qualid      (* extraction plugin *)
+| "Recursive" "Extraction" qualid_list      (* extraction plugin *)
+| "Extraction" string qualid_list      (* extraction plugin *)
+| "Extraction" "TestCompile" qualid_list      (* extraction plugin *)
+| "Separate" "Extraction" qualid_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 *)
+| "Extraction" "Inline" qualid_list      (* extraction plugin *)
+| "Extraction" "NoInline" qualid_list      (* extraction plugin *)
 | "Print" "Extraction" "Inline"      (* extraction plugin *)
 | "Reset" "Extraction" "Inline"      (* extraction plugin *)
-| "Extraction" "Implicit" global "[" int_or_id_list_opt "]"      (* extraction plugin *)
+| "Extraction" "Implicit" qualid "[" 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 *)
+| "Extract" "Constant" qualid string_list_opt "=>" mlname      (* extraction plugin *)
+| "Extract" "Inlined" "Constant" qualid "=>" mlname      (* extraction plugin *)
+| "Extract" "Inductive" qualid "=>" mlname "[" mlname_list_opt "]" string_opt      (* extraction plugin *)
 | "Show" "Extraction"      (* extraction plugin *)
-| "Function" function_rec_definition_loc_list      (* funind plugin *)
+| "Function" fix_definition_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 *)
+| "Generate" "graph" "for" qualid      (* funind plugin *)
+| "Hint" "Rewrite" orient term1_extended_list ":" ident_list_opt
+| "Hint" "Rewrite" orient term1_extended_list "using" ltac_expr ":" ident_list_opt
+| "Hint" "Rewrite" orient term1_extended_list
+| "Hint" "Rewrite" orient term1_extended_list "using" ltac_expr
+| "Derive" "Inversion_clear" ident "with" term1_extended "Sort" sort_family
+| "Derive" "Inversion_clear" ident "with" term1_extended
+| "Derive" "Inversion" ident "with" term1_extended "Sort" sort_family
+| "Derive" "Inversion" ident "with" term1_extended
+| "Derive" "Dependent" "Inversion" ident "with" term1_extended "Sort" sort_family
+| "Derive" "Dependent" "Inversion_clear" ident "with" term1_extended "Sort" sort_family
+| "Declare" "Left" "Step" term1_extended
+| "Declare" "Right" "Step" term1_extended
 | "Print" "Rings"      (* setoid_ring plugin *)
-| "Add" "Field" ident ":" term field_mods_opt      (* setoid_ring plugin *)
+| "Add" "Field" ident ":" term1_extended 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 *)
+| "Numeral" "Notation" qualid qualid qualid ":" ident numnotoption
+| "String" "Notation" qualid qualid qualid ":" ident
 ]
 
-comment_list_opt: [
-| comment_list_opt comment
+orient: [
+| "->"
+| "<-"
 | empty
 ]
 
-Verbose_opt: [
-| "Verbose"
+string_opt: [
+| string
 | empty
 ]
 
-ne_string_alt: [
-| ne_string
-| IDENT
+qualid_list_opt: [
+| qualid_list_opt qualid
+| empty
 ]
 
-ne_string_list: [
-| ne_string_list ne_string
-| ne_string
+univ_name_list_opt: [
+| "@{" name_list_opt "}"
+| empty
 ]
 
-univ_name_list_opt: [
-| univ_name_list
+name_list_opt: [
+| name_list_opt name
 | empty
 ]
 
-option_ref_value_list: [
-| option_ref_value_list option_ref_value
-| option_ref_value
+section_subset_expr: [
+| starredidentref_list_opt
+| ssexpr
 ]
 
-discriminated_opt: [
-| "discriminated"
-| empty
+ssexpr: [
+| "-" ssexpr50
+| ssexpr50
 ]
 
-global_list: [
-| global_list global
-| global
+ssexpr50: [
+| ssexpr0 "-" ssexpr0
+| ssexpr0 "+" ssexpr0
+| ssexpr0
 ]
 
-preident_list_opt: [
-| preident_list_opt preident
-| empty
+ssexpr0: [
+| starredidentref
+| "(" starredidentref_list_opt ")"
+| "(" starredidentref_list_opt ")" "*"
+| "(" ssexpr ")"
+| "(" ssexpr ")" "*"
 ]
 
-reference_list_opt: [
-| reference_list_opt reference
+starredidentref_list_opt: [
+| starredidentref_list_opt starredidentref
 | empty
 ]
 
+starredidentref: [
+| ident
+| ident "*"
+| "Type"
+| "Type" "*"
+]
+
 int_opt: [
 | int
 | empty
@@ -1580,12 +1532,12 @@ using_opt: [
 ]
 
 with_opt: [
-| "with" tactic
+| "with" ltac_expr
 | empty
 ]
 
 ltac_tactic_level_opt: [
-| ltac_tactic_level
+| "(" "at" "level" num ")"
 | empty
 ]
 
@@ -1594,85 +1546,17 @@ ltac_production_item_list: [
 | 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
+tacdef_body_list: [
+| tacdef_body_list "with" tacdef_body
+| tacdef_body
 ]
 
 printable: [
 | "Term" smart_global univ_name_list_opt
 | "All"
-| "Section" global
-| "Grammar" IDENT
-| "Custom" "Grammar" IDENT
+| "Section" qualid
+| "Grammar" ident
+| "Custom" "Grammar" ident
 | "LoadPath" dirpath_opt
 | "Modules"
 | "Libraries"
@@ -1686,17 +1570,18 @@ printable: [
 | "Coercions"
 | "Coercion" "Paths" class_rawexpr class_rawexpr
 | "Canonical" "Projections"
+| "Typing" "Flags"
 | "Tables"
 | "Options"
 | "Hint"
 | "Hint" smart_global
 | "Hint" "*"
-| "HintDb" IDENT
+| "HintDb" ident
 | "Scopes"
-| "Scope" IDENT
-| "Visibility" IDENT_opt3
+| "Scope" ident
+| "Visibility" ident_opt
 | "Implicit" smart_global
-| Sorted_opt "Universes" printunivs_subgraph_opt ne_string_opt
+| Sorted_opt "Universes" printunivs_subgraph_opt string_opt
 | "Assumptions" smart_global
 | "Opaque" "Dependencies" smart_global
 | "Transparent" "Dependencies" smart_global
@@ -1711,9 +1596,9 @@ dirpath_opt: [
 | empty
 ]
 
-IDENT_opt3: [
-| IDENT
-| empty
+dirpath: [
+| ident
+| dirpath field
 ]
 
 Sorted_opt: [
@@ -1722,384 +1607,408 @@ Sorted_opt: [
 ]
 
 printunivs_subgraph_opt: [
-| printunivs_subgraph
+| "Subgraph" "(" qualid_list_opt ")"
 | empty
 ]
 
-ne_string_opt: [
-| ne_string
+comment_list_opt: [
+| comment_list_opt comment
 | empty
 ]
 
-printunivs_subgraph: [
-| "Subgraph" "(" reference_list_opt ")"
+Verbose_opt: [
+| "Verbose"
+| empty
 ]
 
-class_rawexpr: [
-| "Funclass"
-| "Sortclass"
-| smart_global
+string_alt: [
+| string
+| ident
 ]
 
-locatable: [
-| smart_global
-| "Term" smart_global
-| "File" ne_string
-| "Library" global
-| "Module" global
+string_list: [
+| string_list string
+| string
 ]
 
-option_setting: [
-| empty
-| integer
-| STRING
+option_ref_value_list: [
+| option_ref_value_list option_ref_value
+| option_ref_value
 ]
 
-option_ref_value: [
-| global
-| STRING
+discriminated_opt: [
+| "discriminated"
+| empty
 ]
 
-option_table: [
-| IDENT_list
+string_list_opt: [
+| string_list_opt string
+| empty
 ]
 
-as_dirpath: [
-| as_opt3
+mlname_list_opt: [
+| mlname_list_opt mlname
+| empty
 ]
 
-as_opt: [
-| "as" name
-| empty
+fun_scheme_arg_list: [
+| fun_scheme_arg_list "with" fun_scheme_arg
+| fun_scheme_arg
 ]
 
-ne_in_or_out_modules: [
-| "inside" global_list
-| "outside" global_list
+term1_extended_list: [
+| term1_extended_list term1_extended
+| term1_extended
 ]
 
-in_or_out_modules: [
-| ne_in_or_out_modules
+ring_mods_opt: [
+| "(" ring_mod_list_comma ")"      (* setoid_ring plugin *)
 | empty
 ]
 
-comment: [
-| term
-| STRING
-| natural
+field_mods_opt: [
+| "(" field_mod_list_comma ")"      (* setoid_ring plugin *)
+| empty
 ]
 
-positive_search_mark: [
-| "-"
-| empty
+locatable: [
+| smart_global
+| "Term" smart_global
+| "File" string
+| "Library" qualid
+| "Module" qualid
 ]
 
-searchabout_query: [
-| positive_search_mark ne_string scope_opt
-| positive_search_mark constr_pattern
+option_ref_value: [
+| qualid
+| string
 ]
 
-searchabout_queries: [
-| ne_in_or_out_modules
-| searchabout_query searchabout_queries
+as_dirpath: [
+| "as" dirpath
 | empty
 ]
 
-univ_name_list: [
-| "@{" name_list_opt "}"
+comment: [
+| term1_extended
+| string
+| num
 ]
 
-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
+reference_or_constr: [
+| qualid
+| term1_extended
 ]
 
-class_rawexpr_list: [
-| class_rawexpr_list class_rawexpr
-| class_rawexpr
+hint: [
+| "Resolve" reference_or_constr_list hint_info
+| "Resolve" "->" qualid_list num_opt
+| "Resolve" "<-" qualid_list num_opt
+| "Immediate" reference_or_constr_list
+| "Variables" "Transparent"
+| "Variables" "Opaque"
+| "Constants" "Transparent"
+| "Constants" "Opaque"
+| "Transparent" qualid_list
+| "Opaque" qualid_list
+| "Mode" qualid plus_list
+| "Unfold" qualid_list
+| "Constructors" qualid_list
+| "Extern" num term1_extended_opt "=>" ltac_expr
 ]
 
-syntax_modifier_opt: [
-| "(" syntax_modifier_list_comma ")"
-| empty
+reference_or_constr_list: [
+| reference_or_constr_list reference_or_constr
+| reference_or_constr
 ]
 
-syntax_modifier_list_comma: [
-| syntax_modifier_list_comma "," syntax_modifier
-| syntax_modifier
+constr_body: [
+| ":=" term
+| ":" term ":=" term
 ]
 
-only_parsing: [
-| "(" "only" "parsing" ")"
-| "(" "compat" STRING ")"
-| empty
+plus_list: [
+| plus_list plus_alt
+| plus_alt
 ]
 
-level: [
-| "level" natural
-| "next" "level"
+plus_alt: [
+| "+"
+| "!"
+| "-"
 ]
 
-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
+withtac: [
+| "with" ltac_expr
+| empty
 ]
 
-STRING_opt: [
-| STRING
-| empty
+ltac_def_kind: [
+| ":="
+| "::="
 ]
 
-IDENT_list_comma: [
-| IDENT_list_comma "," IDENT
-| IDENT
+tacdef_body: [
+| qualid fun_var_list ltac_def_kind ltac_expr
+| qualid ltac_def_kind ltac_expr
 ]
 
-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
+ltac_production_item: [
+| string
+| ident "(" ident ltac_production_sep_opt ")"
+| ident
 ]
 
-at_level_opt: [
-| at_level
+ltac_production_sep_opt: [
+| "," string
 | empty
 ]
 
-constr_as_binder_kind_opt: [
-| constr_as_binder_kind
+numnotoption: [
 | empty
+| "(" "warning" "after" num ")"
+| "(" "abstract" "after" num ")"
 ]
 
-at_level: [
-| "at" level
+mlname: [
+| ident      (* extraction plugin *)
+| string      (* extraction plugin *)
 ]
 
-constr_as_binder_kind: [
-| "as" "ident"
-| "as" "pattern"
-| "as" "strict" "pattern"
+int_or_id: [
+| ident      (* extraction plugin *)
+| int      (* extraction plugin *)
 ]
 
-opt_hintbases: [
-| empty
-| ":" IDENT_list
+language: [
+| "Ocaml"      (* extraction plugin *)
+| "OCaml"      (* extraction plugin *)
+| "Haskell"      (* extraction plugin *)
+| "Scheme"      (* extraction plugin *)
+| "JSON"      (* extraction plugin *)
 ]
 
-IDENT_list: [
-| IDENT_list IDENT
-| IDENT
+fun_scheme_arg: [
+| ident ":=" "Induction" "for" qualid "Sort" sort_family      (* funind plugin *)
 ]
 
-reference_or_constr: [
-| global
-| term
+ring_mod: [
+| "decidable" term1_extended      (* setoid_ring plugin *)
+| "abstract"      (* setoid_ring plugin *)
+| "morphism" term1_extended      (* setoid_ring plugin *)
+| "constants" "[" ltac_expr "]"      (* setoid_ring plugin *)
+| "closed" "[" qualid_list "]"      (* setoid_ring plugin *)
+| "preprocess" "[" ltac_expr "]"      (* setoid_ring plugin *)
+| "postprocess" "[" ltac_expr "]"      (* setoid_ring plugin *)
+| "setoid" term1_extended term1_extended      (* setoid_ring plugin *)
+| "sign" term1_extended      (* setoid_ring plugin *)
+| "power" term1_extended "[" qualid_list "]"      (* setoid_ring plugin *)
+| "power_tac" term1_extended "[" ltac_expr "]"      (* setoid_ring plugin *)
+| "div" term1_extended      (* setoid_ring plugin *)
 ]
 
-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
+ring_mod_list_comma: [
+| ring_mod_list_comma "," ring_mod
+| ring_mod
 ]
 
-reference_or_constr_list: [
-| reference_or_constr_list reference_or_constr
-| reference_or_constr
+field_mod: [
+| ring_mod      (* setoid_ring plugin *)
+| "completeness" term1_extended      (* setoid_ring plugin *)
 ]
 
-natural_opt2: [
-| "|" natural
-| empty
+field_mod_list_comma: [
+| field_mod_list_comma "," field_mod
+| field_mod
 ]
 
-constr_pattern_opt: [
-| constr_pattern
+debug: [
+| "debug"
 | empty
 ]
 
-constr_body: [
-| ":=" lconstr
-| ":" lconstr ":=" lconstr
+eauto_search_strategy: [
+| "(bfs)"
+| "(dfs)"
+| empty
 ]
 
-mode: [
-| plus_list
+hints_path_atom: [
+| qualid_list
+| "_"
 ]
 
-plus_list: [
-| plus_list plus_alt
-| plus_alt
+hints_path: [
+| "(" hints_path ")"
+| hints_path "*"
+| "emp"
+| "eps"
+| hints_path "|" hints_path
+| hints_path_atom
+| hints_path hints_path
 ]
 
-plus_alt: [
-| "+"
-| "!"
-| "-"
+opthints: [
+| ":" ident_list
+| empty
 ]
 
-vernac_toplevel: [
-| "Drop" "."
-| "Quit" "."
-| "Backtrack" natural natural natural "."
-| "Show" "Goal" natural "at" natural "."
-| vernac_control
+opt_hintbases: [
+| empty
+| ":" ident_list
 ]
 
-orient: [
-| "->"
-| "<-"
+int_or_id_list_opt: [
+| int_or_id_list_opt int_or_id
 | empty
 ]
 
-occurrences: [
-| integer_list
-| var
+query_command: [
+| "Eval" red_expr "in" term "."
+| "Compute" term "."
+| "Check" term "."
+| "About" smart_global univ_name_list_opt "."
+| "SearchHead" term1_extended in_or_out_modules "."
+| "SearchPattern" term1_extended in_or_out_modules "."
+| "SearchRewrite" term1_extended in_or_out_modules "."
+| "Search" searchabout_query searchabout_queries "."
+| "SearchAbout" searchabout_query searchabout_queries "."
+| "SearchAbout" "[" searchabout_query_list "]" in_or_out_modules "."
 ]
 
-integer_list: [
-| integer_list integer
-| integer
+ne_in_or_out_modules: [
+| "inside" qualid_list
+| "outside" qualid_list
 ]
 
-glob: [
-| term
+in_or_out_modules: [
+| ne_in_or_out_modules
+| empty
 ]
 
-lglob: [
-| lconstr
+positive_search_mark: [
+| "-"
+| empty
 ]
 
-casted_constr: [
-| term
+searchabout_query: [
+| positive_search_mark string scope_delimiter_opt
+| positive_search_mark term1_extended
 ]
 
-hloc: [
+searchabout_queries: [
+| ne_in_or_out_modules
+| searchabout_query searchabout_queries
 | empty
-| "in" "|-" "*"
-| "in" ident
-| "in" "(" "Type" "of" ident ")"
-| "in" "(" "Value" "of" ident ")"
-| "in" "(" "type" "of" ident ")"
-| "in" "(" "value" "of" ident ")"
 ]
 
-rename: [
-| ident "into" ident
+searchabout_query_list: [
+| searchabout_query_list searchabout_query
+| searchabout_query
 ]
 
-by_arg_tac: [
-| "by" ltac_expr3
-| empty
+syntax: [
+| "Open" "Scope" ident
+| "Close" "Scope" ident
+| "Delimit" "Scope" ident "with" ident
+| "Undelimit" "Scope" ident
+| "Bind" "Scope" ident "with" class_rawexpr_list
+| "Infix" string ":=" term1_extended syntax_modifier_opt ident_opt3
+| "Notation" ident ident_list_opt ":=" term1_extended only_parsing
+| "Notation" string ":=" term1_extended syntax_modifier_opt ident_opt3
+| "Format" "Notation" string string string
+| "Reserved" "Infix" string syntax_modifier_opt
+| "Reserved" "Notation" string syntax_modifier_opt
 ]
 
-in_clause: [
-| in_clause
-| "*" occs
-| "*" "|-" concl_occ
-| hypident_occ_list_comma_opt "|-" concl_occ
-| hypident_occ_list_comma_opt
+class_rawexpr_list: [
+| class_rawexpr_list class_rawexpr
+| class_rawexpr
 ]
 
-hypident_occ_list_comma_opt: [
-| hypident_occ_list_comma
+syntax_modifier_opt: [
+| "(" syntax_modifier_list_comma ")"
 | empty
 ]
 
-hypident_occ_list_comma: [
-| hypident_occ_list_comma "," hypident_occ
-| hypident_occ
+syntax_modifier_list_comma: [
+| syntax_modifier_list_comma "," syntax_modifier
+| syntax_modifier
 ]
 
-test_lpar_id_colon: [
+only_parsing: [
+| "(" "only" "parsing" ")"
+| "(" "compat" string ")"
 | empty
 ]
 
-withtac: [
-| "with" tactic
-| empty
+level: [
+| "level" num
+| "next" "level"
 ]
 
-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 ")"
+syntax_modifier: [
+| "at" "level" num
+| "in" "custom" ident
+| "in" "custom" ident "at" "level" num
+| "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
 ]
 
-typeclass_constraint_list_comma: [
-| typeclass_constraint_list_comma "," typeclass_constraint
-| typeclass_constraint
+syntax_extension_type: [
+| "ident"
+| "global"
+| "bigint"
+| "binder"
+| "constr"
+| "constr" level_opt constr_as_binder_kind_opt
+| "pattern"
+| "pattern" "at" "level" num
+| "strict" "pattern"
+| "strict" "pattern" "at" "level" num
+| "closed" "binder"
+| "custom" ident level_opt constr_as_binder_kind_opt
 ]
 
-of_alt: [
-| "of"
-| "&"
+level_opt: [
+| level
+| empty
+]
+
+constr_as_binder_kind_opt: [
+| constr_as_binder_kind
+| empty
+]
+
+constr_as_binder_kind: [
+| "as" "ident"
+| "as" "pattern"
+| "as" "strict" "pattern"
 ]
 
 simple_tactic: [
 | "reflexivity"
-| "exact" casted_constr
+| "exact" term1_extended
 | "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
+| "cut" term1_extended
+| "exact_no_check" term1_extended
+| "vm_cast_no_check" term1_extended
+| "native_cast_no_check" term1_extended
+| "casetype" term1_extended
+| "elimtype" term1_extended
+| "lapply" term1_extended
+| "transitivity" term1_extended
 | "left"
 | "eleft"
 | "left" "with" bindings
@@ -2131,32 +2040,32 @@ simple_tactic: [
 | "intro" ident
 | "intro" ident "at" "top"
 | "intro" ident "at" "bottom"
-| "intro" ident "after" var
-| "intro" ident "before" var
+| "intro" ident "after" ident
+| "intro" ident "before" ident
 | "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
+| "intro" "after" ident
+| "intro" "before" ident
+| "move" ident "at" "top"
+| "move" ident "at" "bottom"
+| "move" ident "after" ident
+| "move" ident "before" ident
 | "rename" rename_list_comma
-| "revert" var_list
+| "revert" ident_list
 | "simple" "induction" quantified_hypothesis
 | "simple" "destruct" quantified_hypothesis
 | "double" "induction" quantified_hypothesis quantified_hypothesis
 | "admit"
-| "fix" ident natural
+| "fix" ident num
 | "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
+| "clear" ident_list_opt
+| "clear" "-" ident_list
+| "clearbody" ident_list
+| "generalize" "dependent" term1_extended
+| "replace" term1_extended "with" term1_extended clause_dft_concl by_arg_tac
+| "replace" "->" term1_extended clause_dft_concl
+| "replace" "<-" term1_extended clause_dft_concl
+| "replace" term1_extended clause_dft_concl
 | "simplify_eq"
 | "simplify_eq" destruction_arg
 | "esimplify_eq"
@@ -2175,64 +2084,64 @@ simple_tactic: [
 | "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
+| "dependent" "rewrite" orient term1_extended
+| "dependent" "rewrite" orient term1_extended "in" ident
+| "cutrewrite" orient term1_extended
+| "cutrewrite" orient term1_extended "in" ident
+| "decompose" "sum" term1_extended
+| "decompose" "record" term1_extended
+| "absurd" term1_extended
 | "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
+| "autorewrite" "with" ident_list clause_dft_concl
+| "autorewrite" "with" ident_list clause_dft_concl "using" ltac_expr
+| "autorewrite" "*" "with" ident_list clause_dft_concl
+| "autorewrite" "*" "with" ident_list clause_dft_concl "using" ltac_expr
+| "rewrite" "*" orient term1_extended "in" ident "at" occurrences by_arg_tac
+| "rewrite" "*" orient term1_extended "at" occurrences "in" ident by_arg_tac
+| "rewrite" "*" orient term1_extended "in" ident by_arg_tac
+| "rewrite" "*" orient term1_extended "at" occurrences by_arg_tac
+| "rewrite" "*" orient term1_extended by_arg_tac
+| "refine" term1_extended
+| "simple" "refine" term1_extended
+| "notypeclasses" "refine" term1_extended
+| "simple" "notypeclasses" "refine" term1_extended
 | "solve_constraints"
-| "subst" var_list
+| "subst" ident_list
 | "subst"
 | "simple" "subst"
-| "evar" test_lpar_id_colon "(" ident ":" lconstr ")"
-| "evar" term
-| "instantiate" "(" ident ":=" lglob ")"
-| "instantiate" "(" integer ":=" lglob ")" hloc
+| "evar" "(" ident ":" term ")"
+| "evar" term1_extended
+| "instantiate" "(" ident ":=" term ")"
+| "instantiate" "(" int ":=" term ")" 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
+| "stepl" term1_extended "by" ltac_expr
+| "stepl" term1_extended
+| "stepr" term1_extended "by" ltac_expr
+| "stepr" term1_extended
+| "generalize_eqs" ident
+| "dependent" "generalize_eqs" ident
+| "generalize_eqs_vars" ident
+| "dependent" "generalize_eqs_vars" ident
+| "specialize_eqs" ident
+| "hresolve_core" "(" ident ":=" term1_extended ")" "at" int_or_var "in" term1_extended
+| "hresolve_core" "(" ident ":=" term1_extended ")" "in" term1_extended
 | "hget_evar" int_or_var
 | "destauto"
-| "destauto" "in" var
+| "destauto" "in" ident
 | "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
+| "constr_eq" term1_extended term1_extended
+| "constr_eq_strict" term1_extended term1_extended
+| "constr_eq_nounivs" term1_extended term1_extended
+| "is_evar" term1_extended
+| "has_evar" term1_extended
+| "is_var" term1_extended
+| "is_fix" term1_extended
+| "is_cofix" term1_extended
+| "is_ind" term1_extended
+| "is_constructor" term1_extended
+| "is_proj" term1_extended
+| "is_const" term1_extended
 | "shelve"
 | "shelve_unifiable"
 | "unshelve" ltac_expr1
@@ -2240,8 +2149,8 @@ simple_tactic: [
 | "cycle" int_or_var
 | "swap" int_or_var int_or_var
 | "revgoals"
-| "guard" test
-| "decompose" "[" term_list "]" term
+| "guard" int_or_var comparison int_or_var
+| "decompose" "[" term1_extended_list "]" term1_extended
 | "optimize_heap"
 | "start" "ltac" "profiling"
 | "stop" "ltac" "profiling"
@@ -2253,51 +2162,51 @@ simple_tactic: [
 | "finish_timing" string_opt
 | "finish_timing" "(" string ")" string_opt
 | "eassumption"
-| "eexact" term
+| "eexact" term1_extended
 | "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
+| "prolog" "[" term1_extended_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 "in" ident
 | "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
+| "unify" term1_extended term1_extended
+| "unify" term1_extended term1_extended "with" ident
+| "convert_concl_no_check" term1_extended
+| "typeclasses" "eauto" "bfs" int_or_var_opt "with" ident_list
+| "typeclasses" "eauto" int_or_var_opt "with" ident_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
+| "head_of_constr" ident term1_extended
+| "not_evar" term1_extended
+| "is_ground" term1_extended
+| "autoapply" term1_extended "using" ident
+| "autoapply" term1_extended "with" ident
+| "progress_evars" ltac_expr
 | "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
+| "rewrite_db" ident "in" ident
+| "rewrite_db" ident
+| "substitute" orient constr_with_bindings
+| "setoid_rewrite" orient constr_with_bindings
+| "setoid_rewrite" orient constr_with_bindings "in" ident
+| "setoid_rewrite" orient constr_with_bindings "at" occurrences
+| "setoid_rewrite" orient constr_with_bindings "at" occurrences "in" ident
+| "setoid_rewrite" orient constr_with_bindings "in" ident "at" occurrences
 | "setoid_symmetry"
-| "setoid_symmetry" "in" var
+| "setoid_symmetry" "in" ident
 | "setoid_reflexivity"
-| "setoid_transitivity" term
+| "setoid_transitivity" term1_extended
 | "setoid_etransitivity"
 | "decide" "equality"
-| "compare" term term
+| "compare" term1_extended term1_extended
+| "rewrite_strat" rewstrategy "in" ident
 | "intros" intropattern_list_opt
 | "eintros" intropattern_list_opt
 | "apply" constr_with_bindings_arg_list_comma in_hyp_as
@@ -2308,33 +2217,33 @@ simple_tactic: [
 | "eelim" constr_with_bindings_arg eliminator_opt
 | "case" induction_clause_list
 | "ecase" induction_clause_list
-| "fix" ident natural "with" fixdecl_list
+| "fix" ident num "with" fixdecl_list
 | "cofix" ident "with" cofixdecl_list
 | "pose" bindings_with_parameters
-| "pose" term as_name
+| "pose" term1_extended as_name
 | "epose" bindings_with_parameters
-| "epose" term as_name
+| "epose" term1_extended as_name
 | "set" bindings_with_parameters clause_dft_concl
-| "set" term as_name clause_dft_concl
+| "set" term1_extended 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
+| "eset" term1_extended as_name clause_dft_concl
+| "remember" term1_extended as_name eqn_ipat clause_dft_all
+| "eremember" term1_extended as_name eqn_ipat clause_dft_all
+| "assert" "(" ident ":=" term ")"
+| "eassert" "(" ident ":=" term ")"
+| "assert" "(" ident ":" term ")" by_tactic
+| "eassert" "(" ident ":" term ")" by_tactic
+| "enough" "(" ident ":" term ")" by_tactic
+| "eenough" "(" ident ":" term ")" by_tactic
+| "assert" term1_extended as_ipat by_tactic
+| "eassert" term1_extended as_ipat by_tactic
+| "pose" "proof" term as_ipat
+| "epose" "proof" term as_ipat
+| "enough" term1_extended as_ipat by_tactic
+| "eenough" term1_extended as_ipat by_tactic
+| "generalize" term1_extended
+| "generalize" term1_extended term1_extended_list
+| "generalize" term1_extended occs as_name pattern_occ_list_opt
 | "induction" induction_clause_list
 | "einduction" induction_clause_list
 | "destruct" induction_clause_list
@@ -2345,7 +2254,7 @@ simple_tactic: [
 | "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
+| "inversion" quantified_hypothesis "using" term1_extended in_hyp_list
 | "red" clause_dft_concl
 | "hnf" clause_dft_concl
 | "simpl" delta_flag ref_or_pattern_occ_opt clause_dft_concl
@@ -2356,357 +2265,176 @@ simple_tactic: [
 | "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
+| "fold" term1_extended_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
+| "congruence" int
+| "congruence" "with" term1_extended_list
+| "congruence" int "with" term1_extended_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 *)
+| "firstorder" ltac_expr_opt firstorder_using
+| "firstorder" ltac_expr_opt "with" ident_list
+| "firstorder" ltac_expr_opt firstorder_using "with" ident_list
+| "gintuition" ltac_expr_opt
+| "functional" "inversion" quantified_hypothesis qualid_opt      (* funind plugin *)
+| "functional" "induction" term1_extended_list fun_ind_using with_names      (* funind plugin *)
+| "soft" "functional" "induction" term1_extended_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 *)
+| "psatz_Z" int_or_var ltac_expr      (* micromega plugin *)
+| "psatz_Z" ltac_expr      (* micromega plugin *)
+| "xlia" ltac_expr      (* micromega plugin *)
+| "xnlia" ltac_expr      (* micromega plugin *)
+| "xnra" ltac_expr      (* micromega plugin *)
+| "xnqa" ltac_expr      (* micromega plugin *)
+| "sos_Z" ltac_expr      (* micromega plugin *)
+| "sos_Q" ltac_expr      (* micromega plugin *)
+| "sos_R" ltac_expr      (* micromega plugin *)
+| "lra_Q" ltac_expr      (* micromega plugin *)
+| "lra_R" ltac_expr      (* micromega plugin *)
+| "psatz_R" int_or_var ltac_expr      (* micromega plugin *)
+| "psatz_R" ltac_expr      (* micromega plugin *)
+| "psatz_Q" int_or_var ltac_expr      (* micromega plugin *)
+| "psatz_Q" ltac_expr      (* micromega plugin *)
+| "iter_specs" ltac_expr      (* micromega plugin *)
+| "zify_op"      (* micromega plugin *)
+| "saturate"      (* micromega plugin *)
+| "nsatz_compute" term1_extended      (* 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
+| "ring_lookup" ltac_expr0 "[" term1_extended_list_opt "]" term1_extended_list      (* setoid_ring plugin *)
+| "field_lookup" ltac_expr "[" term1_extended_list_opt "]" term1_extended_list      (* setoid_ring plugin *)
 ]
 
-constr_with_bindings_opt: [
-| constr_with_bindings
-| empty
-]
-
-int_or_var_opt: [
-| int_or_var
-| empty
+int_or_var: [
+| int
+| ident
 ]
 
-uconstr_list_opt: [
-| uconstr_list_opt uconstr
+constr_with_bindings_opt: [
+| constr_with_bindings
 | 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
+hloc: [
 | empty
+| "in" "|-" "*"
+| "in" ident
+| "in" "(" "Type" "of" ident ")"
+| "in" "(" "Value" "of" ident ")"
+| "in" "(" "type" "of" ident ")"
+| "in" "(" "value" "of" ident ")"
 ]
 
-oriented_rewriter_list_comma: [
-| oriented_rewriter_list_comma "," oriented_rewriter
-| oriented_rewriter
-]
-
-simple_alt: [
-| "simple" "inversion"
-| "inversion"
-| "inversion_clear"
+rename: [
+| ident "into" ident
 ]
 
-with_opt2: [
-| "with" term
+by_arg_tac: [
+| "by" ltac_expr3
 | empty
 ]
 
-tactic_opt: [
-| tactic
-| empty
+in_clause: [
+| in_clause
+| "*" occs
+| "*" "|-" concl_occ
+| hypident_occ_list_comma_opt "|-" concl_occ
+| hypident_occ_list_comma_opt
 ]
 
-reference_opt: [
-| reference
+occs: [
+| "at" occs_nums
 | 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
+hypident_occ_list_comma_opt: [
+| hypident_occ_list_comma
 | empty
 ]
 
-preident_list: [
-| preident_list preident
-| preident
-]
-
-auto_using: [
-| "using" uconstr_list_comma
+as_ipat: [
+| "as" simple_intropattern
 | 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
+or_and_intropattern_loc: [
+| or_and_intropattern
+| ident
 ]
 
-opthints: [
-| ":" preident_list
+as_or_and_ipat: [
+| "as" or_and_intropattern_loc
 | empty
 ]
 
-debug: [
-| "debug"
+eqn_ipat: [
+| "eqn" ":" naming_intropattern
+| "_eqn" ":" naming_intropattern
+| "_eqn"
 | empty
 ]
 
-eauto_search_strategy: [
-| "(bfs)"
-| "(dfs)"
+as_name: [
+| "as" ident
 | 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
+by_tactic: [
+| "by" ltac_expr3
 | 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
+rewriter: [
+| "!" constr_with_bindings_arg
+| qmark_alt constr_with_bindings_arg
+| num "!" constr_with_bindings_arg
+| num qmark_alt constr_with_bindings_arg
+| num constr_with_bindings_arg
 | constr_with_bindings_arg
 ]
 
-constr_with_bindings_arg: [
-| ">" constr_with_bindings
-| constr_with_bindings
+qmark_alt: [
+| "?"
+| "?"
 ]
 
-quantified_hypothesis: [
-| ident
-| natural
+oriented_rewriter: [
+| orient rewriter
 ]
 
-conversion: [
-| term
-| term "with" term
-| term "at" occs_nums "with" term
+induction_clause: [
+| destruction_arg as_or_and_ipat eqn_ipat opt_clause
 ]
 
-occs_nums: [
-| nat_or_var_list
-| "-" nat_or_var int_or_var_list_opt
+induction_clause_list: [
+| induction_clause_list_comma eliminator_opt opt_clause
 ]
 
-nat_or_var_list: [
-| nat_or_var_list nat_or_var
-| nat_or_var
+induction_clause_list_comma: [
+| induction_clause_list_comma "," induction_clause
+| induction_clause
 ]
 
-int_or_var_list_opt: [
-| int_or_var_list_opt int_or_var
+eliminator_opt: [
+| "using" constr_with_bindings
 | empty
 ]
 
-occs: [
-| "at" occs_nums
+auto_using: [
+| "using" term1_extended_list_comma
 | empty
 ]
 
-pattern_occ: [
-| term occs
-]
-
-ref_or_pattern_occ: [
-| smart_global occs
-| term occs
-]
-
-unfold_occ: [
-| smart_global occs
+term1_extended_list_comma: [
+| term1_extended_list_comma "," term1_extended
+| term1_extended
 ]
 
 intropattern_list_opt: [
@@ -2764,11 +2492,11 @@ intropattern: [
 ]
 
 simple_intropattern: [
-| simple_intropattern_closed operconstr0_list_opt
+| simple_intropattern_closed term0_list_opt
 ]
 
-operconstr0_list_opt: [
-| operconstr0_list_opt "%" operconstr0
+term0_list_opt: [
+| term0_list_opt "%" term0
 | empty
 ]
 
@@ -2780,13 +2508,13 @@ simple_intropattern_closed: [
 ]
 
 simple_binding: [
-| "(" ident ":=" lconstr ")"
-| "(" natural ":=" lconstr ")"
+| "(" ident ":=" term ")"
+| "(" num ":=" term ")"
 ]
 
 bindings: [
 | simple_binding_list
-| term_list
+| term1_extended_list
 ]
 
 simple_binding_list: [
@@ -2794,88 +2522,88 @@ simple_binding_list: [
 | simple_binding
 ]
 
-term_list: [
-| term_list term
-| term
+constr_with_bindings_arg_list_comma: [
+| constr_with_bindings_arg_list_comma "," constr_with_bindings_arg
+| constr_with_bindings_arg
 ]
 
-constr_with_bindings: [
-| term with_bindings
+fixdecl_list: [
+| fixdecl_list fixdecl
+| fixdecl
 ]
 
-with_bindings: [
-| "with" bindings
+cofixdecl_list: [
+| cofixdecl_list cofixdecl
+| cofixdecl
+]
+
+pattern_occ_list_opt: [
+| pattern_occ_list_opt "," pattern_occ as_name
 | empty
 ]
 
-red_flags: [
-| "beta"
-| "iota"
-| "match"
-| "fix"
-| "cofix"
-| "zeta"
-| "delta" delta_flag
+pattern_occ: [
+| term1_extended occs
 ]
 
-delta_flag: [
-| "-" "[" smart_global_list "]"
-| "[" smart_global_list "]"
+oriented_rewriter_list_comma: [
+| oriented_rewriter_list_comma "," oriented_rewriter
+| oriented_rewriter
+]
+
+simple_alt: [
+| "simple" "inversion"
+| "inversion"
+| "inversion_clear"
+]
+
+with_opt2: [
+| "with" term1_extended
 | empty
 ]
 
-smart_global_list: [
-| smart_global_list smart_global
-| smart_global
+bindings_list_comma: [
+| bindings_list_comma "," bindings
+| bindings
 ]
 
-strategy_flag: [
-| red_flags_list
-| delta_flag
+rename_list_comma: [
+| rename_list_comma "," rename
+| rename
 ]
 
-red_flags_list: [
-| red_flags_list red_flags
-| red_flags
+comparison: [
+| "="
+| "<"
+| "<="
+| ">"
+| ">="
 ]
 
-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
+hintbases: [
+| "with" "*"
+| "with" ident_list
+| empty
 ]
 
-ref_or_pattern_occ_opt: [
-| ref_or_pattern_occ
+qualid_opt: [
+| qualid
 | empty
 ]
 
-unfold_occ_list_comma: [
-| unfold_occ_list_comma "," unfold_occ
-| unfold_occ
+bindings_with_parameters: [
+| "(" ident simple_binder_list_opt ":=" term ")"
 ]
 
-pattern_occ_list_comma: [
-| pattern_occ_list_comma "," pattern_occ
-| pattern_occ
+simple_binder_list_opt: [
+| simple_binder_list_opt simple_binder
+| empty
 ]
 
 hypident: [
-| id_or_meta
-| "(" "type" "of" id_or_meta ")"
-| "(" "value" "of" id_or_meta ")"
-| "(" "type" "of" ident ")"      (* ssr plugin *)
-| "(" "value" "of" ident ")"      (* ssr plugin *)
+| ident
+| "(" "type" "of" ident ")"
+| "(" "value" "of" ident ")"
 ]
 
 hypident_occ: [
@@ -2899,118 +2627,151 @@ opt_clause: [
 | empty
 ]
 
+occs_nums: [
+| num_or_var_list
+| "-" num_or_var int_or_var_list_opt
+]
+
+num_or_var: [
+| num
+| ident
+]
+
+int_or_var_list_opt: [
+| int_or_var_list_opt int_or_var
+| empty
+]
+
+num_or_var_list: [
+| num_or_var_list num_or_var
+| num_or_var
+]
+
 concl_occ: [
 | "*" occs
 | empty
 ]
 
 in_hyp_list: [
-| "in" id_or_meta_list
+| "in" ident_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
+| "in" ident as_ipat
 | empty
 ]
 
 simple_binder: [
 | name
-| "(" name_list ":" lconstr ")"
+| "(" names ":" term ")"
 ]
 
 fixdecl: [
-| "(" ident simple_binder_list_opt fixannot ":" lconstr ")"
+| "(" ident simple_binder_list_opt struct_annot ":" term ")"
 ]
 
-cofixdecl: [
-| "(" ident simple_binder_list_opt ":" lconstr ")"
-]
-
-bindings_with_parameters: [
-| "(" ident simple_binder_list_opt ":=" lconstr ")"
+struct_annot: [
+| "{" "struct" name "}"
+| empty
 ]
 
-simple_binder_list_opt: [
-| simple_binder_list_opt simple_binder
-| empty
+cofixdecl: [
+| "(" ident simple_binder_list_opt ":" term ")"
 ]
 
-eliminator: [
-| "using" constr_with_bindings
+constr_with_bindings: [
+| term1_extended with_bindings
 ]
 
-as_ipat: [
-| "as" simple_intropattern
+with_bindings: [
+| "with" bindings
 | empty
 ]
 
-or_and_intropattern_loc: [
-| or_and_intropattern
-| ident
+destruction_arg: [
+| num
+| constr_with_bindings
+| constr_with_bindings_arg
 ]
 
-as_or_and_ipat: [
-| "as" or_and_intropattern_loc
-| empty
+constr_with_bindings_arg: [
+| ">" constr_with_bindings
+| constr_with_bindings
 ]
 
-eqn_ipat: [
-| "eqn" ":" naming_intropattern
-| "_eqn" ":" naming_intropattern
-| "_eqn"
-| empty
+quantified_hypothesis: [
+| ident
+| num
 ]
 
-as_name: [
-| "as" ident
-| empty
+conversion: [
+| term1_extended
+| term1_extended "with" term1_extended
+| term1_extended "at" occs_nums "with" term1_extended
 ]
 
-by_tactic: [
-| "by" ltac_expr3
+firstorder_using: [
+| "using" qualid
+| "using" qualid "," qualid_list_comma
+| "using" qualid qualid qualid_list_opt
 | 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
+qualid_list_comma: [
+| qualid_list_comma "," qualid
+| qualid
 ]
 
-qmark_alt: [
-| "?"
-| "?"
+fun_ind_using: [
+| "using" constr_with_bindings      (* funind plugin *)
+| empty      (* funind plugin *)
 ]
 
-oriented_rewriter: [
-| orient rewriter
+with_names: [
+| "as" simple_intropattern      (* funind plugin *)
+| empty      (* funind plugin *)
 ]
 
-induction_clause: [
-| destruction_arg as_or_and_ipat eqn_ipat opt_clause
+occurrences: [
+| int_list
+| ident
 ]
 
-induction_clause_list: [
-| induction_clause_list_comma eliminator_opt opt_clause
+int_list: [
+| int_list int
+| int
 ]
 
-induction_clause_list_comma: [
-| induction_clause_list_comma "," induction_clause
-| induction_clause
+rewstrategy: [
+| term1_extended
+| "<-" term1_extended
+| "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" ident
+| "hints" ident
+| "terms" term1_extended_list_opt
+| "eval" red_expr
+| "fold" term1_extended
 ]
 
-eliminator_opt: [
-| eliminator
-| empty
+hypident_occ_list_comma: [
+| hypident_occ_list_comma "," hypident_occ
+| hypident_occ
 ]
 
 ltac_expr: [
@@ -3019,19 +2780,19 @@ ltac_expr: [
 ]
 
 binder_tactic: [
-| "fun" input_fun_list "=>" ltac_expr
+| "fun" fun_var_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
+fun_var_list: [
+| fun_var_list fun_var
+| fun_var
 ]
 
-input_fun: [
-| "_"
+fun_var: [
 | ident
+| "_"
 ]
 
 rec_opt: [
@@ -3047,27 +2808,20 @@ let_clause_list: [
 let_clause: [
 | ident ":=" ltac_expr
 | "_" ":=" ltac_expr
-| ident input_fun_list ":=" ltac_expr
+| ident fun_var_list ":=" ltac_expr
 ]
 
 ltac_expr4: [
 | ltac_expr3 ";" binder_tactic
 | ltac_expr3 ";" ltac_expr3
-| ltac_expr3 ";" "[" gt_opt tactic_then_gen "]"
+| ltac_expr3 ";" "[" multi_goal_tactics "]"
+| ltac_expr3 ";" "[" ">" multi_goal_tactics "]"
 | 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
+multi_goal_tactics: [
+| ltac_expr_opt "|" multi_goal_tactics
+| ltac_expr_opt ".." or_opt ltac_expr_opt_list_or
 | ltac_expr
 | empty
 ]
@@ -3077,13 +2831,8 @@ ltac_expr_opt: [
 | 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_list_or: [
+| ltac_expr_opt_list_or "|" ltac_expr_opt
 | ltac_expr_opt
 ]
 
@@ -3099,51 +2848,10 @@ 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 *)
+| only_selector ltac_expr3
 | 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
@@ -3154,30 +2862,18 @@ ltac_expr2: [
 ]
 
 ltac_expr1: [
-| match_key reverse_opt "goal" "with" match_context_list "end"
-| match_key ltac_expr "with" match_list "end"
+| ltac_match_term
+| ltac_match_goal
 | "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 *)
+| qualid tactic_arg_compat_list_opt
 | ltac_expr0
 ]
 
-match_key: [
-| "match"
-| "lazymatch"
-| "multimatch"
-]
-
-reverse_opt: [
-| "reverse"
-| empty
-]
-
 ltac_expr_list_or_opt: [
 | ltac_expr_list_or
 | empty
@@ -3188,95 +2884,27 @@ ltac_expr_list_or: [
 | 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
+message_token_list_opt: [
+| message_token_list_opt message_token
 | 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: [
+message_token: [
 | ident
-| empty
-]
-
-lconstr_pattern: [
-| lconstr
+| string
+| int
 ]
 
-match_pattern_opt: [
-| "[" match_pattern "]" ":"
+int_or_var_opt: [
+| int_or_var
 | 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
+term1_extended_list_opt: [
+| term1_extended_list_opt term1_extended
 | empty
 ]
 
-message_token: [
-| ident
-| STRING
-| integer
-]
-
 failkw: [
 | "fail"
 | "gfail"
@@ -3284,10 +2912,10 @@ failkw: [
 
 tactic_arg: [
 | "eval" red_expr "in" term
-| "context" ident "[" lconstr "]"
+| "context" ident "[" term "]"
 | "type" "of" term
 | "fresh" fresh_id_list_opt
-| "type_term" uconstr
+| "type_term" term1_extended
 | "numgoals"
 ]
 
@@ -3297,7 +2925,7 @@ fresh_id_list_opt: [
 ]
 
 fresh_id: [
-| STRING
+| string
 | qualid
 ]
 
@@ -3314,857 +2942,112 @@ tactic_arg_compat: [
 
 ltac_expr0: [
 | "(" ltac_expr ")"
-| "[" ">" tactic_then_gen "]"
+| "[>" multi_goal_tactics "]"
 | tactic_atom
-| ssrparentacarg      (* ssr plugin *)
 ]
 
 tactic_atom: [
-| integer
-| reference
+| int
+| qualid
 | "()"
 ]
 
-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
+toplevel_selector: [
+| selector ":"
+| "all" ":"
+| "!" ":"
 ]
 
-tactic: [
-| ltac_expr
+only_selector: [
+| "only" selector ":"
 ]
 
-ltac_info_opt: [
-| ltac_info
-| empty
+selector: [
+| range_selector_list_comma
+| "[" ident "]"
 ]
 
-ltac_info: [
-| "Info" natural
+range_selector_list_comma: [
+| range_selector_list_comma "," range_selector
+| range_selector
 ]
 
-ltac_use_default: [
-| "."
-| "..."
+range_selector: [
+| num "-" num
+| num
 ]
 
-ltac_tactic_level: [
-| "(" "at" "level" natural ")"
+ltac_match_term: [
+| match_key ltac_expr "with" or_opt match_rule_list_or "end"
 ]
 
-ltac_production_sep: [
-| "," string
+match_key: [
+| "match"
+| "multimatch"
+| "lazymatch"
 ]
 
-ltac_production_item: [
-| string
-| ident "(" ident ltac_production_sep_opt ")"
-| ident
+match_rule_list_or: [
+| match_rule_list_or "|" match_rule
+| match_rule
 ]
 
-ltac_production_sep_opt: [
-| ltac_production_sep
-| empty
+match_rule: [
+| match_pattern_alt "=>" ltac_expr
 ]
 
-ltac_tacdef_body: [
-| tacdef_body
+match_pattern_alt: [
+| match_pattern
+| "_"
 ]
 
-firstorder_using: [
-| "using" reference
-| "using" reference "," reference_list_comma
-| "using" reference reference reference_list_opt
-| empty
+match_pattern: [
+| "context" ident_opt "[" term "]"
+| term
 ]
 
-reference_list_comma: [
-| reference_list_comma "," reference
-| reference
+ltac_match_goal: [
+| match_key reverse_opt "goal" "with" or_opt match_context_rule_list_or "end"
 ]
 
-numnotoption: [
+reverse_opt: [
+| "reverse"
 | 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 *)
+match_context_rule_list_or: [
+| match_context_rule_list_or "|" match_context_rule
+| match_context_rule
 ]
 
-ssrocc: [
-| natural natural_list_opt      (* ssr plugin *)
-| "-" natural_list_opt      (* ssr plugin *)
-| "+" natural_list_opt      (* ssr plugin *)
+match_context_rule: [
+| match_hyp_list_comma_opt "|-" match_pattern "=>" ltac_expr
+| "[" match_hyp_list_comma_opt "|-" match_pattern "]" "=>" ltac_expr
+| "_" "=>" ltac_expr
 ]
 
-natural_list_opt: [
-| natural_list_opt natural
+match_hyp_list_comma_opt: [
+| match_hyp_list_comma
 | 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 *)
+match_hyp_list_comma: [
+| match_hyp_list_comma "," match_hyp
+| match_hyp
 ]
 
-ssrdocc: [
-| "{" ssrocc "}"      (* ssr plugin *)
-| "{" ssrhyp_list_opt "}"      (* ssr plugin *)
+match_hyp: [
+| name ":" match_pattern
+| name ":=" match_pattern_opt match_pattern
 ]
 
-ssrhyp_list_opt: [
-| ssrhyp_list_opt ssrhyp
+match_pattern_opt: [
+| "[" match_pattern "]" ":"
 | 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
index a28d07636a..37197a1fec 100644
--- a/doc/tools/docgram/prodn.edit_mlg
+++ b/doc/tools/docgram/prodn.edit_mlg
@@ -12,3 +12,13 @@
 (* Contents used to generate prodn in doc *)
 
 DOC_GRAMMAR
+
+(* todo: doesn't work, gives
+ltac_match:  @match_key @ltac_expr with {? %| } {+| @ltac_expr } end
+instead of
+ltac_match:  @match_key @ltac_expr with {? %| } {+| {| @match_pattern | _ } => @ltac_expr } end
+
+SPLICE: [
+| match_rule
+]
+*)
diff --git a/doc/tools/docgram/productionlist.edit_mlg b/doc/tools/docgram/productionlist.edit_mlg
index 84acd07075..42d94e76bb 100644
--- a/doc/tools/docgram/productionlist.edit_mlg
+++ b/doc/tools/docgram/productionlist.edit_mlg
@@ -15,11 +15,42 @@ 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
+RENAME: [
+| name_alt names_tuple
+| binder_list binders
+| binder_list_opt binders_opt
+| typeclass_constraint_list_comma typeclass_constraints_comma
+| universe_expr_list_comma universe_exprs_comma
+| universe_level_list_opt universe_levels_opt
+| name_list names
+| name_list_comma names_comma
+| case_item_list_comma case_items_comma
+| eqn_list_or_opt eqns_or_opt
+| eqn_list_or eqns_or
+| pattern_list_or patterns_or
+| fix_body_list fix_bodies
+| arg_list args
+| arg_list_opt args_opt
+| evar_binding_list_semi evar_bindings_semi
 ]
 
-ltac_expr_opt2 : [ | DELETENT ]
-ltac_expr_list2_opt : [ | DELETENT ]
+binders_opt: [
+| REPLACE binders_opt binder
+| WITH binders
+]
+
+(* this is here because they're inside _opt generated by EXPAND *)
+SPLICE: [
+| ltac_info
+| eliminator
+| field_mods
+| ltac_production_sep
+| ltac_tactic_level
+| module_binder
+| printunivs_subgraph
+| quoted_attributes
+| ring_mods
+| scope_delimiter
+| univ_decl
+| univ_name_list
+]