Convert Ltac chapter to prodn

4 files changed, 547 insertions, 353 deletions

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 4d4ba28318..33c4bd3e01 100644
--- a/doc/tools/docgram/doc_grammar.ml
+++ b/doc/tools/docgram/doc_grammar.ml
@@ -779,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]
@@ -1828,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"
   ]
@@ -2059,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
 ]