Merge PR #12103: Convert Ltac chapter to prodn

6 files changed, 658 insertions, 401 deletions

diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py
index aec3607349..284c5d585a 100644
--- a/doc/tools/coqrst/coqdomain.py
+++ b/doc/tools/coqrst/coqdomain.py
@@ -131,12 +131,15 @@ class CoqObject(ObjectDescription):
         signature”); for example, the signature of the simplest form of the
         ``exact`` tactic is ``exact @id``.
 
-        Returns None by default, in which case no name will be automatically
-        generated.  This is a convenient way to automatically generate names
-        (link targets) without having to write explicit names everywhere.
+        Generates a name for the directive.  Override this method to return None
+        to avoid generating a name automatically.  This is a convenient way
+        to automatically generate names (link targets) without having to write
+        explicit names everywhere.
 
         """
-        return None
+        m = re.match(r"[a-zA-Z0-9_ ]+", signature)
+        if m:
+            return m.group(0).strip()
 
     def _render_signature(self, signature, signode):
         """Render a signature, placing resulting nodes into signode."""
@@ -343,7 +346,7 @@ class VernacVariantObject(VernacObject):
     def _name_from_signature(self, signature):
         return None
 
-class TacticNotationObject(NotationObject):
+class TacticObject(NotationObject):
     """A tactic, or a tactic notation.
 
     Example::
@@ -356,7 +359,7 @@ class TacticNotationObject(NotationObject):
     index_suffix = "(tactic)"
     annotation = "Tactic"
 
-class AttributeNotationObject(NotationObject):
+class AttributeObject(NotationObject):
     """An attribute.
 
     Example::
@@ -370,7 +373,7 @@ class AttributeNotationObject(NotationObject):
     def _name_from_signature(self, signature):
         return notation_to_string(signature)
 
-class TacticNotationVariantObject(TacticNotationObject):
+class TacticVariantObject(TacticObject):
     """A variant of a tactic.
 
     Example::
@@ -390,6 +393,9 @@ class TacticNotationVariantObject(TacticNotationObject):
     index_suffix = "(tactic variant)"
     annotation = "Variant"
 
+    def _name_from_signature(self, signature):
+        return None
+
 class OptionObject(NotationObject):
     """A Coq option (a setting with non-boolean value, e.g. a string or numeric value).
 
@@ -405,10 +411,6 @@ class OptionObject(NotationObject):
     index_suffix = "(option)"
     annotation = "Option"
 
-    def _name_from_signature(self, signature):
-        return notation_to_string(signature)
-
-
 class FlagObject(NotationObject):
     """A Coq flag (i.e. a boolean setting).
 
@@ -424,10 +426,6 @@ class FlagObject(NotationObject):
     index_suffix = "(flag)"
     annotation = "Flag"
 
-    def _name_from_signature(self, signature):
-        return notation_to_string(signature)
-
-
 class TableObject(NotationObject):
     """A Coq table, i.e. a setting that is a set of values.
 
@@ -442,9 +440,6 @@ class TableObject(NotationObject):
     index_suffix = "(table)"
     annotation = "Table"
 
-    def _name_from_signature(self, signature):
-        return notation_to_string(signature)
-
 class ProductionObject(CoqObject):
     r"""A grammar production.
 
@@ -1271,12 +1266,12 @@ class CoqDomain(Domain):
         # the same role.
         'cmd': VernacObject,
         'cmdv': VernacVariantObject,
-        'tacn': TacticNotationObject,
-        'tacv': TacticNotationVariantObject,
+        'tacn': TacticObject,
+        'tacv': TacticVariantObject,
         'opt': OptionObject,
         'flag': FlagObject,
         'table': TableObject,
-        'attr': AttributeNotationObject,
+        'attr': AttributeObject,
         'thm': GallinaObject,
         'prodn' : ProductionObject,
         'exn': ExceptionObject,
diff --git a/doc/tools/docgram/README.md b/doc/tools/docgram/README.md
index 4cde3809f0..2d29743d78 100644
--- a/doc/tools/docgram/README.md
+++ b/doc/tools/docgram/README.md
@@ -200,6 +200,11 @@ that appear in the specified production:
 `MOVETO <destination> <production>` - moves the production to `<destination>` and,
  if needed, creates a new production <edited_nt> -> \<destination>.
 
+
+`MOVEALLBUT <destination>` - moves all the productions in the nonterminal to `<destination>`
+*except* for the productions following the `MOVEALLBUT` production in the edit script
+(terminated only by the closing `]`).
+
 `OPTINREF` - verifies that <edited_nt> has an empty production.  If so, it removes
 the empty production and replaces all references to <edited_nt> throughout the
 grammar with `OPT <edited_nt>`
diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg
index a9a243868f..80f825358f 100644
--- a/doc/tools/docgram/common.edit_mlg
+++ b/doc/tools/docgram/common.edit_mlg
@@ -20,7 +20,7 @@ RENAME: [
 | Constr.constr_pattern constr_pattern
 | Constr.global global
 | Constr.lconstr lconstr
-| Constr.lconstr_pattern lconstr_pattern
+| Constr.lconstr_pattern cpattern
 | G_vernac.query_command query_command
 | G_vernac.section_subset_expr section_subset_expr
 | Pltac.tactic tactic
@@ -105,25 +105,24 @@ hyp: [
 | var
 ]
 
-ltac_expr_opt: [
-| OPT tactic_expr5
+tactic_then_last: [
+| REPLACE "|" LIST0 ( OPT tactic_expr5 ) SEP "|"
+| WITH LIST0 ( "|" ( OPT tactic_expr5 ) )
 ]
 
-ltac_expr_opt_list_or: [
-| ltac_expr_opt_list_or "|" ltac_expr_opt
-| ltac_expr_opt
+goal_tactics: [
+| LIST0 ( OPT tactic_expr5 ) SEP "|"
 ]
 
+tactic_then_gen: [ | DELETENT ]
+
 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 ".." OPT "|" ltac_expr_opt_list_or
+| goal_tactics
+| OPT ( goal_tactics "|" ) OPT tactic_expr5 ".." OPT ( "|" goal_tactics )
 ]
 
-ltac_expr_opt_list_or: [
-| ltac_expr_opt_list_or "|" OPT tactic_expr5
-| OPT tactic_expr5
+tactic_then_last: [
+| OPTINREF
 ]
 
 reference: [ | DELETENT ]
@@ -240,13 +239,29 @@ scope_name: [
 ]
 
 scope: [
-| scope_name | scope_key
+| scope_name
+| scope_key
+]
+
+scope_delimiter: [
+| REPLACE "%" IDENT
+| WITH "%" scope_key
+]
+
+type: [
+| operconstr200
 ]
 
 operconstr100: [
-| MOVETO term_cast operconstr99 "<:" operconstr200
-| MOVETO term_cast operconstr99 "<<:" operconstr200
-| MOVETO term_cast operconstr99 ":" operconstr200
+| REPLACE operconstr99 "<:" operconstr200
+| WITH operconstr99 "<:" type
+| MOVETO term_cast operconstr99 "<:" type
+| REPLACE operconstr99 "<<:" operconstr200
+| WITH operconstr99 "<<:" type
+| MOVETO term_cast operconstr99 "<<:" type
+| REPLACE operconstr99 ":" operconstr200
+| WITH operconstr99 ":" type
+| MOVETO term_cast operconstr99 ":" type
 | MOVETO term_cast operconstr99 ":>"
 ]
 
@@ -335,10 +350,6 @@ open_binders: [
 | DELETE closed_binder binders
 ]
 
-type: [
-| operconstr200
-]
-
 closed_binder: [
 | name
 
@@ -468,8 +479,10 @@ gallina: [
 | WITH "Let" "CoFixpoint" corec_definition LIST0 ( "with" corec_definition )
 | REPLACE "Scheme" LIST1 scheme SEP "with"
 | WITH "Scheme" scheme LIST0 ( "with" scheme )
-| REPLACE "Primitive" identref OPT [ ":" lconstr ] ":=" register_token
-| WITH "Primitive" identref OPT [ ":" lconstr ] ":=" "#" identref
+]
+
+finite_token: [
+| DELETENT
 ]
 
 constructor_list_or_record_decl: [
@@ -583,6 +596,10 @@ gallina_ext: [
 | REPLACE "Canonical" OPT "Structure" by_notation
 | WITH "Canonical" OPT "Structure" smart_global
 
+| DELETE "Coercion" global ":" class_rawexpr ">->" class_rawexpr
+| REPLACE "Coercion" by_notation ":" class_rawexpr ">->" class_rawexpr
+| WITH "Coercion" smart_global ":" class_rawexpr ">->" class_rawexpr
+
 | REPLACE "Include" "Type" module_type_inl LIST0 ext_module_type
 | WITH "Include" "Type" LIST1 module_type_inl SEP "<+"
 
@@ -619,8 +636,20 @@ digit: [
 | "0" ".." "9"
 ]
 
+decnum: [
+| digit LIST0 [ digit | "_" ]
+]
+
+hexdigit: [
+| [ "0" ".." "9" | "a" ".." "f" | "A" ".." "F" ]
+]
+
+hexnum: [
+| [ "0x" | "0X" ] hexdigit LIST0 [ hexdigit | "_" ]
+]
+
 num: [
-| LIST1 digit
+| [ decnum | hexnum ]
 ]
 
 natural: [ | DELETENT ]
@@ -628,12 +657,13 @@ natural: [
 | num  (* todo: or should it be "nat"? *)
 ]
 
-numeral: [
-| LIST1 digit OPT ("." LIST1 digit) OPT [ [ "e" | "E" ] OPT [ "+" | "-" ] LIST1 digit ]
+int: [
+| OPT "-" num
 ]
 
-int: [
-| OPT "-" LIST1 digit
+numeral: [
+| OPT "-" decnum OPT ( "." LIST1 [ digit | "_" ] ) OPT ( [ "e" | "E" ] OPT [ "+" | "-" ] decnum )
+| OPT "-" hexnum OPT ( "." LIST1 [ hexdigit | "_" ] ) OPT ( [ "p" | "P" ] OPT [ "+" | "-" ] decnum )
 ]
 
 bigint: [
@@ -675,32 +705,100 @@ 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"
-| REPLACE failkw [ int_or_var | ] LIST0 message_token
-| WITH failkw OPT int_or_var LIST0 message_token
-]
-
 DELETE: [
 | tactic_then_locality
 ]
 
+tactic_expr5: [
+(* make these look consistent with use of binder_tactic in other tactic_expr* *)
+| DELETE binder_tactic
+| DELETE tactic_expr4
+| [ tactic_expr4 | binder_tactic ]
+]
+
+ltac_constructs: [
+(* repeated in main ltac grammar - need to create a COPY edit *)
+| tactic_expr3 ";" [ tactic_expr3 | binder_tactic ]
+| tactic_expr3 ";" "[" tactic_then_gen "]"
+
+| tactic_expr1 "+" [ tactic_expr2 | binder_tactic ]
+| tactic_expr1 "||" [ tactic_expr2 | binder_tactic ]
+
+(* | qualid LIST0 tactic_arg  add later due renaming tactic_arg *)
+
+| "[>" tactic_then_gen "]"
+| toplevel_selector tactic_expr5
+]
+
 tactic_expr4: [
 | REPLACE tactic_expr3 ";" tactic_then_gen "]"
 | WITH tactic_expr3 ";" "[" tactic_then_gen "]"
-| tactic_expr3 ";" "[" ">" tactic_then_gen "]"
+| REPLACE tactic_expr3 ";" binder_tactic
+| WITH tactic_expr3 ";" [ tactic_expr3 | binder_tactic ]
+| DELETE tactic_expr3 ";" tactic_expr3
 ]
 
-match_context_list: [
-| EDIT ADD_OPT "|" LIST1 match_context_rule SEP "|"
+l3_tactic: [ ]
+
+tactic_expr3: [
+| DELETE "abstract" tactic_expr2
+| REPLACE "abstract" tactic_expr2 "using" ident
+| WITH "abstract" tactic_expr2 OPT ( "using" ident )
+| l3_tactic
+| MOVEALLBUT ltac_builtins
+| l3_tactic
+| tactic_expr2
+]
+
+l2_tactic: [ ]
+
+tactic_expr2: [
+| REPLACE tactic_expr1 "+" binder_tactic
+| WITH tactic_expr1 "+"  [ tactic_expr2 | binder_tactic ]
+| DELETE tactic_expr1 "+" tactic_expr2
+| REPLACE tactic_expr1 "||" binder_tactic
+| WITH tactic_expr1 "||" [ tactic_expr2 | binder_tactic ]
+| DELETE tactic_expr1 "||" tactic_expr2
+| MOVETO ltac_builtins "tryif" tactic_expr5 "then" tactic_expr5 "else" tactic_expr2
+| l2_tactic
+| DELETE ltac_builtins
 ]
 
-match_hyps: [
-| REPLACE name ":=" "[" match_pattern "]" ":" match_pattern
-| WITH name ":=" OPT ("[" match_pattern "]" ":") match_pattern
-| DELETE name ":=" match_pattern
+l1_tactic: [ ]
+
+tactic_expr1: [
+| EDIT match_key ADD_OPT "reverse" "goal" "with" match_context_list "end"
+| MOVETO simple_tactic match_key OPT "reverse" "goal" "with" match_context_list "end"
+| MOVETO simple_tactic match_key tactic_expr5 "with" match_list "end"
+| REPLACE failkw [ int_or_var | ] LIST0 message_token
+| WITH failkw OPT int_or_var LIST0 message_token
+| REPLACE reference LIST0 tactic_arg_compat
+| WITH reference LIST1 tactic_arg_compat
+| l1_tactic
+| DELETE simple_tactic
+| MOVEALLBUT ltac_builtins
+| l1_tactic
+| tactic_arg
+| reference LIST1 tactic_arg_compat
+| tactic_expr0
+]
+
+(* split match_context_rule *)
+goal_pattern: [
+| LIST0 match_hyps SEP "," "|-" match_pattern
+| "[" LIST0 match_hyps SEP "," "|-" match_pattern "]"
+| "_"
+]
+
+match_context_rule: [
+| DELETE LIST0 match_hyps SEP "," "|-" match_pattern "=>" tactic_expr5
+| DELETE "[" LIST0 match_hyps SEP "," "|-" match_pattern "]" "=>" tactic_expr5
+| DELETE "_" "=>" tactic_expr5
+| goal_pattern "=>" tactic_expr5
+]
+
+match_context_list: [
+| EDIT ADD_OPT "|" LIST1 match_context_rule SEP "|"
 ]
 
 match_list: [
@@ -708,12 +806,10 @@ match_list: [
 ]
 
 match_rule: [
-| REPLACE match_pattern "=>" tactic_expr5
-| WITH [ match_pattern | "_" ] "=>" tactic_expr5
+(* redundant; match_pattern -> term -> _ *)
 | 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 ","
@@ -892,7 +988,14 @@ simple_tactic: [
 | DELETE "congruence" "with" LIST1 constr
 | REPLACE "congruence" int "with" LIST1 constr
 | WITH "congruence" OPT int OPT ( "with" LIST1 constr )
-
+| DELETE "show" "ltac" "profile"
+| REPLACE "show" "ltac" "profile" "cutoff" int
+| WITH "show" "ltac" "profile" OPT [ "cutoff" int | string ]
+| DELETE "show" "ltac" "profile" string
+(* perversely, the mlg uses "tactic3" instead of "tactic_expr3" *)
+| DELETE "transparent_abstract" tactic3
+| REPLACE "transparent_abstract" tactic3 "using" ident
+| WITH "transparent_abstract" tactic_expr3 OPT ( "using" ident )
 ]
 
 (* todo: don't use DELETENT for this *)
@@ -1112,10 +1215,7 @@ numnotoption: [
 binder_tactic: [
 | REPLACE "let" [ "rec" | ] LIST1 let_clause SEP "with" "in" tactic_expr5
 | WITH "let" OPT "rec" let_clause LIST0 ( "with" let_clause ) "in" tactic_expr5
-]
-
-tactic_then_gen: [
-| OPTINREF
+| MOVEALLBUT ltac_builtins
 ]
 
 record_binder_body: [
@@ -1496,11 +1596,6 @@ by_notation: [
 | WITH ne_string OPT [ "%" scope_key ]
 ]
 
-scope_delimiter: [
-| REPLACE "%" IDENT
-| WITH "%" scope_key
-]
-
 decl_notation: [
 | REPLACE ne_lstring ":=" constr only_parsing OPT [ ":" IDENT ]
 | WITH ne_lstring ":=" constr only_parsing OPT [ ":" scope_name ]
@@ -1517,6 +1612,186 @@ ltac_production_item: [
 | DELETE ident
 ]
 
+input_fun: [
+| DELETE ident
+| DELETE "_"
+| name
+]
+
+let_clause: [
+| DELETE identref ":=" tactic_expr5
+| REPLACE "_" ":=" tactic_expr5
+| WITH name  ":=" tactic_expr5
+]
+
+tactic_mode: [
+(* todo: make sure to document this production! *)
+(* deleting to allow splicing query_command into command *)
+| DELETE OPT toplevel_selector query_command
+| DELETE OPT ltac_selector OPT ltac_info tactic ltac_use_default
+| DELETE "par" ":" OPT ltac_info tactic ltac_use_default
+(* Ignore attributes (none apply) and "...". *)
+| ltac_info tactic
+| MOVETO command ltac_info tactic
+| DELETE command
+]
+
+RENAME: [
+| toplevel_selector toplevel_selector_temp
+]
+
+toplevel_selector: [
+| selector_body
+| "all"
+| "!"
+(* par is accepted even though it's not in the .mlg *)
+| "par"
+]
+
+toplevel_selector_temp: [
+| DELETE selector_body ":"
+| DELETE "all" ":"
+| DELETE "!" ":"
+| toplevel_selector ":"
+]
+
+(* not included in insertprodn; defined in rst with :production: *)
+control_command: [ ]
+
+(* move all commands under "command" *)
+
+DELETE: [
+| vernac
+]
+
+vernac_aux: [
+| DELETE gallina "."
+| DELETE gallina_ext "."
+| DELETE syntax "."
+| DELETE command_entry
+]
+
+command: [
+| gallina
+| gallina_ext
+| syntax
+| query_command
+| vernac_control
+| vernac_toplevel
+| command_entry
+]
+
+SPLICE: [
+| query_command
+]
+
+query_command: [ ] (* re-add as a placeholder *)
+
+sentence: [
+| OPT attributes command "."
+| OPT attributes OPT ( num ":" ) query_command "."
+| OPT attributes OPT ( toplevel_selector ":" ) tactic_expr5 [ "." | "..." ]
+| control_command
+]
+
+document: [
+| LIST0 sentence
+]
+
+(* add in ltac and Tactic Notation tactics that appear in the doc: *)
+ltac_defined_tactics: [
+| "classical_left"
+| "classical_right"
+| "contradict" ident
+| "discrR"
+| "easy"
+| "exfalso"
+| "inversion_sigma"
+| "lia"
+| "lra"
+| "nia"
+| "nra"
+| "split_Rabs"
+| "split_Rmult"
+| "tauto"
+| "time_constr" tactic_expr5
+| "zify"
+]
+
+(* todo: need careful review; assume that "[" ... "]" are literals *)
+tactic_notation_tactics: [
+| "assert_fails" tactic_expr3
+| "assert_succeeds" tactic_expr3
+| "field" OPT ( "[" LIST1 operconstr200 "]" )
+| "field_simplify" OPT ( "[" LIST1 operconstr200 "]" ) LIST1 operconstr200 OPT ( "in" ident )
+| "field_simplify_eq" OPT ( "[" LIST1 operconstr200 "]" ) OPT ( "in" ident )
+| "intuition" OPT tactic_expr5
+| "nsatz" OPT ( "with" "radicalmax" ":=" operconstr200 "strategy" ":=" operconstr200 "parameters" ":=" operconstr200 "variables" ":=" operconstr200 )
+| "psatz" operconstr200 OPT int_or_var
+| "ring" OPT ( "[" LIST1 operconstr200 "]" )
+| "ring_simplify" OPT ( "[" LIST1 operconstr200 "]" ) LIST1 operconstr200 OPT ( "in" ident )  (* todo: ident was "hyp", worth keeping? *)
+]
+
+(* defined in OCaml outside of mlgs *)
+tactic_arg: [
+| "uconstr" ":" "(" operconstr200 ")"
+| MOVEALLBUT simple_tactic
+]
+
+nonterminal: [ ]
+
+value_tactic: [ ]
+
+RENAME: [
+| tactic_arg tactic_value
+]
+
+syn_value: [
+| IDENT; ":" "(" nonterminal ")"
+]
+
+tactic_value: [
+| [ value_tactic | syn_value ]
+]
+
+simple_tactic: [
+| ltac_builtins
+| ltac_constructs
+| ltac_defined_tactics
+| tactic_notation_tactics
+]
+
+tacdef_body: [
+| REPLACE global LIST1 input_fun ltac_def_kind tactic_expr5
+| WITH global LIST0 input_fun ltac_def_kind tactic_expr5
+| DELETE global ltac_def_kind tactic_expr5
+]
+
+SPLICE: [
+| def_token
+| extended_def_token
+]
+
+logical_kind: [
+| DELETE thm_token
+| DELETE assumption_token
+| [ thm_token | assumption_token ]
+| DELETE "Definition"
+| DELETE "Example"
+| DELETE "Context"
+| DELETE "Primitive"
+(* SubClass was deleted from def_token *)
+| [ "Definition" | "Example" | "Context" | "Primitive" ]
+| DELETE "Coercion"
+| DELETE "Instance"
+| DELETE "Scheme"
+| DELETE "Canonical"
+| [  "Coercion" | "Instance" | "Scheme" | "Canonical" | "SubClass" ]
+| DELETE "Field"
+| DELETE "Method"
+| [ "Field" | "Method" ]
+]
+
 SPLICE: [
 | noedit_mode
 | bigint
@@ -1595,7 +1870,6 @@ SPLICE: [
 | glob
 | glob_constr_with_bindings
 | id_or_meta
-| lconstr_pattern
 | lglob
 | ltac_tacdef_body
 | mode
@@ -1640,7 +1914,6 @@ SPLICE: [
 | quoted_attributes  (* todo: splice or not? *)
 | printable
 | only_parsing
-| def_token
 | record_fields
 | constructor_type
 | record_binder
@@ -1678,15 +1951,25 @@ SPLICE: [
 | ltac_def_kind
 | intropatterns
 | instance_name
+| failkw
+| selector
 | ne_in_or_out_modules
 | search_queries
 | locatable
 | scope_delimiter
 | bignat
 | one_import_filter_name
-| register_token
 | search_where
-| extended_def_token
+| message_token
+| input_fun
+| tactic_then_last
+| ltac_use_default
+| toplevel_selector_temp
+| comment
+| register_token
+| match_context_rule
+| match_rule
+| by_notation
 ] (* end SPLICE *)
 
 RENAME: [
@@ -1714,15 +1997,14 @@ RENAME: [
 (*| impl_ident_tail impl_ident*)
 | ssexpr35 ssexpr (* strange in mlg, ssexpr50 is after this *)
 
-| tactic_then_gen multi_goal_tactics
-| selector only_selector
+| tactic_then_gen for_each_goal
 | selector_body selector
-| input_fun fun_var
 | match_hyps match_hyp
 
 | BULLET bullet
 | fix_decl fix_body
 | cofix_decl cofix_body
+(* todo: it's confusing that Constr.constr and constr are different things *)
 | constr one_term
 | appl_arg arg
 | rec_definition fix_definition
@@ -1734,7 +2016,7 @@ RENAME: [
 | constructor_list_or_record_decl constructors_or_record
 | record_binder_body field_body
 | class_rawexpr class
-| smart_global smart_qualid
+| smart_global reference
 (*
 | searchabout_query search_item
 *)
@@ -1745,109 +2027,47 @@ RENAME: [
 | constr_as_binder_kind binder_interp
 | syntax_extension_type explicit_subentry
 | numnotoption numeral_modifier
-]
-
-(* todo: doesn't work if up above... maybe because 'clause' doesn't exist? *)
-clause_dft_concl: [
-| OPTINREF
-]
-
-(* add in ltac and Tactic Notation tactics that appear in the doc: *)
-ltac_defined_tactics: [
-| "classical_left"
-| "classical_right"
-| "contradict" ident
-| "discrR"
-| "easy"
-| "exfalso"
-| "inversion_sigma"
-| "lia"
-| "lra"
-| "nia"
-| "nra"
-| "split_Rabs"
-| "split_Rmult"
-| "tauto"
-| "zify"
-]
-
-(* todo: need careful review; assume that "[" ... "]" are literals *)
-tactic_notation_tactics: [
-| "assert_fails" ltac_expr3
-| "assert_succeeds" ltac_expr3
-| "field" OPT ( "[" LIST1 term "]" )
-| "field_simplify" OPT ( "[" LIST1 term "]" ) LIST1 term OPT ( "in" ident )
-| "field_simplify_eq" OPT ( "[" LIST1 term "]" ) OPT ( "in" ident )
-| "intuition" OPT ltac_expr
-| "nsatz" OPT ( "with" "radicalmax" ":=" term "strategy" ":=" term "parameters" ":=" term "variables" ":=" term )
-| "psatz" term OPT int_or_var
-| "ring" OPT ( "[" LIST1 term "]" )
-| "ring_simplify" OPT ( "[" LIST1 term "]" ) LIST1 term OPT ( "in" ident )  (* todo: ident was "hyp", worth keeping? *)
-]
-
-tacticals: [
+| tactic_arg_compat tactic_arg
+| lconstr_pattern cpattern
 ]
 
 simple_tactic: [
-| ltac_defined_tactics
-| tactic_notation_tactics
-]
-
-(* move all commands under "command" *)
-
-DELETE: [
-| vernac
+(* due to renaming of tactic_arg; Use LIST1 for function application *)
+| qualid LIST1 tactic_arg
 ]
 
-tactic_mode: [
-(* todo: make sure to document this production! *)
-(* deleting to allow splicing query_command into command *)
-| DELETE OPT toplevel_selector query_command
-]
-
-vernac_aux: [
-| DELETE gallina "."
-| DELETE gallina_ext "."
-| DELETE syntax "."
-| DELETE command_entry
-]
-
-command: [
-| gallina
-| gallina_ext
-| syntax
-| query_command
-| vernac_control
-| vernac_toplevel
-| command_entry
+(* todo: doesn't work if up above... maybe because 'clause' doesn't exist? *)
+clause_dft_concl: [
+| OPTINREF
 ]
 
 SPLICE: [
 | gallina
 | gallina_ext
 | syntax
-| query_command
 | vernac_control
 | vernac_toplevel
 | command_entry
+| ltac_builtins
+| ltac_constructs
 | ltac_defined_tactics
 | tactic_notation_tactics
 ]
 (* todo: ssrreflect*.rst ref to fix_body is incorrect *)
 
-(* not included in insertprodn; defined in rst with :production: *)
-control_command: [ ]
-query_command: [ ] (* re-add since previously spliced *)
+REACHABLE: [
+| command
+| simple_tactic
+]
 
-sentence: [
-| OPT attributes command "."
-| OPT attributes OPT ( num ":" ) query_command "."
-| OPT attributes OPT toplevel_selector ltac_expr [ "." | "..." ]
-| control_command
+NOTINRSTS: [
+| simple_tactic
+| REACHABLE
+| NOTINRSTS
 ]
 
-document: [
-| LIST0 sentence
+REACHABLE: [
+| NOTINRSTS
 ]
 
 strategy_level: [
diff --git a/doc/tools/docgram/doc_grammar.ml b/doc/tools/docgram/doc_grammar.ml
index 6d4c33f7be..33c4bd3e01 100644
--- a/doc/tools/docgram/doc_grammar.ml
+++ b/doc/tools/docgram/doc_grammar.ml
@@ -50,7 +50,7 @@ let default_args = {
   verify = false;
 }
 
-let start_symbols = ["document"]
+let start_symbols = ["document"; "REACHABLE"]
 let tokens = [ "bullet"; "string"; "unicode_id_part"; "unicode_letter" ]
 
 (* translated symbols *)
@@ -417,21 +417,34 @@ let add_symdef nt file symdef_map =
   in
   symdef_map := StringMap.add nt (Filename.basename file::ent) !symdef_map
 
-let rec edit_SELF nt cur_level next_level right_assoc prod =
+let rec edit_SELF nt cur_level next_level right_assoc inner prod =
+  let subedit sym = List.hd (edit_SELF nt cur_level next_level right_assoc true [sym]) in
   let len = List.length prod in
   List.mapi (fun i sym ->
     match sym with
-    | Snterm s -> begin match s with
-      | s when s = nt || s = "SELF" ->
-        if i = 0 then Snterm next_level
-        else if i+1 < len then sym
-        else if right_assoc then Snterm cur_level else Snterm next_level
-      | "NEXT" -> Snterm next_level
-      | _ -> sym
-    end
-    | Slist1 sym -> Slist1 (List.hd (edit_SELF nt cur_level next_level right_assoc [sym]))
-    | Slist0 sym -> Slist0 (List.hd (edit_SELF nt cur_level next_level right_assoc [sym]))
-    | x -> x)
+    | Sterm _ -> sym
+
+    | Snterm s when s = nt || s = "SELF"->
+      if inner then
+        Snterm nt (* first level *)
+      else if i = 0 then
+        Snterm next_level
+      else if i + 1 = len then
+        (if right_assoc then Snterm cur_level else Snterm next_level)
+      else
+        Snterm nt
+    | Snterm "NEXT" -> Snterm next_level
+    | Snterm _ -> sym
+
+    | Slist1 sym -> Slist1 (subedit sym)
+    | Slist0 sym -> Slist0 (subedit sym)
+    | Slist1sep (sym, sep) -> Slist1sep ((subedit sym), (subedit sep))
+    | Slist0sep (sym, sep) -> Slist0sep ((subedit sym), (subedit sep))
+    | Sopt sym -> Sopt (subedit sym)
+    | Sparen syms -> Sparen (List.map (fun sym -> subedit sym) syms)
+    | Sprod prods -> Sprod (List.map (fun prod -> edit_SELF nt cur_level next_level right_assoc true prod) prods)
+    | Sedit _ -> sym
+    | Sedit2 _ -> sym)
   prod
 
 
@@ -501,6 +514,7 @@ in
 let has_match p prods = List.exists (fun p2 -> ematch p p2) prods
 
 let plugin_regex = Str.regexp "^plugins/\\([a-zA-Z0-9_]+\\)/"
+let level_regex = Str.regexp "[a-zA-Z0-9_]*$"
 
 let read_mlg is_edit ast file level_renames symdef_map =
   let res = ref [] in
@@ -541,6 +555,10 @@ let read_mlg is_edit ast file level_renames symdef_map =
                   -> lev
                 (* Looks like FIRST/LAST can be ignored for documenting the current grammar *)
                 | _ -> "" in
+              if len > 1 && level = "" then
+                error "Missing level string for `%s`\n" nt
+              else if not (Str.string_match level_regex level 0) then
+                error "Invalid level string `%s` for `%s`\n" level nt;
               let cur_level = nt ^ level in
               let next_level = nt ^
                   if i+1 < len then (get_label (List.nth ent.gentry_rules (i+1)).grule_label) else "" in
@@ -552,7 +570,7 @@ let read_mlg is_edit ast file level_renames symdef_map =
               let cvted = List.map cvt_gram_prod rule.grule_prods in
               (* edit names for levels *)
               (* See https://camlp5.github.io/doc/html/grammars.html#b:Associativity *)
-              let edited = List.map (edit_SELF nt cur_level next_level right_assoc) cvted in
+              let edited = List.map (edit_SELF nt cur_level next_level right_assoc false) cvted in
               let prods_to_add =
                 if cur_level <> nt && i+1 < len then
                   edited @ [[Snterm next_level]]
@@ -761,7 +779,7 @@ let rec edit_prod g top edit_map prod =
         begin
           try let splice_prods = NTMap.find nt !g.map in
             match splice_prods with
-            | [] -> assert false
+            | [] -> error "Empty splice for '%s'\n" nt; []
             | [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]
@@ -1145,6 +1163,10 @@ let report_undef_nts g prod rec_nt =
     nts
 
 let apply_edit_file g edits =
+  let moveto src_nt dest_nt oprod prods =
+    g_add_prod_after g (Some src_nt) dest_nt oprod;
+    remove_prod oprod prods src_nt      (* remove orig prod *)
+  in
   List.iter (fun b ->
       let (nt, eprod) = b in
       if not (edit_all_prods g nt eprod) then begin
@@ -1158,17 +1180,26 @@ let apply_edit_file g edits =
               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
+          | (Snterm "MOVETO" :: Snterm dest_nt :: oprod) :: tl ->
+            let prods = try (* add "nt -> dest_nt" production *)
               let posn = find_first oprod prods nt in
-              let prods = if List.mem [Snterm nt2] prods then prods
-                else insert_after posn [[Snterm nt2]] prods (* insert new prod *)
-              in
-              remove_prod oprod prods nt      (* remove orig prod *)
-              with Not_found -> prods)
-            in
+              if List.mem [Snterm dest_nt] prods then prods
+                else insert_after posn [[Snterm dest_nt]] prods (* insert new prod *)
+            with Not_found -> prods in
+            let prods' = moveto nt dest_nt oprod prods in
             aux tl prods' add_nt
+          | [Snterm "MOVEALLBUT"; Snterm dest_nt] :: tl ->
+            List.iter (fun tlprod ->
+                if not (List.mem tlprod prods) then
+                  error "MOVEALLBUT for %s can't find '%s'\n" nt (prod_to_str tlprod))
+              tl;
+            let prods' = List.fold_left (fun prods oprod ->
+                if not (List.mem oprod tl) then begin
+                  moveto nt dest_nt oprod prods
+                end else
+                  prods)
+              prods prods in
+            prods', add_nt
           | (Snterm "OPTINREF" :: _) :: tl ->
             if not (has_match [] prods) then
               error "OPTINREF but no empty production for %s\n" nt;
@@ -1679,6 +1710,28 @@ type seen = {
   cmdvs: (string * int) NTMap.t;
 }
 
+(* Sphinx notations can't handle empty productions *)
+let has_empty_prod rhs =
+  let rec has_empty_prod_r rhs =
+    match rhs with
+      | [] -> false
+      | Sterm _ :: tl
+      | Snterm _ :: tl
+      | Sedit _ :: tl
+      | Sedit2 (_, _) :: tl ->  has_empty_prod_r tl
+
+      | Slist1 sym :: tl
+      | Slist0 sym :: tl
+      | Slist1sep (sym, _) :: tl
+      | Slist0sep (sym, _) :: tl
+      | Sopt sym :: tl ->  has_empty_prod_r [ sym ] ||  has_empty_prod_r tl
+
+      | Sparen prod :: tl -> List.length prod = 0 || has_empty_prod_r tl
+      | Sprod prods :: tl -> List.fold_left
+          (fun rv prod -> List.length prod = 0 || has_empty_prod_r tl || rv) false prods
+  in
+  List.length rhs = 0 || has_empty_prod_r rhs
+
 let process_rst g file args seen tac_prods cmd_prods =
   let old_rst = open_in file in
   let new_rst = open_temp_bin file in
@@ -1709,6 +1762,9 @@ let process_rst g file args seen tac_prods cmd_prods =
         List.iteri (fun i prod ->
             let rhs = String.trim (prod_to_prodn prod) in
             let sep = if i = 0 then " ::=" else "|" in
+            if has_empty_prod prod then
+              error "%s line %d: Empty (sub-)production for %s, edit to remove: '%s %s'\n"
+                file !linenum nt sep rhs;
             fprintf new_rst "%s   %s%s %s\n" indent (if i = 0 then nt else "") sep rhs)
           prods;
         if nt <> end_ then copy_prods tl
@@ -1772,10 +1828,10 @@ let process_rst g file args seen tac_prods cmd_prods =
     "doc/sphinx/language/core/sections.rst";
     "doc/sphinx/language/extensions/implicit-arguments.rst";
     "doc/sphinx/language/extensions/arguments-command.rst";
-    "doc/sphinx/language/using/libraries/funind.rst";
-
-    "doc/sphinx/language/gallina-specification-language.rst";
     "doc/sphinx/language/gallina-extensions.rst";
+    "doc/sphinx/language/gallina-specification-language.rst";
+    "doc/sphinx/language/using/libraries/funind.rst";
+    "doc/sphinx/proof-engine/ltac.rst";
     "doc/sphinx/proof-engine/vernacular-commands.rst";
     "doc/sphinx/user-extensions/syntax-extensions.rst"
   ]
@@ -1859,7 +1915,7 @@ let process_rst g file args seen tac_prods cmd_prods =
   close_out new_rst;
   finish_with_file file args
 
-let report_omitted_prods entries seen label split =
+let report_omitted_prods g seen label split =
   let maybe_warn first last n =
     if first <> "" then begin
       if first <> last then
@@ -1869,14 +1925,21 @@ let report_omitted_prods entries seen label split =
     end
   in
 
+  let included = try
+      List.map (fun prod ->
+        match prod with
+        | Snterm nt :: tl -> nt
+        | _ -> "") (NTMap.find "NOTINRSTS" !g.map)
+    with Not_found -> []
+  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
+      if NTMap.mem nt seen || (List.mem nt included) then begin
         maybe_warn first last n;
         "", "", 0, total
       end else
         (if first = "" then nt else first), nt, n + 1, total + 1)
-    ("", "", 0, 0) entries in
+    ("", "", 0, 0) !g.order in
   maybe_warn first last n;
   if total <> 0 then
     Printf.eprintf "TOTAL %ss not included = %d\n" label total
@@ -1954,7 +2017,7 @@ let process_grammar args =
       let tac_list, tac_prods = plist "simple_tactic" in
       let cmd_list, cmd_prods = plist "command" 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" "";
+      report_omitted_prods g !seen.nts "Nonterminal" "";
       let out = open_out (dir "updated_rsts") in
       close_out out;
     end;
@@ -1996,10 +2059,12 @@ let process_grammar args =
 
       let cmd_nts = ["command"] in
       (* TODO: need to handle tactic_mode (overlaps with query_command) and subprf *)
-      cmdReport "prodnCommands" "cmds" cmd_nts !seen.cmds !seen.cmdvs;
+      if args.check_cmds then
+        cmdReport "prodnCommands" "cmds" cmd_nts !seen.cmds !seen.cmdvs;
 
       let tac_nts = ["simple_tactic"] in
-      cmdReport "prodnTactics" "tacs" tac_nts !seen.tacs !seen.tacvs
+      if args.check_tacs then
+        cmdReport "prodnTactics" "tacs" tac_nts !seen.tacs !seen.tacvs
     end;
 
     (* generate prodnGrammar for reference *)
diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar
index 1b0a5c28ee..c5edb538b7 100644
--- a/doc/tools/docgram/fullGrammar
+++ b/doc/tools/docgram/fullGrammar
@@ -1425,7 +1425,7 @@ simple_tactic: [
 | "firstorder" OPT tactic firstorder_using "with" LIST1 preident
 | "gintuition" OPT tactic
 | "functional" "inversion" quantified_hypothesis OPT reference      (* funind plugin *)
-| "functional" "induction" LIST1 constr fun_ind_using with_names      (* funind plugin *)
+| "functional" "induction" lconstr fun_ind_using with_names      (* funind plugin *)
 | "soft" "functional" "induction" LIST1 constr fun_ind_using with_names      (* funind plugin *)
 | "reflexivity"
 | "exact" casted_constr
@@ -1591,7 +1591,6 @@ simple_tactic: [
 | "auto" OPT int_or_var auto_using hintbases
 | "info_auto" OPT int_or_var auto_using hintbases
 | "debug" "auto" OPT int_or_var auto_using hintbases
-| "prolog" "[" LIST0 uconstr "]" int_or_var
 | "eauto" OPT int_or_var OPT int_or_var auto_using hintbases
 | "new" "auto" OPT int_or_var auto_using hintbases
 | "debug" "eauto" OPT int_or_var OPT int_or_var auto_using hintbases
diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar
index 3a327fc748..f4bf51b6ba 100644
--- a/doc/tools/docgram/orderedGrammar
+++ b/doc/tools/docgram/orderedGrammar
@@ -4,14 +4,7 @@ to match editedGrammar, which will remove comments.  Not compiled into Coq *)
 DOC_GRAMMAR
 
 tactic_mode: [
-| OPT toplevel_selector "{"
-| OPT toplevel_selector OPT ( "Info" num ) ltac_expr ltac_use_default
-| "par" ":" OPT ( "Info" num ) ltac_expr ltac_use_default
-]
-
-ltac_use_default: [
-| "."
-| "..."
+| OPT ( toplevel_selector ":" ) "{"
 ]
 
 term: [
@@ -136,21 +129,34 @@ type: [
 ]
 
 numeral: [
-| LIST1 digit OPT ( "." LIST1 digit ) OPT [ [ "e" | "E" ] OPT [ "+" | "-" ] LIST1 digit ]
+| OPT "-" decnum OPT ( "." LIST1 [ digit | "_" ] ) OPT ( [ "e" | "E" ] OPT [ "+" | "-" ] decnum )
+| OPT "-" hexnum OPT ( "." LIST1 [ hexdigit | "_" ] ) OPT ( [ "p" | "P" ] OPT [ "+" | "-" ] decnum )
 ]
 
 int: [
-| OPT "-" LIST1 digit
+| OPT "-" num
 ]
 
 num: [
-| LIST1 digit
+| [ decnum | hexnum ]
+]
+
+decnum: [
+| digit LIST0 [ digit | "_" ]
 ]
 
 digit: [
 | "0" ".." "9"
 ]
 
+hexnum: [
+| [ "0x" | "0X" ] hexdigit LIST0 [ hexdigit | "_" ]
+]
+
+hexdigit: [
+| [ "0" ".." "9" | "a" ".." "f" | "A" ".." "F" ]
+]
+
 ident: [
 | first_letter LIST0 subsequent_letter
 ]
@@ -176,14 +182,29 @@ where: [
 | "before" ident
 ]
 
+REACHABLE: [
+| command
+| simple_tactic
+| NOTINRSTS
+]
+
+NOTINRSTS: [
+| simple_tactic
+| REACHABLE
+| NOTINRSTS
+]
+
 document: [
 | LIST0 sentence
 ]
 
+nonterminal: [
+]
+
 sentence: [
 | OPT attributes command "."
 | OPT attributes OPT ( num ":" ) query_command "."
-| OPT attributes OPT toplevel_selector ltac_expr [ "." | "..." ]
+| OPT attributes OPT ( toplevel_selector ":" ) ltac_expr [ "." | "..." ]
 | control_command
 ]
 
@@ -193,9 +214,6 @@ control_command: [
 query_command: [
 ]
 
-tacticals: [
-]
-
 attributes: [
 | LIST0 ( "#[" LIST0 attribute SEP "," "]" ) LIST0 legacy_attr
 ]
@@ -345,9 +363,9 @@ term_generalizing: [
 ]
 
 term_cast: [
-| term10 "<:" term
-| term10 "<<:" term
-| term10 ":" term
+| term10 "<:" type
+| term10 "<<:" type
+| term10 ":" type
 | term10 ":>"
 ]
 
@@ -440,7 +458,7 @@ red_expr: [
 ]
 
 delta_flag: [
-| OPT "-" "[" LIST1 smart_qualid "]"
+| OPT "-" "[" LIST1 reference "]"
 ]
 
 strategy_flag: [
@@ -459,7 +477,7 @@ red_flags: [
 ]
 
 ref_or_pattern_occ: [
-| smart_qualid OPT ( "at" occs_nums )
+| reference OPT ( "at" occs_nums )
 | one_term OPT ( "at" occs_nums )
 ]
 
@@ -474,22 +492,13 @@ int_or_var: [
 ]
 
 unfold_occ: [
-| smart_qualid OPT ( "at" occs_nums )
+| reference OPT ( "at" occs_nums )
 ]
 
 pattern_occ: [
 | one_term OPT ( "at" occs_nums )
 ]
 
-finite_token: [
-| "Inductive"
-| "CoInductive"
-| "Variant"
-| "Record"
-| "Structure"
-| "Class"
-]
-
 variant_definition: [
 | ident_decl LIST0 binder OPT [ "|" LIST0 binder ] OPT [ ":" type ] ":=" OPT "|" LIST1 constructor SEP "|" OPT decl_notations
 ]
@@ -538,11 +547,11 @@ cofix_definition: [
 ]
 
 scheme_kind: [
-| "Induction" "for" smart_qualid "Sort" sort_family
-| "Minimality" "for" smart_qualid "Sort" sort_family
-| "Elimination" "for" smart_qualid "Sort" sort_family
-| "Case" "for" smart_qualid "Sort" sort_family
-| "Equality" "for" smart_qualid
+| "Induction" "for" reference "Sort" sort_family
+| "Minimality" "for" reference "Sort" sort_family
+| "Elimination" "for" reference "Sort" sort_family
+| "Case" "for" reference "Sort" sort_family
+| "Equality" "for" reference
 ]
 
 sort_family: [
@@ -597,12 +606,8 @@ module_expr_inl: [
 | LIST1 module_expr_atom OPT functor_app_annot
 ]
 
-smart_qualid: [
+reference: [
 | qualid
-| by_notation
-]
-
-by_notation: [
 | string OPT [ "%" scope_key ]
 ]
 
@@ -679,9 +684,10 @@ command: [
 | "Cd" OPT string
 | "Load" OPT "Verbose" [ string | ident ]
 | "Declare" "ML" "Module" LIST1 string
-| "Locate" smart_qualid
-| "Locate" "Term" smart_qualid
+| "Locate" reference
+| "Locate" "Term" reference
 | "Locate" "Module" qualid
+| "Info" num ltac_expr
 | "Locate" "Ltac" qualid
 | "Locate" "Library" qualid
 | "Locate" "File" string
@@ -702,30 +708,30 @@ command: [
 | "Print" "Graph"
 | "Print" "Classes"
 | "Print" "TypeClasses"
-| "Print" "Instances" smart_qualid
+| "Print" "Instances" reference
 | "Print" "Coercions"
 | "Print" "Coercion" "Paths" class class
-| "Print" "Canonical" "Projections" LIST0 smart_qualid
+| "Print" "Canonical" "Projections" LIST0 reference
 | "Print" "Typing" "Flags"
 | "Print" "Tables"
 | "Print" "Options"
 | "Print" "Hint"
-| "Print" "Hint" smart_qualid
+| "Print" "Hint" reference
 | "Print" "Hint" "*"
 | "Print" "HintDb" ident
 | "Print" "Scopes"
 | "Print" "Scope" scope_name
 | "Print" "Visibility" OPT scope_name
-| "Print" "Implicit" smart_qualid
+| "Print" "Implicit" reference
 | "Print" OPT "Sorted" "Universes" OPT ( "Subgraph" "(" LIST0 qualid ")" ) OPT string
-| "Print" "Assumptions" smart_qualid
-| "Print" "Opaque" "Dependencies" smart_qualid
-| "Print" "Transparent" "Dependencies" smart_qualid
-| "Print" "All" "Dependencies" smart_qualid
-| "Print" "Strategy" smart_qualid
+| "Print" "Assumptions" reference
+| "Print" "Opaque" "Dependencies" reference
+| "Print" "Transparent" "Dependencies" reference
+| "Print" "All" "Dependencies" reference
+| "Print" "Strategy" reference
 | "Print" "Strategies"
 | "Print" "Registered"
-| "Print" OPT "Term" smart_qualid OPT univ_name_list
+| "Print" OPT "Term" reference OPT univ_name_list
 | "Print" "Module" "Type" qualid
 | "Print" "Module" qualid
 | "Print" "Namespace" dirpath
@@ -771,7 +777,7 @@ command: [
 | "Create" "HintDb" ident OPT "discriminated"
 | "Remove" "Hints" LIST1 qualid OPT ( ":" LIST1 ident )
 | "Hint" hint OPT ( ":" LIST1 ident )
-| "Comments" LIST0 comment
+| "Comments" LIST0 [ one_term | string | num ]
 | "Declare" "Instance" ident_decl LIST0 binder ":" term OPT hint_info
 | "Declare" "Scope" scope_name
 | "Obligation" int OPT ( "of" ident ) OPT ( ":" term OPT ( "with" ltac_expr ) )
@@ -903,21 +909,20 @@ command: [
 | "Export" LIST1 filtered_import
 | "Include" module_type_inl LIST0 ( "<+" module_expr_inl )
 | "Include" "Type" LIST1 module_type_inl SEP "<+"
-| "Transparent" LIST1 smart_qualid
-| "Opaque" LIST1 smart_qualid
-| "Strategy" LIST1 [ strategy_level "[" LIST1 smart_qualid "]" ]
+| "Transparent" LIST1 reference
+| "Opaque" LIST1 reference
+| "Strategy" LIST1 [ strategy_level "[" LIST1 reference "]" ]
 | "Canonical" OPT "Structure" ident_decl def_body
-| "Canonical" OPT "Structure" smart_qualid
+| "Canonical" OPT "Structure" reference
 | "Coercion" qualid OPT univ_decl def_body
 | "Identity" "Coercion" ident ":" class ">->" class
-| "Coercion" qualid ":" class ">->" class
-| "Coercion" by_notation ":" class ">->" class
+| "Coercion" reference ":" class ">->" class
 | "Context" LIST1 binder
 | "Instance" OPT ( ident_decl LIST0 binder ) ":" term OPT hint_info OPT [ ":=" "{" LIST0 field_def "}" | ":=" term ]
 | "Existing" "Instance" qualid OPT hint_info
 | "Existing" "Instances" LIST1 qualid OPT [ "|" num ]
 | "Existing" "Class" qualid
-| "Arguments" smart_qualid LIST0 arg_specs LIST0 [ "," LIST0 implicits_alt ] OPT [ ":" LIST1 args_modifier SEP "," ]
+| "Arguments" reference LIST0 arg_specs LIST0 [ "," LIST0 implicits_alt ] OPT [ ":" LIST1 args_modifier SEP "," ]
 | "Implicit" [ "Type" | "Types" ] reserv_list
 | "Generalizable" [ [ "Variable" | "Variables" ] LIST1 ident | "All" "Variables" | "No" "Variables" ]
 | "Set" setting_name OPT [ int | string ]
@@ -936,7 +941,7 @@ command: [
 | "Eval" red_expr "in" term
 | "Compute" term
 | "Check" term
-| "About" smart_qualid OPT univ_name_list
+| "About" reference OPT univ_name_list
 | "SearchHead" one_term OPT ( [ "inside" | "outside" ] LIST1 qualid )
 | "SearchPattern" one_term OPT ( [ "inside" | "outside" ] LIST1 qualid )
 | "SearchRewrite" one_term OPT ( [ "inside" | "outside" ] LIST1 qualid )
@@ -990,12 +995,6 @@ setting_name: [
 | LIST1 ident
 ]
 
-comment: [
-| one_term
-| string
-| num
-]
-
 search_query: [
 | search_item
 | "-" search_query
@@ -1009,18 +1008,10 @@ search_item: [
 ]
 
 logical_kind: [
-| thm_token
-| assumption_token
-| "Context"
-| "Definition"
-| "Example"
-| "Coercion"
-| "Instance"
-| "Scheme"
-| "Canonical"
-| "Field"
-| "Method"
-| "Primitive"
+| [ thm_token | assumption_token ]
+| [ "Definition" | "Example" | "Context" | "Primitive" ]
+| [ "Coercion" | "Instance" | "Scheme" | "Canonical" | "SubClass" ]
+| [ "Field" | "Method" ]
 ]
 
 univ_name_list: [
@@ -1045,8 +1036,7 @@ hint: [
 ]
 
 tacdef_body: [
-| qualid LIST1 fun_var [ ":=" | "::=" ] ltac_expr
-| qualid [ ":=" | "::=" ] ltac_expr
+| qualid LIST0 name [ ":=" | "::=" ] ltac_expr
 ]
 
 ltac_production_item: [
@@ -1115,7 +1105,7 @@ eauto_search_strategy_name: [
 class: [
 | "Funclass"
 | "Sortclass"
-| smart_qualid
+| reference
 ]
 
 syntax_modifier: [
@@ -1204,6 +1194,38 @@ simple_tactic: [
 | "generalize" "dependent" one_term
 | "replace" one_term "with" one_term OPT clause_dft_concl OPT ( "by" ltac_expr3 )
 | "replace" OPT [ "->" | "<-" ] one_term OPT clause_dft_concl
+| "try" ltac_expr3
+| "do" int_or_var ltac_expr3
+| "timeout" int_or_var ltac_expr3
+| "time" OPT string ltac_expr3
+| "repeat" ltac_expr3
+| "progress" ltac_expr3
+| "once" ltac_expr3
+| "exactly_once" ltac_expr3
+| "infoH" ltac_expr3
+| "abstract" ltac_expr2 OPT ( "using" ident )
+| "only" selector ":" ltac_expr3
+| "tryif" ltac_expr "then" ltac_expr "else" ltac_expr2
+| "first" "[" LIST0 ltac_expr SEP "|" "]"
+| "solve" "[" LIST0 ltac_expr SEP "|" "]"
+| "idtac" LIST0 [ ident | string | int ]
+| [ "fail" | "gfail" ] OPT int_or_var LIST0 [ ident | string | int ]
+| "eval" red_expr "in" term
+| "context" ident "[" term "]"
+| "type" "of" term
+| "fresh" LIST0 [ string | qualid ]
+| "type_term" one_term
+| "numgoals"
+| "uconstr" ":" "(" term ")"
+| "fun" LIST1 name "=>" ltac_expr
+| "let" OPT "rec" let_clause LIST0 ( "with" let_clause ) "in" ltac_expr
+| "info" ltac_expr
+| ltac_expr3 ";" [ ltac_expr3 | binder_tactic ]
+| ltac_expr3 ";" "[" for_each_goal "]"
+| ltac_expr1 "+" [ ltac_expr2 | binder_tactic ]
+| ltac_expr1 "||" [ ltac_expr2 | binder_tactic ]
+| "[>" for_each_goal "]"
+| toplevel_selector ":" ltac_expr
 | "simplify_eq" OPT destruction_arg
 | "esimplify_eq" OPT destruction_arg
 | "discriminate" OPT destruction_arg
@@ -1242,8 +1264,7 @@ simple_tactic: [
 | "hresolve_core" "(" ident ":=" one_term ")" OPT ( "at" int_or_var ) "in" one_term
 | "hget_evar" int_or_var
 | "destauto" OPT ( "in" ident )
-| "transparent_abstract" ltac_expr3
-| "transparent_abstract" ltac_expr3 "using" ident
+| "transparent_abstract" ltac_expr3 OPT ( "using" ident )
 | "constr_eq" one_term one_term
 | "constr_eq_strict" one_term one_term
 | "constr_eq_nounivs" one_term one_term
@@ -1266,13 +1287,11 @@ simple_tactic: [
 | "guard" int_or_var comparison int_or_var
 | "decompose" "[" LIST1 one_term "]" one_term
 | "optimize_heap"
-| "with_strategy" strategy_level_or_var "[" LIST1 smart_qualid "]" ltac_expr3
+| "with_strategy" strategy_level_or_var "[" LIST1 reference "]" ltac_expr3
 | "start" "ltac" "profiling"
 | "stop" "ltac" "profiling"
 | "reset" "ltac" "profile"
-| "show" "ltac" "profile"
-| "show" "ltac" "profile" "cutoff" int
-| "show" "ltac" "profile" string
+| "show" "ltac" "profile" OPT [ "cutoff" int | string ]
 | "restart_timer" OPT string
 | "finish_timing" OPT ( "(" string ")" ) OPT string
 | "eassumption"
@@ -1283,7 +1302,6 @@ simple_tactic: [
 | "auto" OPT int_or_var OPT auto_using OPT hintbases
 | "info_auto" OPT int_or_var OPT auto_using OPT hintbases
 | "debug" "auto" OPT int_or_var OPT auto_using OPT hintbases
-| "prolog" "[" LIST0 one_term "]" int_or_var
 | "eauto" OPT int_or_var OPT int_or_var OPT auto_using OPT hintbases
 | "new" "auto" OPT int_or_var OPT auto_using OPT hintbases
 | "debug" "eauto" OPT int_or_var OPT int_or_var OPT auto_using OPT hintbases
@@ -1383,7 +1401,7 @@ simple_tactic: [
 | "firstorder" OPT ltac_expr firstorder_rhs
 | "gintuition" OPT ltac_expr
 | "functional" "inversion" [ ident | num ] OPT qualid      (* funind plugin *)
-| "functional" "induction" LIST1 one_term OPT fun_ind_using OPT with_names      (* funind plugin *)
+| "functional" "induction" term OPT fun_ind_using OPT with_names      (* funind plugin *)
 | "soft" "functional" "induction" LIST1 one_term OPT fun_ind_using OPT with_names      (* funind plugin *)
 | "psatz_Z" OPT int_or_var ltac_expr
 | "xlia" ltac_expr      (* micromega plugin *)
@@ -1407,6 +1425,8 @@ simple_tactic: [
 | "protect_fv" string OPT ( "in" ident )
 | "ring_lookup" ltac_expr0 "[" LIST0 one_term "]" LIST1 one_term      (* setoid_ring plugin *)
 | "field_lookup" ltac_expr "[" LIST0 one_term "]" LIST1 one_term      (* setoid_ring plugin *)
+| match_key OPT "reverse" "goal" "with" OPT "|" LIST1 ( goal_pattern "=>" ltac_expr ) SEP "|" "end"
+| match_key ltac_expr "with" OPT "|" LIST1 ( match_pattern "=>" ltac_expr ) SEP "|" "end"
 | "classical_left"
 | "classical_right"
 | "contradict" ident
@@ -1421,6 +1441,7 @@ simple_tactic: [
 | "split_Rabs"
 | "split_Rmult"
 | "tauto"
+| "time_constr" ltac_expr
 | "zify"
 | "assert_fails" ltac_expr3
 | "assert_succeeds" ltac_expr3
@@ -1432,6 +1453,7 @@ simple_tactic: [
 | "psatz" term OPT int_or_var
 | "ring" OPT ( "[" LIST1 term "]" )
 | "ring_simplify" OPT ( "[" LIST1 term "]" ) LIST1 term OPT ( "in" ident )
+| qualid LIST1 tactic_arg
 ]
 
 hloc: [
@@ -1676,134 +1698,67 @@ rewstrategy: [
 | "old_hints" ident
 ]
 
-ltac_expr: [
-| binder_tactic
-| ltac_expr4
+l3_tactic: [
 ]
 
-binder_tactic: [
-| "fun" LIST1 fun_var "=>" ltac_expr
-| "let" OPT "rec" let_clause LIST0 ( "with" let_clause ) "in" ltac_expr
-| "info" ltac_expr
+l2_tactic: [
 ]
 
-fun_var: [
-| ident
-| "_"
+l1_tactic: [
 ]
 
-let_clause: [
-| ident ":=" ltac_expr
-| "_" ":=" ltac_expr
-| ident LIST1 fun_var ":=" ltac_expr
+binder_tactic: [
 ]
 
-ltac_expr4: [
-| ltac_expr3 ";" binder_tactic
-| ltac_expr3 ";" ltac_expr3
-| ltac_expr3 ";" "[" OPT multi_goal_tactics "]"
-| ltac_expr3
-| ltac_expr3 ";" "[" ">" OPT multi_goal_tactics "]"
+value_tactic: [
 ]
 
-multi_goal_tactics: [
-| OPT ltac_expr "|" multi_goal_tactics
-| ltac_expr_opt ".." OPT "|" ltac_expr_opt_list_or
-| ltac_expr
+syn_value: [
+| ident ":" "(" nonterminal ")"
 ]
 
-ltac_expr_opt: [
-| OPT ltac_expr
+ltac_expr: [
+| [ ltac_expr4 | binder_tactic ]
 ]
 
-ltac_expr_opt_list_or: [
-| ltac_expr_opt_list_or "|" ltac_expr_opt
-| ltac_expr_opt
-| ltac_expr_opt_list_or "|" OPT ltac_expr
-| OPT ltac_expr
+ltac_expr4: [
+| ltac_expr3 ";" [ ltac_expr3 | binder_tactic ]
+| ltac_expr3 ";" "[" for_each_goal "]"
+| ltac_expr3
 ]
 
 ltac_expr3: [
-| "try" ltac_expr3
-| "do" int_or_var ltac_expr3
-| "timeout" int_or_var ltac_expr3
-| "time" OPT string ltac_expr3
-| "repeat" ltac_expr3
-| "progress" ltac_expr3
-| "once" ltac_expr3
-| "exactly_once" ltac_expr3
-| "infoH" ltac_expr3
-| "abstract" ltac_expr2
-| "abstract" ltac_expr2 "using" ident
-| only_selector ltac_expr3
+| l3_tactic
 | ltac_expr2
 ]
 
-only_selector: [
-| "only" selector ":"
-]
-
-selector: [
-| LIST1 range_selector SEP ","
-| "[" ident "]"
-]
-
-range_selector: [
-| num "-" num
-| num
-]
-
 ltac_expr2: [
-| ltac_expr1 "+" binder_tactic
-| ltac_expr1 "+" ltac_expr2
-| "tryif" ltac_expr "then" ltac_expr "else" ltac_expr2
-| ltac_expr1 "||" binder_tactic
-| ltac_expr1 "||" ltac_expr2
+| ltac_expr1 "+" [ ltac_expr2 | binder_tactic ]
+| ltac_expr1 "||" [ ltac_expr2 | binder_tactic ]
+| l2_tactic
 | ltac_expr1
 ]
 
 ltac_expr1: [
-| ltac_match_term
-| "first" "[" LIST0 ltac_expr SEP "|" "]"
-| "solve" "[" LIST0 ltac_expr SEP "|" "]"
-| "idtac" LIST0 message_token
-| failkw OPT int_or_var LIST0 message_token
-| ltac_match_goal
-| simple_tactic
-| tactic_arg
-| qualid LIST0 tactic_arg_compat
+| tactic_value
+| qualid LIST1 tactic_arg
+| l1_tactic
 | ltac_expr0
 ]
 
-message_token: [
-| ident
-| string
-| int
-]
-
-failkw: [
-| "fail"
-| "gfail"
+tactic_value: [
+| [ value_tactic | syn_value ]
 ]
 
 tactic_arg: [
-| "eval" red_expr "in" term
-| "context" ident "[" term "]"
-| "type" "of" term
-| "fresh" LIST0 [ string | qualid ]
-| "type_term" one_term
-| "numgoals"
-]
-
-tactic_arg_compat: [
-| tactic_arg
+| tactic_value
 | term
 | "()"
 ]
 
 ltac_expr0: [
 | "(" ltac_expr ")"
-| "[>" OPT multi_goal_tactics "]"
+| "[>" for_each_goal "]"
 | tactic_atom
 ]
 
@@ -1813,43 +1768,61 @@ tactic_atom: [
 | "()"
 ]
 
+let_clause: [
+| name ":=" ltac_expr
+| ident LIST1 name ":=" ltac_expr
+]
+
+for_each_goal: [
+| goal_tactics
+| OPT ( goal_tactics "|" ) OPT ltac_expr ".." OPT ( "|" goal_tactics )
+]
+
+goal_tactics: [
+| LIST0 ( OPT ltac_expr ) SEP "|"
+]
+
 toplevel_selector: [
-| selector ":"
-| "all" ":"
-| "!" ":"
+| selector
+| "all"
+| "!"
+| "par"
 ]
 
-ltac_match_term: [
-| match_key ltac_expr "with" OPT "|" LIST1 match_rule SEP "|" "end"
+selector: [
+| LIST1 range_selector SEP ","
+| "[" ident "]"
+]
+
+range_selector: [
+| num "-" num
+| num
 ]
 
 match_key: [
+| "lazymatch"
 | "match"
 | "multimatch"
-| "lazymatch"
-]
-
-match_rule: [
-| [ match_pattern | "_" ] "=>" ltac_expr
 ]
 
 match_pattern: [
-| "context" OPT ident "[" term "]"
-| term
+| cpattern
+| "context" OPT ident "[" cpattern "]"
 ]
 
-ltac_match_goal: [
-| match_key OPT "reverse" "goal" "with" OPT "|" LIST1 match_context_rule SEP "|" "end"
+cpattern: [
+| term
 ]
 
-match_context_rule: [
-| LIST0 match_hyp SEP "," "|-" match_pattern "=>" ltac_expr
-| "[" LIST0 match_hyp SEP "," "|-" match_pattern "]" "=>" ltac_expr
-| "_" "=>" ltac_expr
+goal_pattern: [
+| LIST0 match_hyp SEP "," "|-" match_pattern
+| "[" LIST0 match_hyp SEP "," "|-" match_pattern "]"
+| "_"
 ]
 
 match_hyp: [
 | name ":" match_pattern
-| name ":=" OPT ( "[" match_pattern "]" ":" ) match_pattern
+| name ":=" match_pattern
+| name ":=" "[" match_pattern "]" ":" match_pattern
 ]