Convert ltac2 chapter to use prodn, update syntax

4 files changed, 1751 insertions, 104 deletions

diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg
index 5cfde2cf2f..6625e07d05 100644
--- a/doc/tools/docgram/common.edit_mlg
+++ b/doc/tools/docgram/common.edit_mlg
@@ -54,6 +54,46 @@ SPLICE: [
 | G_TACTIC_in_clause
 ]
 
+RENAME: [
+| G_LTAC2_delta_flag ltac2_delta_flag
+| G_LTAC2_strategy_flag ltac2_strategy_flag
+| G_LTAC2_binder ltac2_binder
+| G_LTAC2_branches ltac2_branches
+| G_LTAC2_let_clause ltac2_let_clause
+| G_LTAC2_tactic_atom ltac2_tactic_atom
+| G_LTAC2_rewriter ltac2_rewriter
+| G_LTAC2_constr_with_bindings ltac2_constr_with_bindings
+| G_LTAC2_match_rule ltac2_match_rule
+| G_LTAC2_match_pattern ltac2_match_pattern
+| G_LTAC2_intropatterns ltac2_intropatterns
+| G_LTAC2_simple_intropattern ltac2_simple_intropattern
+| G_LTAC2_simple_intropattern_closed ltac2_simple_intropattern_closed
+| G_LTAC2_or_and_intropattern ltac2_or_and_intropattern
+| G_LTAC2_equality_intropattern ltac2_equality_intropattern
+| G_LTAC2_naming_intropattern ltac2_naming_intropattern
+| G_LTAC2_destruction_arg ltac2_destruction_arg
+| G_LTAC2_with_bindings ltac2_with_bindings
+| G_LTAC2_bindings ltac2_bindings
+| G_LTAC2_simple_binding ltac2_simple_binding
+| G_LTAC2_in_clause ltac2_in_clause
+| G_LTAC2_occs ltac2_occs
+| G_LTAC2_occs_nums ltac2_occs_nums
+| G_LTAC2_concl_occ ltac2_concl_occ
+| G_LTAC2_hypident_occ ltac2_hypident_occ
+| G_LTAC2_hypident ltac2_hypident
+| G_LTAC2_induction_clause ltac2_induction_clause
+| G_LTAC2_as_or_and_ipat ltac2_as_or_and_ipat
+| G_LTAC2_eqn_ipat ltac2_eqn_ipat
+| G_LTAC2_conversion ltac2_conversion
+| G_LTAC2_oriented_rewriter ltac2_oriented_rewriter
+| G_LTAC2_tactic_then_gen ltac2_tactic_then_gen
+| G_LTAC2_tactic_then_last ltac2_tactic_then_last
+| G_LTAC2_as_name ltac2_as_name
+| G_LTAC2_as_ipat ltac2_as_ipat
+| G_LTAC2_by_tactic ltac2_by_tactic
+| G_LTAC2_match_list ltac2_match_list
+]
+
 (* renames to eliminate qualified names
    put other renames at the end *)
 RENAME: [
@@ -64,7 +104,6 @@ RENAME: [
 | Constr.lconstr_pattern cpattern
 | G_vernac.query_command query_command
 | G_vernac.section_subset_expr section_subset_expr
-| Pltac.tactic tactic
 | Prim.ident ident
 | Prim.reference reference
 | Pvernac.Vernac_.main_entry vernac_control
@@ -109,6 +148,8 @@ DELETE: [
 | test_name_colon
 | test_pipe_closedcurly
 | ensure_fixannot
+| test_array_opening
+| test_array_closing
 
   (* SSR *)
 (* | ssr_null_entry *)
@@ -165,6 +206,26 @@ tactic_then_last: [
 | OPTINREF
 ]
 
+ltac2_tactic_then_last: [
+| REPLACE "|" LIST0 ( OPT tac2expr6 ) SEP "|"      (* Ltac2 plugin *)
+| WITH LIST0 (  "|" OPT tac2expr6 )  TAG Ltac2
+]
+
+ltac2_goal_tactics: [
+| LIST0 ( OPT tac2expr6 ) SEP "|"  TAG Ltac2
+]
+
+ltac2_tactic_then_gen: [ | DELETENT ]
+
+ltac2_tactic_then_gen: [
+| ltac2_goal_tactics  TAG Ltac2
+| OPT ( ltac2_goal_tactics "|" ) OPT tac2expr6 ".." OPT ( "|" ltac2_goal_tactics )  TAG Ltac2
+]
+
+ltac2_tactic_then_last: [
+| OPTINREF
+]
+
 reference: [ | DELETENT ]
 
 reference: [
@@ -340,6 +401,8 @@ operconstr0: [
 | MOVETO term_generalizing "`{" operconstr200 "}"
 | MOVETO term_generalizing "`(" operconstr200 ")"
 | MOVETO term_ltac "ltac" ":" "(" tactic_expr5 ")"
+| REPLACE "[" "|" array_elems "|" lconstr type_cstr "|" "]" univ_instance
+| WITH "[|" array_elems "|" lconstr type_cstr "|]" univ_instance
 ]
 
 fix_decls: [
@@ -582,9 +645,28 @@ delta_flag: [
 | OPTINREF
 ]
 
+ltac2_delta_flag: [
+| EDIT ADD_OPT "-" "[" refglobals "]"      (* Ltac2 plugin *)
+]
+
+ltac2_branches: [
+| EDIT ADD_OPT "|" LIST1 branch SEP "|"      (* Ltac2 plugin *)
+| OPTINREF
+]
+
+RENAME: [
+| red_flag ltac2_red_flag
+| red_flags red_flag
+]
+
+RENAME: [
+]
+
 strategy_flag: [
 | REPLACE OPT delta_flag
 | WITH delta_flag
+(*| REPLACE LIST1 red_flags
+| WITH LIST1 red_flag*)
 | (* empty *)
 | OPTINREF
 ]
@@ -872,7 +954,7 @@ simple_tactic: [
 | DELETE "autorewrite" "with" LIST1 preident clause "using" tactic
 | DELETE "autorewrite" "*" "with" LIST1 preident clause
 | REPLACE "autorewrite" "*" "with" LIST1 preident clause "using" tactic
-| WITH "autorewrite" OPT "*" "with" LIST1 preident clause_dft_concl OPT ( "using" tactic )
+| WITH "autorewrite" OPT "*" "with" LIST1 preident clause OPT ( "using" tactic )
 | DELETE "cofix" ident
 | REPLACE "cofix" ident "with" LIST1 cofixdecl
 | WITH "cofix" ident OPT ( "with" LIST1 cofixdecl )
@@ -931,7 +1013,7 @@ simple_tactic: [
 | DELETE "replace" "->" uconstr clause
 | DELETE "replace" "<-" uconstr clause
 | DELETE "replace" uconstr clause
-| "replace" orient uconstr clause_dft_concl   (* todo: fix 'clause' *)
+| "replace" orient uconstr clause
 | REPLACE "rewrite" "*" orient uconstr "in" hyp "at" occurrences by_arg_tac
 | WITH "rewrite" "*" orient uconstr OPT ( "in" hyp ) OPT ( "at" occurrences by_arg_tac )
 | DELETE "rewrite" "*" orient uconstr "in" hyp by_arg_tac
@@ -1194,6 +1276,7 @@ command: [
 | REPLACE "String" "Notation" reference reference reference ":" ident
 | WITH "String" "Notation" reference reference reference ":" scope_name
 
+| DELETE "Ltac2" ltac2_entry      (* was split up *)
 ]
 
 option_setting: [
@@ -1211,14 +1294,10 @@ syntax: [
 | WITH "Undelimit" "Scope" scope_name
 | REPLACE "Bind" "Scope" IDENT; "with" LIST1 class_rawexpr
 | WITH "Bind" "Scope" scope_name; "with" LIST1 class_rawexpr
-| REPLACE "Infix" ne_lstring ":=" constr [ "(" LIST1 syntax_modifier SEP "," ")" | ]   OPT [ ":" IDENT ]
-| WITH    "Infix" ne_lstring ":=" constr OPT [ "(" LIST1 syntax_modifier SEP "," ")" ] OPT [ ":" scope_name ]
-| REPLACE "Notation" lstring ":=" constr [ "(" LIST1 syntax_modifier SEP "," ")" | ]   OPT [ ":" IDENT ]
-| WITH    "Notation" lstring ":=" constr OPT [ "(" LIST1 syntax_modifier SEP "," ")" ] OPT [ ":" scope_name ]
-| REPLACE "Reserved" "Infix" ne_lstring [ "(" LIST1 syntax_modifier SEP "," ")" | ]
-| WITH    "Reserved" "Infix" ne_lstring OPT [ "(" LIST1 syntax_modifier SEP "," ")" ]
-| REPLACE "Reserved" "Notation" ne_lstring [ "(" LIST1 syntax_modifier SEP "," ")" | ]
-| WITH    "Reserved" "Notation" ne_lstring OPT [ "(" LIST1 syntax_modifier SEP "," ")" ]
+| REPLACE "Infix" ne_lstring ":=" constr syntax_modifiers   OPT [ ":" IDENT ]
+| WITH    "Infix" ne_lstring ":=" constr syntax_modifiers OPT [ ":" scope_name ]
+| REPLACE "Notation" lstring ":=" constr syntax_modifiers   OPT [ ":" IDENT ]
+| WITH    "Notation" lstring ":=" constr syntax_modifiers OPT [ ":" scope_name ]
 ]
 
 syntax_modifier: [
@@ -1489,8 +1568,33 @@ by_tactic: [
 ]
 
 rewriter: [
-| REPLACE [ "?" | LEFTQMARK ] constr_with_bindings_arg
-| WITH "?" constr_with_bindings_arg
+| DELETE "!" constr_with_bindings_arg
+| DELETE [ "?" | LEFTQMARK ] constr_with_bindings_arg
+| DELETE natural "!" constr_with_bindings_arg
+| DELETE natural [ "?" | LEFTQMARK ] constr_with_bindings_arg
+| DELETE natural constr_with_bindings_arg
+| DELETE constr_with_bindings_arg
+| OPT natural OPT [ "?" | "!" ] constr_with_bindings_arg
+]
+
+ltac2_rewriter: [
+| DELETE "!" ltac2_constr_with_bindings      (* Ltac2 plugin *)
+| DELETE [ "?" | LEFTQMARK ] ltac2_constr_with_bindings
+| DELETE lnatural "!" ltac2_constr_with_bindings      (* Ltac2 plugin *)
+| DELETE lnatural [ "?" | LEFTQMARK ] ltac2_constr_with_bindings
+| DELETE lnatural ltac2_constr_with_bindings      (* Ltac2 plugin *)
+| DELETE ltac2_constr_with_bindings      (* Ltac2 plugin *)
+| OPT natural OPT [ "?" | "!" ] ltac2_constr_with_bindings
+]
+
+tac2expr0: [
+| DELETE "(" ")"
+]
+
+tac2type_body: [
+| REPLACE ":=" tac2typ_knd      (* Ltac2 plugin *)
+| WITH [ ":=" | "::=" ] tac2typ_knd TAG Ltac2
+| DELETE "::=" tac2typ_knd      (* Ltac2 plugin *)
 ]
 
 intropattern_or_list_or: [
@@ -1556,6 +1660,12 @@ in_clause: [
 | DELETE LIST0 hypident_occ SEP ","
 ]
 
+ltac2_in_clause: [
+| REPLACE LIST0 ltac2_hypident_occ SEP "," "|-" ltac2_concl_occ      (* Ltac2 plugin *)
+| WITH LIST0 ltac2_hypident_occ SEP "," OPT ( "|-" ltac2_concl_occ )  TAG Ltac2
+| DELETE LIST0 ltac2_hypident_occ SEP ","      (* Ltac2 plugin *)
+]
+
 concl_occ: [
 | OPTINREF
 ]
@@ -1628,8 +1738,12 @@ by_notation: [
 ]
 
 decl_notation: [
-| REPLACE ne_lstring ":=" constr only_parsing OPT [ ":" IDENT ]
-| WITH ne_lstring ":=" constr only_parsing OPT [ ":" scope_name ]
+| REPLACE ne_lstring ":=" constr syntax_modifiers OPT [ ":" IDENT ]
+| WITH ne_lstring ":=" constr syntax_modifiers OPT [ ":" scope_name ]
+]
+
+syntax_modifiers: [
+| OPTINREF
 ]
 
 
@@ -1667,6 +1781,15 @@ tactic_mode: [
 | DELETE command
 ]
 
+sexpr: [
+| REPLACE syn_node      (* Ltac2 plugin *)
+| WITH name TAG Ltac2
+| REPLACE syn_node "(" LIST1 sexpr SEP "," ")"      (* Ltac2 plugin *)
+| WITH name "(" LIST1 sexpr SEP "," ")" TAG Ltac2
+]
+
+syn_node: [ | DELETENT ]
+
 RENAME: [
 | toplevel_selector toplevel_selector_temp
 ]
@@ -1785,9 +1908,24 @@ tactic_value: [
 | [ value_tactic | syn_value ]
 ]
 
+
+(* defined in Ltac2/Notations.v *)
+
+ltac2_match_key: [
+| "lazy_match!"
+| "match!"
+| "multi_match!"
+]
+
+ltac2_constructs: [
+| ltac2_match_key tac2expr6 "with" ltac2_match_list "end"
+| ltac2_match_key OPT "reverse" "goal" "with" gmatch_list "end"
+]
+
 simple_tactic: [
 | ltac_builtins
 | ltac_constructs
+| ltac2_constructs
 | ltac_defined_tactics
 | tactic_notation_tactics
 ]
@@ -1798,6 +1936,24 @@ tacdef_body: [
 | DELETE global ltac_def_kind tactic_expr5
 ]
 
+tac2def_typ: [
+| REPLACE "Type" rec_flag LIST1 tac2typ_def SEP "with"      (* Ltac2 plugin *)
+| WITH "Type" rec_flag tac2typ_def LIST0 ( "with" tac2typ_def ) TAG Ltac2
+]
+
+tac2def_val: [
+| REPLACE mut_flag rec_flag LIST1 tac2def_body SEP "with"      (* Ltac2 plugin *)
+| WITH mut_flag rec_flag tac2def_body LIST0 ( "with" tac2def_body ) TAG Ltac1
+]
+
+tac2alg_constructors: [
+| REPLACE "|" LIST1 tac2alg_constructor SEP "|"      (* Ltac2 plugin *)
+| WITH OPT "|" LIST1 tac2alg_constructor SEP "|" TAG Ltac2
+| DELETE LIST0 tac2alg_constructor SEP "|"      (* Ltac2 plugin *)
+| (* empty *)
+| OPTINREF
+]
+
 SPLICE: [
 | def_token
 | extended_def_token
@@ -1823,7 +1979,233 @@ logical_kind: [
 | [ "Field" | "Method" ]
 ]
 
+(* ltac2 *)
+
+DELETE: [
+| test_ltac1_env
+]
+
+mut_flag: [
+| OPTINREF
+]
+
+rec_flag: [
+| OPTINREF
+]
+
+ltac2_orient: [ | DELETENT ]
+
+ltac2_orient: [
+| orient
+]
+
 SPLICE: [
+| ltac2_orient
+]
+
+tac2typ_prm: [
+| OPTINREF
+]
+
+tac2type_body: [
+| OPTINREF
+]
+
+atomic_tac2pat: [
+| OPTINREF
+]
+
+tac2expr0: [
+(*
+| DELETE "(" ")" (* covered by "()" prodn *)
+| REPLACE "{" [  | LIST1 tac2rec_fieldexpr OPT ";" ] "}"
+| WITH "{" OPT ( LIST1 tac2rec_fieldexpr OPT ";" ) "}"
+*)
+]
+
+(* todo: should
+| tac2pat1 "," LIST0 tac2pat1 SEP ","
+use LIST1? *)
+
+SPLICE: [
+| tac2expr4
+]
+
+tac2expr3: [
+| REPLACE tac2expr2 "," LIST1 tac2expr2 SEP ","      (* Ltac2 plugin *)
+| WITH LIST1 tac2expr2 SEP "," TAG Ltac2
+| DELETE tac2expr2      (* Ltac2 plugin *)
+]
+
+tac2rec_fieldexprs: [
+| DELETE tac2rec_fieldexpr ";" tac2rec_fieldexprs
+| DELETE tac2rec_fieldexpr ";"
+| DELETE tac2rec_fieldexpr
+| LIST1 tac2rec_fieldexpr OPT ";"
+| OPTINREF
+]
+
+tac2rec_fields: [
+| DELETE tac2rec_field ";" tac2rec_fields
+| DELETE tac2rec_field ";"
+| DELETE tac2rec_field
+| LIST1 tac2rec_field SEP ";" OPT ";" TAG Ltac2
+| OPTINREF
+]
+
+(* todo: weird productions, ints only after an initial "-"??:
+  occs_nums: [
+  | LIST1 [ num | ident ]
+  | "-" [ num | ident ] LIST0 int_or_var
+*)
+ltac2_occs_nums: [
+| DELETE LIST1 nat_or_anti      (* Ltac2 plugin *)
+| REPLACE "-" nat_or_anti LIST0 nat_or_anti      (* Ltac2 plugin *)
+| WITH OPT "-" LIST1 nat_or_anti TAG Ltac2
+]
+
+syn_level: [
+| OPTINREF
+]
+
+ltac2_delta_flag: [
+| OPTINREF
+]
+
+ltac2_occs: [
+| OPTINREF
+]
+
+ltac2_concl_occ: [
+| OPTINREF
+]
+
+ltac2_with_bindings: [
+| OPTINREF
+]
+
+ltac2_as_or_and_ipat: [
+| OPTINREF
+]
+
+ltac2_eqn_ipat: [
+| OPTINREF
+]
+
+ltac2_as_name: [
+| OPTINREF
+]
+
+ltac2_as_ipat: [
+| OPTINREF
+]
+
+ltac2_by_tactic: [
+| OPTINREF
+]
+
+ltac2_entry: [
+| REPLACE tac2def_typ      (* Ltac2 plugin *)
+| WITH "Ltac2" tac2def_typ
+| REPLACE tac2def_syn      (* Ltac2 plugin *)
+| WITH "Ltac2" tac2def_syn
+| REPLACE tac2def_mut      (* Ltac2 plugin *)
+| WITH "Ltac2" tac2def_mut
+| REPLACE tac2def_val     (* Ltac2 plugin *)
+| WITH "Ltac2" tac2def_val
+| REPLACE tac2def_ext     (* Ltac2 plugin *)
+| WITH "Ltac2" tac2def_ext
+| "Ltac2" "Notation" [ string | lident ] ":=" tac2expr6 TAG Ltac2  (* variant *)
+| MOVEALLBUT command
+(* todo: MOVEALLBUT should ignore tag on "but" prodns *)
+]
+
+ltac2_match_list: [
+| EDIT ADD_OPT "|" LIST1 ltac2_match_rule SEP "|"      (* Ltac2 plugin *)
+]
+
+ltac2_or_and_intropattern: [
+| DELETE "(" ltac2_simple_intropattern ")"      (* Ltac2 plugin *)
+| REPLACE "(" ltac2_simple_intropattern "," LIST1 ltac2_simple_intropattern SEP "," ")"      (* Ltac2 plugin *)
+| WITH "(" LIST1 ltac2_simple_intropattern SEP "," ")" TAG Ltac2
+| REPLACE "(" ltac2_simple_intropattern "&" LIST1 ltac2_simple_intropattern SEP "&" ")"      (* Ltac2 plugin *)
+| WITH "(" LIST1 ltac2_simple_intropattern SEP "&" ")" TAG Ltac2
+]
+
+SPLICE: [
+| tac2def_val
+| tac2def_typ
+| tac2def_ext
+| tac2def_syn
+| tac2def_mut
+| mut_flag
+| rec_flag
+| locident
+| syn_level
+| tac2rec_fieldexprs
+| tac2type_body
+| tac2alg_constructors
+| tac2rec_fields
+| ltac2_binder
+| branch
+| anti
+]
+
+tac2expr5: [
+| REPLACE "let" OPT "rec" LIST1 ltac2_let_clause SEP "with" "in" tac2expr6      (* Ltac2 plugin *)
+| WITH "let" OPT "rec" ltac2_let_clause LIST0 ( "with" ltac2_let_clause ) "in" tac2expr6 TAG Ltac2
+| MOVETO simple_tactic "match" tac2expr5 "with" OPT ltac2_branches "end"      (* Ltac2 plugin *)
+| DELETE simple_tactic
+]
+
+RENAME: [
+| Prim.string string
+| Prim.integer int
+| Prim.qualid qualid
+| Prim.natural num
+]
+
+gmatch_list: [
+| EDIT ADD_OPT "|" LIST1 gmatch_rule SEP "|"      (* Ltac2 plugin *)
+]
+
+ltac2_quotations: [
+
+]
+
+ltac2_tactic_atom: [
+| MOVETO ltac2_quotations "constr" ":" "(" lconstr ")"      (* Ltac2 plugin *)
+| MOVETO ltac2_quotations "open_constr" ":" "(" lconstr ")"      (* Ltac2 plugin *)
+| MOVETO ltac2_quotations "ident" ":" "(" lident ")"      (* Ltac2 plugin *)
+| MOVETO ltac2_quotations "pattern" ":" "(" cpattern ")"      (* Ltac2 plugin *)
+| MOVETO ltac2_quotations "reference" ":" "(" globref ")"      (* Ltac2 plugin *)
+| MOVETO ltac2_quotations "ltac1" ":" "(" ltac1_expr_in_env ")"      (* Ltac2 plugin *)
+| MOVETO ltac2_quotations "ltac1val" ":" "(" ltac1_expr_in_env ")"      (* Ltac2 plugin *)
+]
+
+(* non-Ltac2 "clause" is really clause_dft_concl + there is an ltac2 "clause" *)
+ltac2_clause: [ ]
+
+clause: [
+| MOVEALLBUT ltac2_clause
+]
+
+clause: [
+| clause_dft_concl
+]
+
+q_clause: [
+| REPLACE clause
+| WITH ltac2_clause  TAG Ltac2
+]
+
+ltac2_induction_clause: [
+| REPLACE ltac2_destruction_arg OPT ltac2_as_or_and_ipat OPT ltac2_eqn_ipat OPT clause      (* Ltac2 plugin *)
+| WITH ltac2_destruction_arg OPT ltac2_as_or_and_ipat OPT ltac2_eqn_ipat OPT ltac2_clause  TAG Ltac2
+]
+
+SPLICE: [
+| clause
 | noedit_mode
 | bigint
 | match_list
@@ -1839,6 +2221,7 @@ SPLICE: [
 | pattern_ident
 | constr_eval  (* splices as multiple prods *)
 | tactic_then_last  (* todo: dependency on c.edit_mlg edit?? really useful? *)
+| ltac2_tactic_then_last
 | Prim.name
 | ltac_selector
 | Constr.ident
@@ -1993,7 +2376,6 @@ SPLICE: [
 | search_where
 | message_token
 | input_fun
-| tactic_then_last
 | ltac_use_default
 | toplevel_selector_temp
 | comment
@@ -2001,14 +2383,24 @@ SPLICE: [
 | match_context_rule
 | match_rule
 | by_notation
+| lnatural
+| nat_or_anti
+| globref
+| let_binder
+| refglobals (* Ltac2 *)
+| syntax_modifiers
+| array_elems
+| ltac2_expr
+| G_LTAC2_input_fun
+| ltac2_simple_intropattern_closed
+| ltac2_with_bindings
 ] (* end SPLICE *)
 
 RENAME: [
-| clause clause_dft_concl
-
 | 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 *)
+| ltac1_expr ltac_expr
 | tactic_expr5 ltac_expr
 | tactic_expr4 ltac_expr4
 | tactic_expr3 ltac_expr3
@@ -2029,6 +2421,7 @@ RENAME: [
 | ssexpr35 ssexpr (* strange in mlg, ssexpr50 is after this *)
 
 | tactic_then_gen for_each_goal
+| ltac2_tactic_then_gen ltac2_for_each_goal
 | selector_body selector
 | match_hyps match_hyp
 
@@ -2060,6 +2453,20 @@ RENAME: [
 | numnotoption numeral_modifier
 | tactic_arg_compat tactic_arg
 | lconstr_pattern cpattern
+| Pltac.tactic ltac_expr
+| sexpr ltac2_scope
+| tac2type5 ltac2_type
+| tac2type2 ltac2_type2
+| tac2type1 ltac2_type1
+| tac2type0 ltac2_type0
+| typ_param ltac2_typevar
+| tac2expr6 ltac2_expr
+| tac2expr5 ltac2_expr5
+| tac2expr3 ltac2_expr3
+| tac2expr2 ltac2_expr2
+| tac2expr1 ltac2_expr1
+| tac2expr0 ltac2_expr0
+| gmatch_list goal_match_list
 ]
 
 simple_tactic: [
@@ -2081,6 +2488,7 @@ SPLICE: [
 | command_entry
 | ltac_builtins
 | ltac_constructs
+| ltac2_constructs
 | ltac_defined_tactics
 | tactic_notation_tactics
 ]
@@ -2095,6 +2503,45 @@ NOTINRSTS: [
 | simple_tactic
 | REACHABLE
 | NOTINRSTS
+| l1_tactic
+| l2_tactic
+| l3_tactic
+| binder_tactic
+| value_tactic
+| ltac2_entry
+(* ltac2 syntactic classes *)
+| q_intropatterns
+| q_intropattern
+| q_ident
+| q_destruction_arg
+| q_with_bindings
+| q_bindings
+| q_strategy_flag
+| q_reference
+| q_clause
+| q_occurrences
+| q_induction_clause
+| q_conversion
+| q_rewriting
+| q_dispatch
+| q_hintdb
+| q_move_location
+| q_pose
+| q_assert
+| q_constr_matching
+| q_goal_matching
+
+(* todo: figure these out
+(*Warning: editedGrammar: Undefined symbol 'ltac1_expr' *)
+| dangling_pattern_extension_rule
+| vernac_aux
+| subprf
+| tactic_mode
+| tac2expr_in_env (* no refs *)
+| tac2mode (* no refs *)
+| ltac_use_default (* from tac2mode *)
+| tacticals
+*)
 ]
 
 REACHABLE: [
diff --git a/doc/tools/docgram/doc_grammar.ml b/doc/tools/docgram/doc_grammar.ml
index 0f8144cbcf..0ac652c0db 100644
--- a/doc/tools/docgram/doc_grammar.ml
+++ b/doc/tools/docgram/doc_grammar.ml
@@ -732,6 +732,8 @@ let rec edit_prod g top edit_map prod =
   let splice_prods = match prod with
     | Snterm nt :: [] when is_splice nt ->
       get_splice_prods nt
+    | Snterm nt :: Sedit2 ("TAG", _) :: [] when is_splice nt ->
+      get_splice_prods nt
     | _ -> []
   in
   if top && splice_prods <> [] then
@@ -1901,7 +1903,8 @@ let process_rst g file args seen tac_prods cmd_prods =
     "doc/sphinx/proof-engine/ltac.rst";
     "doc/sphinx/proof-engine/ltac2.rst";
     "doc/sphinx/proof-engine/vernacular-commands.rst";
-    "doc/sphinx/user-extensions/syntax-extensions.rst"
+    "doc/sphinx/user-extensions/syntax-extensions.rst";
+    "doc/sphinx/proof-engine/vernacular-commands.rst"
   ]
   in
 
diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar
index 4c76ad9dda..7f4e92fc37 100644
--- a/doc/tools/docgram/fullGrammar
+++ b/doc/tools/docgram/fullGrammar
@@ -117,9 +117,14 @@ operconstr0: [
 | "{|" record_declaration bar_cbrace
 | "{" binder_constr "}"
 | "`{" operconstr200 "}"
+| test_array_opening "[" "|" array_elems "|" lconstr type_cstr test_array_closing "|" "]" univ_instance
 | "`(" operconstr200 ")"
 ]
 
+array_elems: [
+| LIST0 lconstr SEP ";"
+]
+
 record_declaration: [
 | fields_def
 ]
@@ -650,6 +655,17 @@ command: [
 | "Show" "Ltac" "Profile" "CutOff" int
 | "Show" "Ltac" "Profile" string
 | "Show" "Lia" "Profile"      (* micromega plugin *)
+| "Add" "Zify" "InjTyp" constr      (* micromega plugin *)
+| "Add" "Zify" "BinOp" constr      (* micromega plugin *)
+| "Add" "Zify" "UnOp" constr      (* micromega plugin *)
+| "Add" "Zify" "CstOp" constr      (* micromega plugin *)
+| "Add" "Zify" "BinRel" constr      (* micromega plugin *)
+| "Add" "Zify" "PropOp" constr      (* micromega plugin *)
+| "Add" "Zify" "PropBinOp" constr      (* micromega plugin *)
+| "Add" "Zify" "PropUOp" constr      (* micromega plugin *)
+| "Add" "Zify" "BinOpSpec" constr      (* micromega plugin *)
+| "Add" "Zify" "UnOpSpec" constr      (* micromega plugin *)
+| "Add" "Zify" "Saturate" constr      (* micromega plugin *)
 | "Add" "InjTyp" constr      (* micromega plugin *)
 | "Add" "BinOp" constr      (* micromega plugin *)
 | "Add" "UnOp" constr      (* micromega plugin *)
@@ -658,7 +674,6 @@ command: [
 | "Add" "PropOp" constr      (* micromega plugin *)
 | "Add" "PropBinOp" 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 *)
@@ -667,6 +682,8 @@ command: [
 | "Show" "Zify" "UnOp"      (* micromega plugin *)
 | "Show" "Zify" "CstOp"      (* micromega plugin *)
 | "Show" "Zify" "BinRel"      (* micromega plugin *)
+| "Show" "Zify" "UnOpSpec"      (* micromega plugin *)
+| "Show" "Zify" "BinOpSpec"      (* micromega plugin *)
 | "Show" "Zify" "Spec"      (* micromega plugin *)
 | "Add" "Ring" ident ":" constr OPT ring_mods      (* setoid_ring plugin *)
 | "Print" "Rings"      (* setoid_ring plugin *)
@@ -674,6 +691,9 @@ command: [
 | "Print" "Fields"      (* setoid_ring plugin *)
 | "Numeral" "Notation" reference reference reference ":" ident numnotoption
 | "String" "Notation" reference reference reference ":" ident
+| "Ltac2" ltac2_entry      (* Ltac2 plugin *)
+| "Ltac2" "Eval" ltac2_expr      (* Ltac2 plugin *)
+| "Print" "Ltac2" reference      (* Ltac2 plugin *)
 ]
 
 reference_or_constr: [
@@ -785,7 +805,7 @@ gallina: [
 | "Combined" "Scheme" identref "from" LIST1 identref SEP ","
 | "Register" global "as" qualid
 | "Register" "Inline" global
-| "Primitive" identref OPT [ ":" lconstr ] ":=" register_token
+| "Primitive" ident_decl OPT [ ":" lconstr ] ":=" register_token
 | "Universe" LIST1 identref
 | "Universes" LIST1 identref
 | "Constraint" LIST1 univ_constraint SEP ","
@@ -866,7 +886,7 @@ reduce: [
 ]
 
 decl_notation: [
-| ne_lstring ":=" constr only_parsing OPT [ ":" IDENT ]
+| ne_lstring ":=" constr syntax_modifiers OPT [ ":" IDENT ]
 ]
 
 decl_sep: [
@@ -1347,12 +1367,12 @@ syntax: [
 | "Delimit" "Scope" IDENT; "with" IDENT
 | "Undelimit" "Scope" IDENT
 | "Bind" "Scope" IDENT; "with" LIST1 class_rawexpr
-| "Infix" ne_lstring ":=" constr [ "(" LIST1 syntax_modifier SEP "," ")" | ] OPT [ ":" IDENT ]
+| "Infix" ne_lstring ":=" constr syntax_modifiers OPT [ ":" IDENT ]
 | "Notation" identref LIST0 ident ":=" constr only_parsing
-| "Notation" lstring ":=" constr [ "(" LIST1 syntax_modifier SEP "," ")" | ] OPT [ ":" IDENT ]
+| "Notation" lstring ":=" constr syntax_modifiers OPT [ ":" IDENT ]
 | "Format" "Notation" STRING STRING STRING
-| "Reserved" "Infix" ne_lstring [ "(" LIST1 syntax_modifier SEP "," ")" | ]
-| "Reserved" "Notation" ne_lstring [ "(" LIST1 syntax_modifier SEP "," ")" | ]
+| "Reserved" "Infix" ne_lstring syntax_modifiers
+| "Reserved" "Notation" ne_lstring syntax_modifiers
 ]
 
 only_parsing: [
@@ -1381,6 +1401,11 @@ syntax_modifier: [
 | IDENT syntax_extension_type
 ]
 
+syntax_modifiers: [
+| "(" LIST1 syntax_modifier SEP "," ")"
+|
+]
+
 syntax_extension_type: [
 | "ident"
 | "global"
@@ -1987,7 +2012,6 @@ failkw: [
 binder_tactic: [
 | "fun" LIST1 input_fun "=>" tactic_expr5
 | "let" [ "rec" | ] LIST1 let_clause SEP "with" "in" tactic_expr5
-| "info" tactic_expr5
 ]
 
 tactic_arg_compat: [
@@ -2542,3 +2566,642 @@ numnotoption: [
 | "(" "abstract" "after" bignat ")"
 ]
 
+tac2pat1: [
+| Prim.qualid LIST1 tac2pat0      (* Ltac2 plugin *)
+| Prim.qualid      (* Ltac2 plugin *)
+| "[" "]"      (* Ltac2 plugin *)
+| tac2pat0 "::" tac2pat0      (* Ltac2 plugin *)
+| tac2pat0      (* Ltac2 plugin *)
+]
+
+tac2pat0: [
+| "_"      (* Ltac2 plugin *)
+| "()"      (* Ltac2 plugin *)
+| Prim.qualid      (* Ltac2 plugin *)
+| "(" atomic_tac2pat ")"      (* Ltac2 plugin *)
+]
+
+atomic_tac2pat: [
+|      (* Ltac2 plugin *)
+| tac2pat1 ":" tac2type5      (* Ltac2 plugin *)
+| tac2pat1 "," LIST0 tac2pat1 SEP ","      (* Ltac2 plugin *)
+| tac2pat1      (* Ltac2 plugin *)
+]
+
+tac2expr6: [
+| tac2expr5 ";" tac2expr6      (* Ltac2 plugin *)
+| tac2expr5      (* Ltac2 plugin *)
+]
+
+tac2expr5: [
+| "fun" LIST1 G_LTAC2_input_fun "=>" tac2expr6      (* Ltac2 plugin *)
+| "let" rec_flag LIST1 G_LTAC2_let_clause SEP "with" "in" tac2expr6      (* Ltac2 plugin *)
+| "match" tac2expr5 "with" G_LTAC2_branches "end"      (* Ltac2 plugin *)
+| tac2expr4      (* Ltac2 plugin *)
+]
+
+tac2expr4: [
+| tac2expr3      (* Ltac2 plugin *)
+]
+
+tac2expr3: [
+| tac2expr2 "," LIST1 tac2expr2 SEP ","      (* Ltac2 plugin *)
+| tac2expr2      (* Ltac2 plugin *)
+]
+
+tac2expr2: [
+| tac2expr1 "::" tac2expr2      (* Ltac2 plugin *)
+| tac2expr1      (* Ltac2 plugin *)
+]
+
+tac2expr1: [
+| tac2expr0 LIST1 tac2expr0      (* Ltac2 plugin *)
+| tac2expr0 ".(" Prim.qualid ")"      (* Ltac2 plugin *)
+| tac2expr0 ".(" Prim.qualid ")" ":=" tac2expr5      (* Ltac2 plugin *)
+| tac2expr0      (* Ltac2 plugin *)
+]
+
+tac2expr0: [
+| "(" tac2expr6 ")"      (* Ltac2 plugin *)
+| "(" tac2expr6 ":" tac2type5 ")"      (* Ltac2 plugin *)
+| "()"      (* Ltac2 plugin *)
+| "(" ")"      (* Ltac2 plugin *)
+| "[" LIST0 tac2expr5 SEP ";" "]"      (* Ltac2 plugin *)
+| "{" tac2rec_fieldexprs "}"      (* Ltac2 plugin *)
+| G_LTAC2_tactic_atom      (* Ltac2 plugin *)
+]
+
+G_LTAC2_branches: [
+|      (* Ltac2 plugin *)
+| "|" LIST1 branch SEP "|"      (* Ltac2 plugin *)
+| LIST1 branch SEP "|"      (* Ltac2 plugin *)
+]
+
+branch: [
+| tac2pat1 "=>" tac2expr6      (* Ltac2 plugin *)
+]
+
+rec_flag: [
+| "rec"      (* Ltac2 plugin *)
+|      (* Ltac2 plugin *)
+]
+
+mut_flag: [
+| "mutable"      (* Ltac2 plugin *)
+|      (* Ltac2 plugin *)
+]
+
+typ_param: [
+| "'" Prim.ident      (* Ltac2 plugin *)
+]
+
+G_LTAC2_tactic_atom: [
+| Prim.integer      (* Ltac2 plugin *)
+| Prim.string      (* Ltac2 plugin *)
+| Prim.qualid      (* Ltac2 plugin *)
+| "@" Prim.ident      (* Ltac2 plugin *)
+| "&" lident      (* Ltac2 plugin *)
+| "'" Constr.constr      (* Ltac2 plugin *)
+| "constr" ":" "(" Constr.lconstr ")"      (* Ltac2 plugin *)
+| "open_constr" ":" "(" Constr.lconstr ")"      (* Ltac2 plugin *)
+| "ident" ":" "(" lident ")"      (* Ltac2 plugin *)
+| "pattern" ":" "(" Constr.lconstr_pattern ")"      (* Ltac2 plugin *)
+| "reference" ":" "(" globref ")"      (* Ltac2 plugin *)
+| "ltac1" ":" "(" ltac1_expr_in_env ")"      (* Ltac2 plugin *)
+| "ltac1val" ":" "(" ltac1_expr_in_env ")"      (* Ltac2 plugin *)
+]
+
+ltac1_expr_in_env: [
+| test_ltac1_env LIST0 locident "|-" ltac1_expr      (* Ltac2 plugin *)
+| ltac1_expr      (* Ltac2 plugin *)
+]
+
+tac2expr_in_env: [
+| test_ltac1_env LIST0 locident "|-" tac2expr6      (* Ltac2 plugin *)
+| tac2expr6      (* Ltac2 plugin *)
+]
+
+G_LTAC2_let_clause: [
+| let_binder ":=" tac2expr6      (* Ltac2 plugin *)
+]
+
+let_binder: [
+| LIST1 G_LTAC2_input_fun      (* Ltac2 plugin *)
+]
+
+tac2type5: [
+| tac2type2 "->" tac2type5      (* Ltac2 plugin *)
+| tac2type2      (* Ltac2 plugin *)
+]
+
+tac2type2: [
+| tac2type1 "*" LIST1 tac2type1 SEP "*"      (* Ltac2 plugin *)
+| tac2type1      (* Ltac2 plugin *)
+]
+
+tac2type1: [
+| tac2type0 Prim.qualid      (* Ltac2 plugin *)
+| tac2type0      (* Ltac2 plugin *)
+]
+
+tac2type0: [
+| "(" LIST1 tac2type5 SEP "," ")" OPT Prim.qualid      (* Ltac2 plugin *)
+| typ_param      (* Ltac2 plugin *)
+| "_"      (* Ltac2 plugin *)
+| Prim.qualid      (* Ltac2 plugin *)
+]
+
+locident: [
+| Prim.ident      (* Ltac2 plugin *)
+]
+
+G_LTAC2_binder: [
+| "_"      (* Ltac2 plugin *)
+| Prim.ident      (* Ltac2 plugin *)
+]
+
+G_LTAC2_input_fun: [
+| tac2pat0      (* Ltac2 plugin *)
+]
+
+tac2def_body: [
+| G_LTAC2_binder LIST0 G_LTAC2_input_fun ":=" tac2expr6      (* Ltac2 plugin *)
+]
+
+tac2def_val: [
+| mut_flag rec_flag LIST1 tac2def_body SEP "with"      (* Ltac2 plugin *)
+]
+
+tac2def_mut: [
+| "Set" Prim.qualid OPT [ "as" locident ] ":=" tac2expr6      (* Ltac2 plugin *)
+]
+
+tac2typ_knd: [
+| tac2type5      (* Ltac2 plugin *)
+| "[" ".." "]"      (* Ltac2 plugin *)
+| "[" tac2alg_constructors "]"      (* Ltac2 plugin *)
+| "{" tac2rec_fields "}"      (* Ltac2 plugin *)
+]
+
+tac2alg_constructors: [
+| "|" LIST1 tac2alg_constructor SEP "|"      (* Ltac2 plugin *)
+| LIST0 tac2alg_constructor SEP "|"      (* Ltac2 plugin *)
+]
+
+tac2alg_constructor: [
+| Prim.ident      (* Ltac2 plugin *)
+| Prim.ident "(" LIST0 tac2type5 SEP "," ")"      (* Ltac2 plugin *)
+]
+
+tac2rec_fields: [
+| tac2rec_field ";" tac2rec_fields      (* Ltac2 plugin *)
+| tac2rec_field ";"      (* Ltac2 plugin *)
+| tac2rec_field      (* Ltac2 plugin *)
+|      (* Ltac2 plugin *)
+]
+
+tac2rec_field: [
+| mut_flag Prim.ident ":" tac2type5      (* Ltac2 plugin *)
+]
+
+tac2rec_fieldexprs: [
+| tac2rec_fieldexpr ";" tac2rec_fieldexprs      (* Ltac2 plugin *)
+| tac2rec_fieldexpr ";"      (* Ltac2 plugin *)
+| tac2rec_fieldexpr      (* Ltac2 plugin *)
+|      (* Ltac2 plugin *)
+]
+
+tac2rec_fieldexpr: [
+| Prim.qualid ":=" tac2expr1      (* Ltac2 plugin *)
+]
+
+tac2typ_prm: [
+|      (* Ltac2 plugin *)
+| typ_param      (* Ltac2 plugin *)
+| "(" LIST1 typ_param SEP "," ")"      (* Ltac2 plugin *)
+]
+
+tac2typ_def: [
+| tac2typ_prm Prim.qualid tac2type_body      (* Ltac2 plugin *)
+]
+
+tac2type_body: [
+|      (* Ltac2 plugin *)
+| ":=" tac2typ_knd      (* Ltac2 plugin *)
+| "::=" tac2typ_knd      (* Ltac2 plugin *)
+]
+
+tac2def_typ: [
+| "Type" rec_flag LIST1 tac2typ_def SEP "with"      (* Ltac2 plugin *)
+]
+
+tac2def_ext: [
+| "@" "external" locident ":" tac2type5 ":=" Prim.string Prim.string      (* Ltac2 plugin *)
+]
+
+syn_node: [
+| "_"      (* Ltac2 plugin *)
+| Prim.ident      (* Ltac2 plugin *)
+]
+
+sexpr: [
+| Prim.string      (* Ltac2 plugin *)
+| Prim.integer      (* Ltac2 plugin *)
+| syn_node      (* Ltac2 plugin *)
+| syn_node "(" LIST1 sexpr SEP "," ")"      (* Ltac2 plugin *)
+]
+
+syn_level: [
+|      (* Ltac2 plugin *)
+| ":" Prim.integer      (* Ltac2 plugin *)
+]
+
+tac2def_syn: [
+| "Notation" LIST1 sexpr syn_level ":=" tac2expr6      (* Ltac2 plugin *)
+]
+
+lident: [
+| Prim.ident      (* Ltac2 plugin *)
+]
+
+globref: [
+| "&" Prim.ident      (* Ltac2 plugin *)
+| Prim.qualid      (* Ltac2 plugin *)
+]
+
+anti: [
+| "$" Prim.ident      (* Ltac2 plugin *)
+]
+
+ident_or_anti: [
+| lident      (* Ltac2 plugin *)
+| "$" Prim.ident      (* Ltac2 plugin *)
+]
+
+lnatural: [
+| Prim.natural      (* Ltac2 plugin *)
+]
+
+q_ident: [
+| ident_or_anti      (* Ltac2 plugin *)
+]
+
+qhyp: [
+| anti      (* Ltac2 plugin *)
+| lnatural      (* Ltac2 plugin *)
+| lident      (* Ltac2 plugin *)
+]
+
+G_LTAC2_simple_binding: [
+| "(" qhyp ":=" Constr.lconstr ")"      (* Ltac2 plugin *)
+]
+
+G_LTAC2_bindings: [
+| test_lpar_idnum_coloneq LIST1 G_LTAC2_simple_binding      (* Ltac2 plugin *)
+| LIST1 Constr.constr      (* Ltac2 plugin *)
+]
+
+q_bindings: [
+| G_LTAC2_bindings      (* Ltac2 plugin *)
+]
+
+q_with_bindings: [
+| G_LTAC2_with_bindings      (* Ltac2 plugin *)
+]
+
+G_LTAC2_intropatterns: [
+| LIST0 nonsimple_intropattern      (* Ltac2 plugin *)
+]
+
+G_LTAC2_or_and_intropattern: [
+| "[" LIST1 G_LTAC2_intropatterns SEP "|" "]"      (* Ltac2 plugin *)
+| "()"      (* Ltac2 plugin *)
+| "(" G_LTAC2_simple_intropattern ")"      (* Ltac2 plugin *)
+| "(" G_LTAC2_simple_intropattern "," LIST1 G_LTAC2_simple_intropattern SEP "," ")"      (* Ltac2 plugin *)
+| "(" G_LTAC2_simple_intropattern "&" LIST1 G_LTAC2_simple_intropattern SEP "&" ")"      (* Ltac2 plugin *)
+]
+
+G_LTAC2_equality_intropattern: [
+| "->"      (* Ltac2 plugin *)
+| "<-"      (* Ltac2 plugin *)
+| "[=" G_LTAC2_intropatterns "]"      (* Ltac2 plugin *)
+]
+
+G_LTAC2_naming_intropattern: [
+| LEFTQMARK lident      (* Ltac2 plugin *)
+| "?$" lident      (* Ltac2 plugin *)
+| "?"      (* Ltac2 plugin *)
+| ident_or_anti      (* Ltac2 plugin *)
+]
+
+nonsimple_intropattern: [
+| G_LTAC2_simple_intropattern      (* Ltac2 plugin *)
+| "*"      (* Ltac2 plugin *)
+| "**"      (* Ltac2 plugin *)
+]
+
+G_LTAC2_simple_intropattern: [
+| G_LTAC2_simple_intropattern_closed      (* Ltac2 plugin *)
+]
+
+G_LTAC2_simple_intropattern_closed: [
+| G_LTAC2_or_and_intropattern      (* Ltac2 plugin *)
+| G_LTAC2_equality_intropattern      (* Ltac2 plugin *)
+| "_"      (* Ltac2 plugin *)
+| G_LTAC2_naming_intropattern      (* Ltac2 plugin *)
+]
+
+q_intropatterns: [
+| G_LTAC2_intropatterns      (* Ltac2 plugin *)
+]
+
+q_intropattern: [
+| G_LTAC2_simple_intropattern      (* Ltac2 plugin *)
+]
+
+nat_or_anti: [
+| lnatural      (* Ltac2 plugin *)
+| "$" Prim.ident      (* Ltac2 plugin *)
+]
+
+G_LTAC2_eqn_ipat: [
+| "eqn" ":" G_LTAC2_naming_intropattern      (* Ltac2 plugin *)
+|      (* Ltac2 plugin *)
+]
+
+G_LTAC2_with_bindings: [
+| "with" G_LTAC2_bindings      (* Ltac2 plugin *)
+|      (* Ltac2 plugin *)
+]
+
+G_LTAC2_constr_with_bindings: [
+| Constr.constr G_LTAC2_with_bindings      (* Ltac2 plugin *)
+]
+
+G_LTAC2_destruction_arg: [
+| lnatural      (* Ltac2 plugin *)
+| lident      (* Ltac2 plugin *)
+| G_LTAC2_constr_with_bindings      (* Ltac2 plugin *)
+]
+
+q_destruction_arg: [
+| G_LTAC2_destruction_arg      (* Ltac2 plugin *)
+]
+
+G_LTAC2_as_or_and_ipat: [
+| "as" G_LTAC2_or_and_intropattern      (* Ltac2 plugin *)
+|      (* Ltac2 plugin *)
+]
+
+G_LTAC2_occs_nums: [
+| LIST1 nat_or_anti      (* Ltac2 plugin *)
+| "-" nat_or_anti LIST0 nat_or_anti      (* Ltac2 plugin *)
+]
+
+G_LTAC2_occs: [
+| "at" G_LTAC2_occs_nums      (* Ltac2 plugin *)
+|      (* Ltac2 plugin *)
+]
+
+G_LTAC2_hypident: [
+| ident_or_anti      (* Ltac2 plugin *)
+| "(" "type" "of" ident_or_anti ")"      (* Ltac2 plugin *)
+| "(" "value" "of" ident_or_anti ")"      (* Ltac2 plugin *)
+]
+
+G_LTAC2_hypident_occ: [
+| G_LTAC2_hypident G_LTAC2_occs      (* Ltac2 plugin *)
+]
+
+G_LTAC2_in_clause: [
+| "*" G_LTAC2_occs      (* Ltac2 plugin *)
+| "*" "|-" G_LTAC2_concl_occ      (* Ltac2 plugin *)
+| LIST0 G_LTAC2_hypident_occ SEP "," "|-" G_LTAC2_concl_occ      (* Ltac2 plugin *)
+| LIST0 G_LTAC2_hypident_occ SEP ","      (* Ltac2 plugin *)
+]
+
+clause: [
+| "in" G_LTAC2_in_clause      (* Ltac2 plugin *)
+| "at" G_LTAC2_occs_nums      (* Ltac2 plugin *)
+]
+
+q_clause: [
+| clause      (* Ltac2 plugin *)
+]
+
+G_LTAC2_concl_occ: [
+| "*" G_LTAC2_occs      (* Ltac2 plugin *)
+|      (* Ltac2 plugin *)
+]
+
+G_LTAC2_induction_clause: [
+| G_LTAC2_destruction_arg G_LTAC2_as_or_and_ipat G_LTAC2_eqn_ipat OPT clause      (* Ltac2 plugin *)
+]
+
+q_induction_clause: [
+| G_LTAC2_induction_clause      (* Ltac2 plugin *)
+]
+
+G_LTAC2_conversion: [
+| Constr.constr      (* Ltac2 plugin *)
+| Constr.constr "with" Constr.constr      (* Ltac2 plugin *)
+]
+
+q_conversion: [
+| G_LTAC2_conversion      (* Ltac2 plugin *)
+]
+
+ltac2_orient: [
+| "->"      (* Ltac2 plugin *)
+| "<-"      (* Ltac2 plugin *)
+|      (* Ltac2 plugin *)
+]
+
+G_LTAC2_rewriter: [
+| "!" G_LTAC2_constr_with_bindings      (* Ltac2 plugin *)
+| [ "?" | LEFTQMARK ] G_LTAC2_constr_with_bindings      (* Ltac2 plugin *)
+| lnatural "!" G_LTAC2_constr_with_bindings      (* Ltac2 plugin *)
+| lnatural [ "?" | LEFTQMARK ] G_LTAC2_constr_with_bindings      (* Ltac2 plugin *)
+| lnatural G_LTAC2_constr_with_bindings      (* Ltac2 plugin *)
+| G_LTAC2_constr_with_bindings      (* Ltac2 plugin *)
+]
+
+G_LTAC2_oriented_rewriter: [
+| ltac2_orient G_LTAC2_rewriter      (* Ltac2 plugin *)
+]
+
+q_rewriting: [
+| G_LTAC2_oriented_rewriter      (* Ltac2 plugin *)
+]
+
+G_LTAC2_tactic_then_last: [
+| "|" LIST0 ( OPT tac2expr6 ) SEP "|"      (* Ltac2 plugin *)
+|      (* Ltac2 plugin *)
+]
+
+G_LTAC2_tactic_then_gen: [
+| tac2expr6 "|" G_LTAC2_tactic_then_gen      (* Ltac2 plugin *)
+| tac2expr6 ".." G_LTAC2_tactic_then_last      (* Ltac2 plugin *)
+| ".." G_LTAC2_tactic_then_last      (* Ltac2 plugin *)
+| tac2expr6      (* Ltac2 plugin *)
+| "|" G_LTAC2_tactic_then_gen      (* Ltac2 plugin *)
+|      (* Ltac2 plugin *)
+]
+
+q_dispatch: [
+| G_LTAC2_tactic_then_gen      (* Ltac2 plugin *)
+]
+
+q_occurrences: [
+| G_LTAC2_occs      (* Ltac2 plugin *)
+]
+
+red_flag: [
+| "beta"      (* Ltac2 plugin *)
+| "iota"      (* Ltac2 plugin *)
+| "match"      (* Ltac2 plugin *)
+| "fix"      (* Ltac2 plugin *)
+| "cofix"      (* Ltac2 plugin *)
+| "zeta"      (* Ltac2 plugin *)
+| "delta" G_LTAC2_delta_flag      (* Ltac2 plugin *)
+]
+
+refglobal: [
+| "&" Prim.ident      (* Ltac2 plugin *)
+| Prim.qualid      (* Ltac2 plugin *)
+| "$" Prim.ident      (* Ltac2 plugin *)
+]
+
+q_reference: [
+| refglobal      (* Ltac2 plugin *)
+]
+
+refglobals: [
+| LIST1 refglobal      (* Ltac2 plugin *)
+]
+
+G_LTAC2_delta_flag: [
+| "-" "[" refglobals "]"      (* Ltac2 plugin *)
+| "[" refglobals "]"      (* Ltac2 plugin *)
+|      (* Ltac2 plugin *)
+]
+
+G_LTAC2_strategy_flag: [
+| LIST1 red_flag      (* Ltac2 plugin *)
+| G_LTAC2_delta_flag      (* Ltac2 plugin *)
+]
+
+q_strategy_flag: [
+| G_LTAC2_strategy_flag      (* Ltac2 plugin *)
+]
+
+hintdb: [
+| "*"      (* Ltac2 plugin *)
+| LIST1 ident_or_anti      (* Ltac2 plugin *)
+]
+
+q_hintdb: [
+| hintdb      (* Ltac2 plugin *)
+]
+
+G_LTAC2_match_pattern: [
+| "context" OPT Prim.ident "[" Constr.lconstr_pattern "]"      (* Ltac2 plugin *)
+| Constr.lconstr_pattern      (* Ltac2 plugin *)
+]
+
+G_LTAC2_match_rule: [
+| G_LTAC2_match_pattern "=>" tac2expr6      (* Ltac2 plugin *)
+]
+
+G_LTAC2_match_list: [
+| LIST1 G_LTAC2_match_rule SEP "|"      (* Ltac2 plugin *)
+| "|" LIST1 G_LTAC2_match_rule SEP "|"      (* Ltac2 plugin *)
+]
+
+q_constr_matching: [
+| G_LTAC2_match_list      (* Ltac2 plugin *)
+]
+
+gmatch_hyp_pattern: [
+| Prim.name ":" G_LTAC2_match_pattern      (* Ltac2 plugin *)
+]
+
+gmatch_pattern: [
+| "[" LIST0 gmatch_hyp_pattern SEP "," "|-" G_LTAC2_match_pattern "]"      (* Ltac2 plugin *)
+]
+
+gmatch_rule: [
+| gmatch_pattern "=>" tac2expr6      (* Ltac2 plugin *)
+]
+
+gmatch_list: [
+| LIST1 gmatch_rule SEP "|"      (* Ltac2 plugin *)
+| "|" LIST1 gmatch_rule SEP "|"      (* Ltac2 plugin *)
+]
+
+q_goal_matching: [
+| gmatch_list      (* Ltac2 plugin *)
+]
+
+move_location: [
+| "at" "top"      (* Ltac2 plugin *)
+| "at" "bottom"      (* Ltac2 plugin *)
+| "after" ident_or_anti      (* Ltac2 plugin *)
+| "before" ident_or_anti      (* Ltac2 plugin *)
+]
+
+q_move_location: [
+| move_location      (* Ltac2 plugin *)
+]
+
+G_LTAC2_as_name: [
+|      (* Ltac2 plugin *)
+| "as" ident_or_anti      (* Ltac2 plugin *)
+]
+
+pose: [
+| test_lpar_id_coloneq "(" ident_or_anti ":=" Constr.lconstr ")"      (* Ltac2 plugin *)
+| Constr.constr G_LTAC2_as_name      (* Ltac2 plugin *)
+]
+
+q_pose: [
+| pose      (* Ltac2 plugin *)
+]
+
+G_LTAC2_as_ipat: [
+| "as" G_LTAC2_simple_intropattern      (* Ltac2 plugin *)
+|      (* Ltac2 plugin *)
+]
+
+G_LTAC2_by_tactic: [
+| "by" tac2expr6      (* Ltac2 plugin *)
+|      (* Ltac2 plugin *)
+]
+
+assertion: [
+| test_lpar_id_coloneq "(" ident_or_anti ":=" Constr.lconstr ")"      (* Ltac2 plugin *)
+| test_lpar_id_colon "(" ident_or_anti ":" Constr.lconstr ")" G_LTAC2_by_tactic      (* Ltac2 plugin *)
+| Constr.constr G_LTAC2_as_ipat G_LTAC2_by_tactic      (* Ltac2 plugin *)
+]
+
+q_assert: [
+| assertion      (* Ltac2 plugin *)
+]
+
+ltac2_entry: [
+| tac2def_val      (* Ltac2 plugin *)
+| tac2def_typ      (* Ltac2 plugin *)
+| tac2def_ext      (* Ltac2 plugin *)
+| tac2def_syn      (* Ltac2 plugin *)
+| tac2def_mut      (* Ltac2 plugin *)
+]
+
+ltac2_expr: [
+| tac2expr6      (* Ltac2 plugin *)
+]
+
+tac2mode: [
+| ltac2_expr ltac_use_default      (* Ltac2 plugin *)
+| G_vernac.query_command      (* Ltac2 plugin *)
+]
+
diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar
index f4bf51b6ba..84efc1e36c 100644
--- a/doc/tools/docgram/orderedGrammar
+++ b/doc/tools/docgram/orderedGrammar
@@ -45,6 +45,7 @@ term0: [
 | term_match
 | term_record
 | term_generalizing
+| "[|" LIST0 term SEP ";" "|" term OPT ( ":" type ) "|]" OPT univ_annot
 | term_ltac
 | "(" term ")"
 ]
@@ -192,6 +193,32 @@ NOTINRSTS: [
 | simple_tactic
 | REACHABLE
 | NOTINRSTS
+| l1_tactic
+| l3_tactic
+| l2_tactic
+| binder_tactic
+| value_tactic
+| ltac2_entry
+| q_intropatterns
+| q_intropattern
+| q_ident
+| q_destruction_arg
+| q_with_bindings
+| q_bindings
+| q_strategy_flag
+| q_reference
+| q_clause
+| q_occurrences
+| q_induction_clause
+| q_conversion
+| q_rewriting
+| q_dispatch
+| q_hintdb
+| q_move_location
+| q_pose
+| q_assert
+| q_constr_matching
+| q_goal_matching
 ]
 
 document: [
@@ -462,11 +489,11 @@ delta_flag: [
 ]
 
 strategy_flag: [
-| LIST1 red_flags
+| LIST1 red_flag
 | delta_flag
 ]
 
-red_flags: [
+red_flag: [
 | "beta"
 | "iota"
 | "match"
@@ -751,6 +778,26 @@ command: [
 | "Declare" "Reduction" ident ":=" red_expr
 | "Declare" "Custom" "Entry" ident
 | "Derive" ident "SuchThat" one_term "As" ident      (* derive plugin *)
+| "Extraction" qualid      (* extraction plugin *)
+| "Recursive" "Extraction" LIST1 qualid      (* extraction plugin *)
+| "Extraction" string LIST1 qualid      (* extraction plugin *)
+| "Extraction" "TestCompile" LIST1 qualid      (* extraction plugin *)
+| "Separate" "Extraction" LIST1 qualid      (* extraction plugin *)
+| "Extraction" "Library" ident      (* extraction plugin *)
+| "Recursive" "Extraction" "Library" ident      (* extraction plugin *)
+| "Extraction" "Language" language      (* extraction plugin *)
+| "Extraction" "Inline" LIST1 qualid      (* extraction plugin *)
+| "Extraction" "NoInline" LIST1 qualid      (* extraction plugin *)
+| "Print" "Extraction" "Inline"      (* extraction plugin *)
+| "Reset" "Extraction" "Inline"      (* extraction plugin *)
+| "Extraction" "Implicit" qualid "[" LIST0 int_or_id "]"      (* extraction plugin *)
+| "Extraction" "Blacklist" LIST1 ident      (* extraction plugin *)
+| "Print" "Extraction" "Blacklist"      (* extraction plugin *)
+| "Reset" "Extraction" "Blacklist"      (* extraction plugin *)
+| "Extract" "Constant" qualid LIST0 string "=>" [ ident | string ]      (* extraction plugin *)
+| "Extract" "Inlined" "Constant" qualid "=>" [ ident | string ]      (* extraction plugin *)
+| "Extract" "Inductive" qualid "=>" [ ident | string ] "[" LIST0 [ ident | string ] "]" OPT string      (* extraction plugin *)
+| "Show" "Extraction"      (* extraction plugin *)
 | "Proof"
 | "Proof" "Mode" string
 | "Proof" term
@@ -807,6 +854,17 @@ command: [
 | "Reset" "Ltac" "Profile"
 | "Show" "Ltac" "Profile" OPT [ "CutOff" int | string ]
 | "Show" "Lia" "Profile"      (* micromega plugin *)
+| "Add" "Zify" "InjTyp" one_term      (* micromega plugin *)
+| "Add" "Zify" "BinOp" one_term      (* micromega plugin *)
+| "Add" "Zify" "UnOp" one_term      (* micromega plugin *)
+| "Add" "Zify" "CstOp" one_term      (* micromega plugin *)
+| "Add" "Zify" "BinRel" one_term      (* micromega plugin *)
+| "Add" "Zify" "PropOp" one_term      (* micromega plugin *)
+| "Add" "Zify" "PropBinOp" one_term      (* micromega plugin *)
+| "Add" "Zify" "PropUOp" one_term      (* micromega plugin *)
+| "Add" "Zify" "BinOpSpec" one_term      (* micromega plugin *)
+| "Add" "Zify" "UnOpSpec" one_term      (* micromega plugin *)
+| "Add" "Zify" "Saturate" one_term      (* micromega plugin *)
 | "Add" "InjTyp" one_term      (* micromega plugin *)
 | "Add" "BinOp" one_term      (* micromega plugin *)
 | "Add" "UnOp" one_term      (* micromega plugin *)
@@ -815,7 +873,6 @@ command: [
 | "Add" "PropOp" one_term      (* micromega plugin *)
 | "Add" "PropBinOp" one_term      (* micromega plugin *)
 | "Add" "PropUOp" one_term      (* micromega plugin *)
-| "Add" "Spec" one_term      (* micromega plugin *)
 | "Add" "BinOpSpec" one_term      (* micromega plugin *)
 | "Add" "UnOpSpec" one_term      (* micromega plugin *)
 | "Add" "Saturate" one_term      (* micromega plugin *)
@@ -824,8 +881,13 @@ command: [
 | "Show" "Zify" "UnOp"      (* micromega plugin *)
 | "Show" "Zify" "CstOp"      (* micromega plugin *)
 | "Show" "Zify" "BinRel"      (* micromega plugin *)
+| "Show" "Zify" "UnOpSpec"      (* micromega plugin *)
+| "Show" "Zify" "BinOpSpec"      (* micromega plugin *)
 | "Show" "Zify" "Spec"      (* micromega plugin *)
 | "Add" "Ring" ident ":" one_term OPT ( "(" LIST1 ring_mod SEP "," ")" )      (* setoid_ring plugin *)
+| "Print" "Rings"      (* setoid_ring plugin *)
+| "Add" "Field" ident ":" one_term OPT ( "(" LIST1 field_mod SEP "," ")" )      (* setoid_ring plugin *)
+| "Print" "Fields"      (* setoid_ring plugin *)
 | "Hint" "Cut" "[" hints_path "]" OPT ( ":" LIST1 ident )
 | "Typeclasses" "Transparent" LIST0 qualid
 | "Typeclasses" "Opaque" LIST0 qualid
@@ -841,26 +903,6 @@ command: [
 | "Print" "Firstorder" "Solver"
 | "Function" fix_definition LIST0 ( "with" fix_definition )
 | "Functional" "Scheme" fun_scheme_arg LIST0 ( "with" fun_scheme_arg )
-| "Extraction" qualid      (* extraction plugin *)
-| "Recursive" "Extraction" LIST1 qualid      (* extraction plugin *)
-| "Extraction" string LIST1 qualid      (* extraction plugin *)
-| "Extraction" "TestCompile" LIST1 qualid      (* extraction plugin *)
-| "Separate" "Extraction" LIST1 qualid      (* extraction plugin *)
-| "Extraction" "Library" ident      (* extraction plugin *)
-| "Recursive" "Extraction" "Library" ident      (* extraction plugin *)
-| "Extraction" "Language" language      (* extraction plugin *)
-| "Extraction" "Inline" LIST1 qualid      (* extraction plugin *)
-| "Extraction" "NoInline" LIST1 qualid      (* extraction plugin *)
-| "Print" "Extraction" "Inline"      (* extraction plugin *)
-| "Reset" "Extraction" "Inline"      (* extraction plugin *)
-| "Extraction" "Implicit" qualid "[" LIST0 int_or_id "]"      (* extraction plugin *)
-| "Extraction" "Blacklist" LIST1 ident      (* extraction plugin *)
-| "Print" "Extraction" "Blacklist"      (* extraction plugin *)
-| "Reset" "Extraction" "Blacklist"      (* extraction plugin *)
-| "Extract" "Constant" qualid LIST0 string "=>" [ ident | string ]      (* extraction plugin *)
-| "Extract" "Inlined" "Constant" qualid "=>" [ ident | string ]      (* extraction plugin *)
-| "Extract" "Inductive" qualid "=>" [ ident | string ] "[" LIST0 [ ident | string ] "]" OPT string      (* extraction plugin *)
-| "Show" "Extraction"      (* extraction plugin *)
 | "Functional" "Case" fun_scheme_arg      (* funind plugin *)
 | "Generate" "graph" "for" qualid      (* funind plugin *)
 | "Hint" "Rewrite" OPT [ "->" | "<-" ] LIST1 one_term OPT ( "using" ltac_expr ) OPT ( ":" LIST0 ident )
@@ -870,9 +912,6 @@ command: [
 | "Derive" "Dependent" "Inversion_clear" ident "with" one_term "Sort" sort_family
 | "Declare" "Left" "Step" one_term
 | "Declare" "Right" "Step" one_term
-| "Print" "Rings"      (* setoid_ring plugin *)
-| "Add" "Field" ident ":" one_term OPT ( "(" LIST1 field_mod SEP "," ")" )      (* setoid_ring plugin *)
-| "Print" "Fields"      (* setoid_ring plugin *)
 | "Numeral" "Notation" qualid qualid qualid ":" scope_name OPT numeral_modifier
 | "String" "Notation" qualid qualid qualid ":" scope_name
 | "SubClass" ident_decl def_body
@@ -889,7 +928,7 @@ command: [
 | "Combined" "Scheme" ident "from" LIST1 ident SEP ","
 | "Register" qualid "as" qualid
 | "Register" "Inline" qualid
-| "Primitive" ident OPT [ ":" term ] ":=" "#" ident
+| "Primitive" ident_decl OPT [ ":" term ] ":=" "#" ident
 | "Universe" LIST1 ident
 | "Universes" LIST1 ident
 | "Constraint" LIST1 univ_constraint SEP ","
@@ -932,12 +971,12 @@ command: [
 | "Delimit" "Scope" scope_name "with" scope_key
 | "Undelimit" "Scope" scope_name
 | "Bind" "Scope" scope_name "with" LIST1 class
-| "Infix" string ":=" one_term OPT [ "(" LIST1 syntax_modifier SEP "," ")" ] OPT [ ":" scope_name ]
+| "Infix" string ":=" one_term OPT ( "(" LIST1 syntax_modifier SEP "," ")" ) OPT [ ":" scope_name ]
 | "Notation" ident LIST0 ident ":=" one_term OPT ( "(" "only" "parsing" ")" )
-| "Notation" string ":=" one_term OPT [ "(" LIST1 syntax_modifier SEP "," ")" ] OPT [ ":" scope_name ]
+| "Notation" string ":=" one_term OPT ( "(" LIST1 syntax_modifier SEP "," ")" ) OPT [ ":" scope_name ]
 | "Format" "Notation" string string string
-| "Reserved" "Infix" string OPT [ "(" LIST1 syntax_modifier SEP "," ")" ]
-| "Reserved" "Notation" string OPT [ "(" LIST1 syntax_modifier SEP "," ")" ]
+| "Reserved" "Infix" string OPT ( "(" LIST1 syntax_modifier SEP "," ")" )
+| "Reserved" "Notation" string OPT ( "(" LIST1 syntax_modifier SEP "," ")" )
 | "Eval" red_expr "in" term
 | "Compute" term
 | "Check" term
@@ -946,6 +985,14 @@ command: [
 | "SearchPattern" one_term OPT ( [ "inside" | "outside" ] LIST1 qualid )
 | "SearchRewrite" one_term OPT ( [ "inside" | "outside" ] LIST1 qualid )
 | "Search" LIST1 ( search_query ) OPT ( [ "inside" | "outside" ] LIST1 qualid )
+| "Ltac2" OPT "mutable" OPT "rec" tac2def_body LIST0 ( "with" tac2def_body )
+| "Ltac2" "Type" OPT "rec" tac2typ_def LIST0 ( "with" tac2typ_def )
+| "Ltac2" "@" "external" ident ":" ltac2_type ":=" string string
+| "Ltac2" "Notation" LIST1 ltac2_scope OPT ( ":" int ) ":=" ltac2_expr
+| "Ltac2" "Set" qualid OPT [ "as" ident ] ":=" ltac2_expr
+| "Ltac2" "Notation" [ string | lident ] ":=" ltac2_expr      (* Ltac2 plugin *)
+| "Ltac2" "Eval" ltac2_expr      (* Ltac2 plugin *)
+| "Print" "Ltac2" qualid      (* Ltac2 plugin *)
 | "Time" sentence
 | "Redirect" string sentence
 | "Timeout" num sentence
@@ -1044,8 +1091,170 @@ ltac_production_item: [
 | ident OPT ( "(" ident OPT ( "," string ) ")" )
 ]
 
+tac2expr_in_env: [
+| LIST0 ident "|-" ltac2_expr      (* Ltac2 plugin *)
+| ltac2_expr      (* Ltac2 plugin *)
+]
+
+ltac2_type: [
+| ltac2_type2 "->" ltac2_type      (* Ltac2 plugin *)
+| ltac2_type2      (* Ltac2 plugin *)
+]
+
+ltac2_type2: [
+| ltac2_type1 "*" LIST1 ltac2_type1 SEP "*"      (* Ltac2 plugin *)
+| ltac2_type1      (* Ltac2 plugin *)
+]
+
+ltac2_type1: [
+| ltac2_type0 qualid      (* Ltac2 plugin *)
+| ltac2_type0      (* Ltac2 plugin *)
+]
+
+ltac2_type0: [
+| "(" LIST1 ltac2_type SEP "," ")" OPT qualid      (* Ltac2 plugin *)
+| ltac2_typevar      (* Ltac2 plugin *)
+| "_"      (* Ltac2 plugin *)
+| qualid      (* Ltac2 plugin *)
+]
+
+ltac2_typevar: [
+| "'" ident      (* Ltac2 plugin *)
+]
+
+lident: [
+| ident      (* Ltac2 plugin *)
+]
+
+destruction_arg: [
+| num
+| constr_with_bindings
+| constr_with_bindings_arg
+]
+
+constr_with_bindings_arg: [
+| ">" constr_with_bindings
+| constr_with_bindings
+]
+
+clause_dft_concl: [
+| "in" in_clause
+| OPT ( "at" occs_nums )
+]
+
+in_clause: [
+| "*" OPT ( "at" occs_nums )
+| "*" "|-" OPT concl_occ
+| LIST0 hypident_occ SEP "," OPT ( "|-" OPT concl_occ )
+]
+
+hypident_occ: [
+| hypident OPT ( "at" occs_nums )
+]
+
+hypident: [
+| ident
+| "(" "type" "of" ident ")"
+| "(" "value" "of" ident ")"
+]
+
+concl_occ: [
+| "*" OPT ( "at" occs_nums )
+]
+
+q_intropatterns: [
+| ltac2_intropatterns      (* Ltac2 plugin *)
+]
+
+ltac2_intropatterns: [
+| LIST0 nonsimple_intropattern      (* Ltac2 plugin *)
+]
+
+nonsimple_intropattern: [
+| "*"      (* Ltac2 plugin *)
+| "**"      (* Ltac2 plugin *)
+| ltac2_simple_intropattern      (* Ltac2 plugin *)
+]
+
+q_intropattern: [
+| ltac2_simple_intropattern      (* Ltac2 plugin *)
+]
+
+ltac2_simple_intropattern: [
+| ltac2_naming_intropattern      (* Ltac2 plugin *)
+| "_"      (* Ltac2 plugin *)
+| ltac2_or_and_intropattern      (* Ltac2 plugin *)
+| ltac2_equality_intropattern      (* Ltac2 plugin *)
+]
+
+ltac2_or_and_intropattern: [
+| "[" LIST1 ltac2_intropatterns SEP "|" "]"      (* Ltac2 plugin *)
+| "()"      (* Ltac2 plugin *)
+| "(" LIST1 ltac2_simple_intropattern SEP "," ")"      (* Ltac2 plugin *)
+| "(" LIST1 ltac2_simple_intropattern SEP "&" ")"      (* Ltac2 plugin *)
+]
+
+ltac2_equality_intropattern: [
+| "->"      (* Ltac2 plugin *)
+| "<-"      (* Ltac2 plugin *)
+| "[=" ltac2_intropatterns "]"      (* Ltac2 plugin *)
+]
+
+ltac2_naming_intropattern: [
+| "?" lident      (* Ltac2 plugin *)
+| "?$" lident      (* Ltac2 plugin *)
+| "?"      (* Ltac2 plugin *)
+| ident_or_anti      (* Ltac2 plugin *)
+]
+
+q_ident: [
+| ident_or_anti      (* Ltac2 plugin *)
+]
+
+ident_or_anti: [
+| lident      (* Ltac2 plugin *)
+| "$" ident      (* Ltac2 plugin *)
+]
+
+q_destruction_arg: [
+| ltac2_destruction_arg      (* Ltac2 plugin *)
+]
+
+ltac2_destruction_arg: [
+| num      (* Ltac2 plugin *)
+| lident      (* Ltac2 plugin *)
+| ltac2_constr_with_bindings      (* Ltac2 plugin *)
+]
+
+ltac2_constr_with_bindings: [
+| term OPT ( "with" ltac2_bindings )      (* Ltac2 plugin *)
+]
+
+q_bindings: [
+| ltac2_bindings      (* Ltac2 plugin *)
+]
+
+q_with_bindings: [
+| OPT ( "with" ltac2_bindings )      (* Ltac2 plugin *)
+]
+
+ltac2_bindings: [
+| LIST1 ltac2_simple_binding      (* Ltac2 plugin *)
+| LIST1 term      (* Ltac2 plugin *)
+]
+
+ltac2_simple_binding: [
+| "(" qhyp ":=" term ")"      (* Ltac2 plugin *)
+]
+
+qhyp: [
+| "$" ident      (* Ltac2 plugin *)
+| num      (* Ltac2 plugin *)
+| lident      (* Ltac2 plugin *)
+]
+
 int_or_id: [
-| ident      (* extraction plugin *)
+| ident
 | int      (* extraction plugin *)
 ]
 
@@ -1151,7 +1360,7 @@ decl_notations: [
 ]
 
 decl_notation: [
-| string ":=" one_term OPT ( "(" "only" "parsing" ")" ) OPT [ ":" scope_name ]
+| string ":=" one_term OPT ( "(" LIST1 syntax_modifier SEP "," ")" ) OPT [ ":" scope_name ]
 ]
 
 simple_tactic: [
@@ -1210,6 +1419,7 @@ simple_tactic: [
 | "solve" "[" LIST0 ltac_expr SEP "|" "]"
 | "idtac" LIST0 [ ident | string | int ]
 | [ "fail" | "gfail" ] OPT int_or_var LIST0 [ ident | string | int ]
+| "fun" LIST1 name "=>" ltac_expr
 | "eval" red_expr "in" term
 | "context" ident "[" term "]"
 | "type" "of" term
@@ -1219,13 +1429,14 @@ simple_tactic: [
 | "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
+| ltac2_match_key ltac2_expr "with" ltac2_match_list "end"
+| ltac2_match_key OPT "reverse" "goal" "with" goal_match_list "end"
 | "simplify_eq" OPT destruction_arg
 | "esimplify_eq" OPT destruction_arg
 | "discriminate" OPT destruction_arg
@@ -1329,10 +1540,10 @@ simple_tactic: [
 | "setoid_reflexivity"
 | "setoid_transitivity" one_term
 | "setoid_etransitivity"
-| "decide" "equality"
-| "compare" one_term one_term
 | "intros" LIST0 intropattern
 | "eintros" LIST0 intropattern
+| "decide" "equality"
+| "compare" one_term one_term
 | "apply" LIST1 constr_with_bindings_arg SEP "," OPT in_hyp_as
 | "eapply" LIST1 constr_with_bindings_arg SEP "," OPT in_hyp_as
 | "simple" "apply" LIST1 constr_with_bindings_arg SEP "," OPT in_hyp_as
@@ -1453,6 +1664,7 @@ simple_tactic: [
 | "psatz" term OPT int_or_var
 | "ring" OPT ( "[" LIST1 term "]" )
 | "ring_simplify" OPT ( "[" LIST1 term "]" ) LIST1 term OPT ( "in" ident )
+| "match" ltac2_expr5 "with" OPT ltac2_branches "end"
 | qualid LIST1 tactic_arg
 ]
 
@@ -1465,26 +1677,6 @@ hloc: [
 | "in" "(" "value" "of" ident ")"
 ]
 
-in_clause: [
-| LIST0 hypident_occ SEP "," OPT ( "|-" OPT concl_occ )
-| "*" "|-" OPT concl_occ
-| "*" OPT ( "at" occs_nums )
-]
-
-concl_occ: [
-| "*" OPT ( "at" occs_nums )
-]
-
-hypident_occ: [
-| hypident OPT ( "at" occs_nums )
-]
-
-hypident: [
-| ident
-| "(" "type" "of" ident ")"
-| "(" "value" "of" ident ")"
-]
-
 as_ipat: [
 | "as" simple_intropattern
 ]
@@ -1507,12 +1699,7 @@ as_name: [
 ]
 
 rewriter: [
-| "!" constr_with_bindings_arg
-| "?" constr_with_bindings_arg
-| num "!" constr_with_bindings_arg
-| num [ "?" | "?" ] constr_with_bindings_arg
-| num constr_with_bindings_arg
-| constr_with_bindings_arg
+| OPT num OPT [ "?" | "!" ] constr_with_bindings_arg
 ]
 
 oriented_rewriter: [
@@ -1554,9 +1741,9 @@ naming_intropattern: [
 ]
 
 intropattern: [
-| simple_intropattern
 | "*"
 | "**"
+| simple_intropattern
 ]
 
 simple_intropattern: [
@@ -1597,9 +1784,367 @@ bindings_with_parameters: [
 | "(" ident LIST0 simple_binder ":=" term ")"
 ]
 
-clause_dft_concl: [
-| "in" in_clause
-| OPT ( "at" occs_nums )
+q_clause: [
+| ltac2_clause      (* Ltac2 plugin *)
+]
+
+ltac2_clause: [
+| "in" ltac2_in_clause      (* Ltac2 plugin *)
+| "at" ltac2_occs_nums      (* Ltac2 plugin *)
+]
+
+ltac2_in_clause: [
+| "*" OPT ltac2_occs      (* Ltac2 plugin *)
+| "*" "|-" OPT ltac2_concl_occ      (* Ltac2 plugin *)
+| LIST0 ltac2_hypident_occ SEP "," OPT ( "|-" OPT ltac2_concl_occ )      (* Ltac2 plugin *)
+]
+
+q_occurrences: [
+| OPT ltac2_occs      (* Ltac2 plugin *)
+]
+
+ltac2_occs: [
+| "at" ltac2_occs_nums      (* Ltac2 plugin *)
+]
+
+ltac2_occs_nums: [
+| OPT "-" LIST1 [ num      (* Ltac2 plugin *) | "$" ident ]      (* Ltac2 plugin *)
+]
+
+ltac2_concl_occ: [
+| "*" OPT ltac2_occs      (* Ltac2 plugin *)
+]
+
+ltac2_hypident_occ: [
+| ltac2_hypident OPT ltac2_occs      (* Ltac2 plugin *)
+]
+
+ltac2_hypident: [
+| ident_or_anti      (* Ltac2 plugin *)
+| "(" "type" "of" ident_or_anti ")"      (* Ltac2 plugin *)
+| "(" "value" "of" ident_or_anti ")"      (* Ltac2 plugin *)
+]
+
+q_induction_clause: [
+| ltac2_induction_clause      (* Ltac2 plugin *)
+]
+
+ltac2_induction_clause: [
+| ltac2_destruction_arg OPT ltac2_as_or_and_ipat OPT ltac2_eqn_ipat OPT ltac2_clause      (* Ltac2 plugin *)
+]
+
+ltac2_as_or_and_ipat: [
+| "as" ltac2_or_and_intropattern      (* Ltac2 plugin *)
+]
+
+ltac2_eqn_ipat: [
+| "eqn" ":" ltac2_naming_intropattern      (* Ltac2 plugin *)
+]
+
+q_conversion: [
+| ltac2_conversion      (* Ltac2 plugin *)
+]
+
+ltac2_conversion: [
+| term      (* Ltac2 plugin *)
+| term "with" term      (* Ltac2 plugin *)
+]
+
+q_rewriting: [
+| ltac2_oriented_rewriter      (* Ltac2 plugin *)
+]
+
+ltac2_oriented_rewriter: [
+| [ "->" | "<-" ] ltac2_rewriter      (* Ltac2 plugin *)
+]
+
+ltac2_rewriter: [
+| OPT num OPT [ "?" | "!" ] ltac2_constr_with_bindings
+]
+
+q_dispatch: [
+| ltac2_for_each_goal      (* Ltac2 plugin *)
+]
+
+ltac2_for_each_goal: [
+| ltac2_goal_tactics      (* Ltac2 plugin *)
+| OPT ( ltac2_goal_tactics "|" ) OPT ltac2_expr ".." OPT ( "|" ltac2_goal_tactics )      (* Ltac2 plugin *)
+]
+
+ltac2_goal_tactics: [
+| LIST0 ( OPT ltac2_expr ) SEP "|"      (* Ltac2 plugin *)
+]
+
+q_strategy_flag: [
+| ltac2_strategy_flag      (* Ltac2 plugin *)
+]
+
+ltac2_strategy_flag: [
+| LIST1 ltac2_red_flag      (* Ltac2 plugin *)
+| OPT ltac2_delta_flag      (* Ltac2 plugin *)
+]
+
+ltac2_red_flag: [
+| "beta"      (* Ltac2 plugin *)
+| "iota"      (* Ltac2 plugin *)
+| "match"      (* Ltac2 plugin *)
+| "fix"      (* Ltac2 plugin *)
+| "cofix"      (* Ltac2 plugin *)
+| "zeta"      (* Ltac2 plugin *)
+| "delta" OPT ltac2_delta_flag      (* Ltac2 plugin *)
+]
+
+ltac2_delta_flag: [
+| OPT "-" "[" LIST1 refglobal "]"
+]
+
+q_reference: [
+| refglobal      (* Ltac2 plugin *)
+]
+
+refglobal: [
+| "&" ident      (* Ltac2 plugin *)
+| qualid      (* Ltac2 plugin *)
+| "$" ident      (* Ltac2 plugin *)
+]
+
+q_hintdb: [
+| hintdb      (* Ltac2 plugin *)
+]
+
+hintdb: [
+| "*"      (* Ltac2 plugin *)
+| LIST1 ident_or_anti      (* Ltac2 plugin *)
+]
+
+q_constr_matching: [
+| ltac2_match_list      (* Ltac2 plugin *)
+]
+
+ltac2_match_key: [
+| "lazy_match!"
+| "match!"
+| "multi_match!"
+]
+
+ltac2_match_list: [
+| OPT "|" LIST1 ltac2_match_rule SEP "|"
+]
+
+ltac2_match_rule: [
+| ltac2_match_pattern "=>" ltac2_expr      (* Ltac2 plugin *)
+]
+
+ltac2_match_pattern: [
+| cpattern      (* Ltac2 plugin *)
+| "context" OPT ident "[" cpattern "]"      (* Ltac2 plugin *)
+]
+
+q_goal_matching: [
+| goal_match_list      (* Ltac2 plugin *)
+]
+
+goal_match_list: [
+| OPT "|" LIST1 gmatch_rule SEP "|"
+]
+
+gmatch_rule: [
+| gmatch_pattern "=>" ltac2_expr      (* Ltac2 plugin *)
+]
+
+gmatch_pattern: [
+| "[" LIST0 gmatch_hyp_pattern SEP "," "|-" ltac2_match_pattern "]"      (* Ltac2 plugin *)
+]
+
+gmatch_hyp_pattern: [
+| name ":" ltac2_match_pattern      (* Ltac2 plugin *)
+]
+
+q_move_location: [
+| move_location      (* Ltac2 plugin *)
+]
+
+move_location: [
+| "at" "top"      (* Ltac2 plugin *)
+| "at" "bottom"      (* Ltac2 plugin *)
+| "after" ident_or_anti      (* Ltac2 plugin *)
+| "before" ident_or_anti      (* Ltac2 plugin *)
+]
+
+q_pose: [
+| pose      (* Ltac2 plugin *)
+]
+
+pose: [
+| "(" ident_or_anti ":=" term ")"      (* Ltac2 plugin *)
+| term OPT ltac2_as_name      (* Ltac2 plugin *)
+]
+
+ltac2_as_name: [
+| "as" ident_or_anti      (* Ltac2 plugin *)
+]
+
+q_assert: [
+| assertion      (* Ltac2 plugin *)
+]
+
+assertion: [
+| "(" ident_or_anti ":=" term ")"      (* Ltac2 plugin *)
+| "(" ident_or_anti ":" term ")" OPT ltac2_by_tactic      (* Ltac2 plugin *)
+| term OPT ltac2_as_ipat OPT ltac2_by_tactic      (* Ltac2 plugin *)
+]
+
+ltac2_as_ipat: [
+| "as" ltac2_simple_intropattern      (* Ltac2 plugin *)
+]
+
+ltac2_by_tactic: [
+| "by" ltac2_expr      (* Ltac2 plugin *)
+]
+
+ltac2_entry: [
+]
+
+tac2def_body: [
+| [ "_" | ident ] LIST0 tac2pat0 ":=" ltac2_expr      (* Ltac2 plugin *)
+]
+
+tac2typ_def: [
+| OPT tac2typ_prm qualid OPT ( [ ":=" | "::=" ] tac2typ_knd )      (* Ltac2 plugin *)
+]
+
+tac2typ_prm: [
+| ltac2_typevar      (* Ltac2 plugin *)
+| "(" LIST1 ltac2_typevar SEP "," ")"      (* Ltac2 plugin *)
+]
+
+tac2typ_knd: [
+| ltac2_type      (* Ltac2 plugin *)
+| "[" OPT ( OPT "|" LIST1 tac2alg_constructor SEP "|" ) "]"      (* Ltac2 plugin *)
+| "[" ".." "]"      (* Ltac2 plugin *)
+| "{" OPT ( LIST1 tac2rec_field SEP ";" OPT ";" ) "}"      (* Ltac2 plugin *)
+]
+
+tac2alg_constructor: [
+| ident      (* Ltac2 plugin *)
+| ident "(" LIST0 ltac2_type SEP "," ")"      (* Ltac2 plugin *)
+]
+
+tac2rec_field: [
+| OPT "mutable" ident ":" ltac2_type      (* Ltac2 plugin *)
+]
+
+ltac2_scope: [
+| string      (* Ltac2 plugin *)
+| int      (* Ltac2 plugin *)
+| name      (* Ltac2 plugin *)
+| name "(" LIST1 ltac2_scope SEP "," ")"      (* Ltac2 plugin *)
+]
+
+ltac2_expr: [
+| ltac2_expr5 ";" ltac2_expr      (* Ltac2 plugin *)
+| ltac2_expr5      (* Ltac2 plugin *)
+]
+
+ltac2_expr5: [
+| "fun" LIST1 tac2pat0 "=>" ltac2_expr      (* Ltac2 plugin *)
+| "let" OPT "rec" ltac2_let_clause LIST0 ( "with" ltac2_let_clause ) "in" ltac2_expr      (* Ltac2 plugin *)
+| ltac2_expr3      (* Ltac2 plugin *)
+]
+
+ltac2_let_clause: [
+| LIST1 tac2pat0 ":=" ltac2_expr      (* Ltac2 plugin *)
+]
+
+ltac2_expr3: [
+| LIST1 ltac2_expr2 SEP ","      (* Ltac2 plugin *)
+]
+
+ltac2_expr2: [
+| ltac2_expr1 "::" ltac2_expr2      (* Ltac2 plugin *)
+| ltac2_expr1      (* Ltac2 plugin *)
+]
+
+ltac2_expr1: [
+| ltac2_expr0 LIST1 ltac2_expr0      (* Ltac2 plugin *)
+| ltac2_expr0 ".(" qualid ")"      (* Ltac2 plugin *)
+| ltac2_expr0 ".(" qualid ")" ":=" ltac2_expr5      (* Ltac2 plugin *)
+| ltac2_expr0      (* Ltac2 plugin *)
+]
+
+tac2rec_fieldexpr: [
+| qualid ":=" ltac2_expr1      (* Ltac2 plugin *)
+]
+
+ltac2_expr0: [
+| "(" ltac2_expr ")"      (* Ltac2 plugin *)
+| "(" ltac2_expr ":" ltac2_type ")"      (* Ltac2 plugin *)
+| "()"      (* Ltac2 plugin *)
+| "[" LIST0 ltac2_expr5 SEP ";" "]"      (* Ltac2 plugin *)
+| "{" OPT ( LIST1 tac2rec_fieldexpr OPT ";" ) "}"      (* Ltac2 plugin *)
+| ltac2_tactic_atom      (* Ltac2 plugin *)
+]
+
+ltac2_tactic_atom: [
+| int      (* Ltac2 plugin *)
+| string      (* Ltac2 plugin *)
+| qualid      (* Ltac2 plugin *)
+| "@" ident      (* Ltac2 plugin *)
+| "&" lident      (* Ltac2 plugin *)
+| "'" term      (* Ltac2 plugin *)
+| ltac2_quotations
+]
+
+ltac2_quotations: [
+| "ident" ":" "(" lident ")"
+| "constr" ":" "(" term ")"
+| "open_constr" ":" "(" term ")"
+| "pattern" ":" "(" cpattern ")"
+| "reference" ":" "(" [ "&" ident | qualid ] ")"
+| "ltac1" ":" "(" ltac1_expr_in_env ")"
+| "ltac1val" ":" "(" ltac1_expr_in_env ")"
+]
+
+ltac1_expr_in_env: [
+| ltac_expr      (* Ltac2 plugin *)
+| LIST0 ident "|-" ltac_expr      (* Ltac2 plugin *)
+]
+
+ltac2_branches: [
+| OPT "|" LIST1 ( tac2pat1 "=>" ltac2_expr ) SEP "|"
+]
+
+tac2pat1: [
+| qualid LIST1 tac2pat0      (* Ltac2 plugin *)
+| qualid      (* Ltac2 plugin *)
+| "[" "]"      (* Ltac2 plugin *)
+| tac2pat0 "::" tac2pat0      (* Ltac2 plugin *)
+| tac2pat0      (* Ltac2 plugin *)
+]
+
+tac2pat0: [
+| "_"      (* Ltac2 plugin *)
+| "()"      (* Ltac2 plugin *)
+| qualid      (* Ltac2 plugin *)
+| "(" OPT atomic_tac2pat ")"      (* Ltac2 plugin *)
+]
+
+atomic_tac2pat: [
+| tac2pat1 ":" ltac2_type      (* Ltac2 plugin *)
+| tac2pat1 "," LIST0 tac2pat1 SEP ","      (* Ltac2 plugin *)
+| tac2pat1      (* Ltac2 plugin *)
+]
+
+tac2mode: [
+| ltac2_expr [ "." | "..." ]      (* Ltac2 plugin *)
+| "Eval" red_expr "in" term
+| "Compute" term
+| "Check" term
+| "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 )
+| "Search" LIST1 ( search_query ) OPT ( [ "inside" | "outside" ] LIST1 qualid )
 ]
 
 clause_dft_all: [
@@ -1636,17 +2181,6 @@ constr_with_bindings: [
 | one_term OPT ( "with" bindings )
 ]
 
-destruction_arg: [
-| num
-| constr_with_bindings
-| constr_with_bindings_arg
-]
-
-constr_with_bindings_arg: [
-| ">" constr_with_bindings
-| constr_with_bindings
-]
-
 conversion: [
 | one_term
 | one_term "with" one_term