Convert misc chapters to prodn

4 files changed, 235 insertions, 186 deletions

diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg
index 1e9be8dded..f9aba5b1e1 100644
--- a/doc/tools/docgram/common.edit_mlg
+++ b/doc/tools/docgram/common.edit_mlg
@@ -103,7 +103,7 @@ RENAME: [
 | Constr.lconstr lconstr
 | Constr.lconstr_pattern cpattern
 | G_vernac.query_command query_command
-| G_vernac.section_subset_expr section_subset_expr
+| G_vernac.section_subset_expr section_var_expr
 | Prim.ident ident
 | Prim.reference reference
 | Pvernac.Vernac_.main_entry vernac_control
@@ -182,10 +182,6 @@ DELETE: [
 
 (* additional nts to be spliced *)
 
-hyp: [
-| var
-]
-
 tactic_then_last: [
 | REPLACE "|" LIST0 ( OPT tactic_expr5 ) SEP "|"
 | WITH LIST0 ( "|" ( OPT tactic_expr5 ) )
@@ -303,9 +299,9 @@ atomic_constr: [
 | MOVETO primitive_notations NUMBER
 | MOVETO primitive_notations string
 | MOVETO term_evar "_"
-| REPLACE "?" "[" ident "]"
-| WITH "?[" ident "]"
-| MOVETO term_evar "?[" ident "]"
+| REPLACE "?" "[" identref "]"
+| WITH "?[" identref "]"
+| MOVETO term_evar "?[" identref "]"
 | REPLACE "?" "[" pattern_ident "]"
 | WITH "?[" pattern_ident "]"
 | MOVETO term_evar "?[" pattern_ident "]"
@@ -373,7 +369,7 @@ operconstr10: [
 | MOVETO term_application operconstr9 LIST1 appl_arg
 | MOVETO term_application "@" qualid_annotated LIST1 operconstr9
 (* fixme: add in as a prodn somewhere *)
-| MOVETO dangling_pattern_extension_rule "@" pattern_identref LIST1 identref
+| MOVETO dangling_pattern_extension_rule "@" pattern_ident LIST1 identref
 | DELETE dangling_pattern_extension_rule
 ]
 
@@ -545,7 +541,13 @@ evar_instance: [
 
 (* No constructor syntax, OPT [ "|" binders ] is not supported for Record *)
 record_definition: [
-| opt_coercion ident_decl binders OPT [ ":" type ] OPT [ identref ] "{" record_fields "}"  decl_notations
+| opt_coercion ident_decl binders OPT [ ":" sort ] OPT ( ":=" OPT [ identref ] "{" record_fields "}" )
+]
+
+(* No mutual recursion, no inductive classes, type must be a sort *)
+(* constructor is optional but "Class record_definition" covers that case *)
+singleton_class_definition: [
+| opt_coercion ident_decl binders OPT [ ":" sort ] ":=" constructor
 ]
 
 (* No record syntax, opt_coercion not supported for Variant, := ... required *)
@@ -562,7 +564,8 @@ gallina: [
 |   "CoInductive" inductive_definition LIST0 ( "with" inductive_definition )
 |   "Variant" variant_definition LIST0 ( "with" variant_definition )
 |   [ "Record" | "Structure" ] record_definition LIST0 ( "with" record_definition )
-|   "Class" inductive_definition LIST0 ( "with" inductive_definition )
+|   "Class" record_definition
+|   "Class" singleton_class_definition
 | REPLACE "Fixpoint" LIST1 rec_definition SEP "with"
 | WITH "Fixpoint" rec_definition LIST0 ( "with" rec_definition )
 | REPLACE "Let" "Fixpoint" LIST1 rec_definition SEP "with"
@@ -713,6 +716,10 @@ gallina_ext: [
 | REPLACE "Coercion" by_notation ":" class_rawexpr ">->" class_rawexpr
 | WITH "Coercion" smart_global ":" class_rawexpr ">->" class_rawexpr
 
+(* semantically restricted per https://github.com/coq/coq/pull/12936#discussion_r492705820 *)
+| REPLACE "Coercion" global OPT univ_decl def_body
+| WITH "Coercion" ident OPT univ_decl def_body
+
 | REPLACE "Include" "Type" module_type_inl LIST0 ext_module_type
 | WITH "Include" "Type" LIST1 module_type_inl SEP "<+"
 
@@ -725,7 +732,7 @@ gallina_ext: [
 | REPLACE "Export" "Unset" option_table
 | WITH "Unset" option_table
 | REPLACE "Instance" instance_name ":" operconstr200 hint_info [ ":=" "{" record_declaration "}" | ":=" lconstr | ]
-| WITH "Instance" instance_name ":" operconstr200 hint_info OPT [ ":=" "{" record_declaration "}" | ":=" lconstr ]
+| WITH "Instance" instance_name ":" type hint_info OPT [ ":=" "{" record_declaration "}" | ":=" lconstr ]
 
 | REPLACE "From" global "Require" export_token LIST1 global
 | WITH "From" dirpath "Require" export_token LIST1 global
@@ -1083,8 +1090,8 @@ simple_tactic: [
 | EDIT "psatz_R" ADD_OPT int_or_var tactic
 | EDIT "psatz_Q" ADD_OPT int_or_var tactic
 | EDIT "psatz_Z" ADD_OPT int_or_var tactic
-| REPLACE "subst" LIST1 var
-| WITH "subst" OPT ( LIST1 var )
+| REPLACE "subst" LIST1 hyp
+| WITH "subst" OPT ( LIST1 hyp )
 | DELETE "subst"
 | DELETE "congruence"
 | DELETE "congruence" natural
@@ -1099,6 +1106,14 @@ simple_tactic: [
 | DELETE "transparent_abstract" tactic3
 | REPLACE "transparent_abstract" tactic3 "using" ident
 | WITH "transparent_abstract" tactic_expr3 OPT ( "using" ident )
+| REPLACE "typeclasses" "eauto" "bfs" OPT int_or_var "with" LIST1 preident
+| WITH "typeclasses" "eauto" OPT "bfs" OPT int_or_var OPT ( "with" LIST1 preident )
+| DELETE "typeclasses" "eauto" OPT int_or_var "with" LIST1 preident
+| DELETE "typeclasses" "eauto" "bfs" OPT int_or_var
+| DELETE "typeclasses" "eauto" OPT int_or_var
+(* in Tactic Notation: *)
+| "setoid_replace" constr "with" constr OPT ( "using" "relation" constr ) OPT ( "in" hyp )
+       OPT ( "at" LIST1 int_or_var ) OPT ( "by" tactic_expr3 )
 ]
 
 (* todo: don't use DELETENT for this *)
@@ -1130,6 +1145,23 @@ printable: [
 | INSERTALL "Print"
 ]
 
+add_zify: [
+| [ "InjTyp" | "BinOp" | "UnOp" | "CstOp" | "BinRel" | "UnOpSpec" | "BinOpSpec" ]  TAG Micromega
+| [ "PropOp" | "PropBinOp" | "PropUOp" | "Saturate" ]TAG Micromega
+]
+
+show_zify: [
+| [ "InjTyp" | "BinOp" | "UnOp" | "CstOp" | "BinRel" | "UnOpSpec" | "BinOpSpec" | "Spec" ]  TAG Micromega
+]
+
+scheme_kind: [
+| DELETE "Induction" "for" smart_global "Sort" sort_family
+| DELETE "Minimality" "for" smart_global "Sort" sort_family
+| DELETE "Elimination" "for" smart_global "Sort" sort_family
+| DELETE "Case" "for" smart_global "Sort" sort_family
+| [ "Induction" | "Minimality" | "Elimination" | "Case" ] "for" smart_global "Sort" sort_family
+]
+
 command: [
 | REPLACE "Print" printable
 | WITH printable
@@ -1202,7 +1234,7 @@ command: [
 | WITH "Next" "Obligation" OPT ( "of" ident ) withtac
 | DELETE "Next" "Obligation" withtac
 | REPLACE "Obligation" natural "of" ident ":" lglob withtac
-| WITH "Obligation" natural OPT ( "of" ident ) OPT ( ":" lglob withtac )
+| WITH "Obligation" natural OPT ( "of" ident ) OPT ( ":" type withtac )
 | DELETE "Obligation" natural "of" ident withtac
 | DELETE "Obligation" natural ":" lglob withtac
 | DELETE "Obligation" natural withtac
@@ -1232,13 +1264,14 @@ command: [
 | REPLACE "Solve" "All" "Obligations" "with" tactic
 | WITH "Solve" "All" "Obligations" OPT ( "with" tactic )
 | DELETE "Solve" "All" "Obligations"
+| DELETE "Solve" "Obligations" "of" ident "with" tactic
+| DELETE "Solve" "Obligations" "of" ident
+| DELETE "Solve" "Obligations" "with" tactic
+| DELETE "Solve" "Obligations"
+| "Solve" "Obligations" OPT ( "of" ident ) OPT ( "with" tactic )
 | REPLACE "Solve" "Obligation" natural "of" ident "with" tactic
 | WITH "Solve" "Obligation" natural OPT ( "of" ident ) "with" tactic
-| DELETE "Solve" "Obligations"
 | DELETE "Solve" "Obligation" natural "with" tactic
-| REPLACE "Solve" "Obligations" "of" ident "with" tactic
-| WITH "Solve" "Obligations" OPT ( OPT ( "of" ident ) "with" tactic )
-| DELETE "Solve" "Obligations" "with" tactic
 | DELETE "Undo"
 | DELETE "Undo" natural
 | REPLACE "Undo" "To" natural
@@ -1263,10 +1296,36 @@ command: [
 (* odd that these are in command while other notation-related ones are in syntax *)
 | REPLACE "Numeral" "Notation" reference reference reference ":" ident numnotoption
 | WITH "Numeral" "Notation" reference reference reference ":" scope_name numnotoption
+| REPLACE "Number" "Notation" reference reference reference ":" ident numnotoption
+| WITH "Number" "Notation" reference reference reference ":" scope_name numnotoption
 | REPLACE "String" "Notation" reference reference reference ":" ident
 | WITH "String" "Notation" reference reference reference ":" scope_name
 
 | DELETE "Ltac2" ltac2_entry      (* was split up *)
+| DELETE "Add" "Zify" "InjTyp" constr      (* micromega plugin *)
+| DELETE "Add" "Zify" "BinOp" constr      (* micromega plugin *)
+| DELETE "Add" "Zify" "UnOp" constr      (* micromega plugin *)
+| DELETE "Add" "Zify" "CstOp" constr      (* micromega plugin *)
+| DELETE "Add" "Zify" "BinRel" constr      (* micromega plugin *)
+| DELETE "Add" "Zify" "PropOp" constr      (* micromega plugin *)
+| DELETE "Add" "Zify" "PropBinOp" constr      (* micromega plugin *)
+| DELETE "Add" "Zify" "PropUOp" constr      (* micromega plugin *)
+| DELETE "Add" "Zify" "BinOpSpec" constr      (* micromega plugin *)
+| DELETE "Add" "Zify" "UnOpSpec" constr      (* micromega plugin *)
+| DELETE "Add" "Zify" "Saturate" constr      (* micromega plugin *)
+| "Add" "Zify" add_zify constr  TAG Micromega
+
+| DELETE "Show" "Zify" "InjTyp"      (* micromega plugin *)
+| DELETE "Show" "Zify" "BinOp"      (* micromega plugin *)
+| DELETE "Show" "Zify" "UnOp"      (* micromega plugin *)
+| DELETE "Show" "Zify" "CstOp"      (* micromega plugin *)
+| DELETE "Show" "Zify" "BinRel"      (* micromega plugin *)
+| DELETE "Show" "Zify" "UnOpSpec"      (* micromega plugin *)
+| DELETE "Show" "Zify" "BinOpSpec"      (* micromega plugin *)
+(* keep this one | "Show" "Zify" "Spec"      (* micromega plugin *)*)
+| "Show" "Zify" show_zify  TAG Micromega
+| REPLACE "Goal" lconstr
+| WITH "Goal" type
 ]
 
 option_setting: [
@@ -1394,7 +1453,7 @@ type_cstr: [
 
 inductive_definition: [
 | REPLACE opt_coercion ident_decl binders OPT [ "|" binders ] OPT [ ":" lconstr ] opt_constructors_or_fields decl_notations
-| WITH opt_coercion ident_decl binders OPT [ "|" binders ] OPT [ ":" type ] opt_constructors_or_fields decl_notations
+| WITH    opt_coercion ident_decl binders OPT [ "|" binders ] OPT [ ":" type ]    opt_constructors_or_fields decl_notations
 ]
 
 (* note that constructor -> identref constructor_type *)
@@ -1617,7 +1676,7 @@ eauto_search_strategy: [
 constr_body: [
 | DELETE ":=" lconstr
 | REPLACE ":" lconstr ":=" lconstr
-| WITH OPT ( ":" lconstr ) ":=" lconstr
+| WITH OPT ( ":" type ) ":=" lconstr
 ]
 
 opt_hintbases: [
@@ -1769,8 +1828,15 @@ tactic_mode: [
 | ltac_info tactic
 | MOVETO command ltac_info tactic
 | DELETE command
+| REPLACE OPT toplevel_selector "{"
+(* semantically restricted *)
+| WITH OPT ( [ natural | "[" ident "]" ] ":" ) "{"
+| MOVETO simple_tactic OPT ( [ natural | "[" ident "]" ] ":" ) "{"
+| DELETE simple_tactic
 ]
 
+tactic_mode: [ | DELETENT ]
+
 sexpr: [
 | REPLACE syn_node      (* Ltac2 plugin *)
 | WITH name TAG Ltac2
@@ -1866,14 +1932,14 @@ ltac_defined_tactics: [
 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 )
+| "field" OPT ( "[" LIST1 constr "]" )
+| "field_simplify" OPT ( "[" LIST1 constr "]" ) LIST1 constr OPT ( "in" ident )
+| "field_simplify_eq" OPT ( "[" LIST1 constr "]" ) 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? *)
+| "nsatz" OPT ( "with" "radicalmax" ":=" constr "strategy" ":=" constr "parameters" ":=" constr "variables" ":=" constr )
+| "psatz" constr OPT int_or_var
+| "ring" OPT ( "[" LIST1 constr "]" )
+| "ring_simplify" OPT ( "[" LIST1 constr "]" ) LIST1 constr OPT ( "in" ident )  (* todo: ident was "hyp", worth keeping? *)
 ]
 
 (* defined in OCaml outside of mlgs *)
@@ -2194,6 +2260,36 @@ ltac2_induction_clause: [
 | WITH ltac2_destruction_arg OPT ltac2_as_or_and_ipat OPT ltac2_eqn_ipat OPT ltac2_clause  TAG Ltac2
 ]
 
+starredidentref: [
+| EDIT identref ADD_OPT "*"
+| EDIT "Type" ADD_OPT "*"
+| "All"
+]
+
+ssexpr0: [
+| DELETE "(" LIST0 starredidentref ")"
+| DELETE "(" LIST0 starredidentref ")" "*"
+| DELETE "(" ssexpr35 ")"
+| DELETE "(" ssexpr35 ")" "*"
+| "(" section_subset_expr ")" OPT "*"
+]
+
+ssexpr35: [
+| EDIT ADD_OPT "-" ssexpr50
+]
+
+simple_binding: [
+| REPLACE "(" ident ":=" lconstr ")"
+| WITH "(" [ ident | natural ] ":=" lconstr ")"
+| DELETE "(" natural ":=" lconstr ")"
+]
+
+
+subprf: [
+| MOVEALLBUT simple_tactic
+| "{" (* should be removed.  See https://github.com/coq/coq/issues/12004 *)
+]
+
 SPLICE: [
 | clause
 | noedit_mode
@@ -2204,7 +2300,6 @@ SPLICE: [
 | NUMBER
 | STRING
 | hyp
-| var
 | identref
 | pattern_ident
 | constr_eval  (* splices as multiple prods *)
@@ -2286,7 +2381,7 @@ SPLICE: [
 | decorated_vernac
 | ext_module_expr
 | ext_module_type
-| pattern_identref
+| pattern_ident
 | test
 | binder_constr
 | atomic_constr
@@ -2381,6 +2476,13 @@ SPLICE: [
 | G_LTAC2_input_fun
 | ltac2_simple_intropattern_closed
 | ltac2_with_bindings
+| int_or_id
+| fun_ind_using
+| with_names
+| eauto_search_strategy_name
+| constr_with_bindings
+| simple_binding
+| ssexpr35 (* strange in mlg, ssexpr50 is after this *)
 ] (* end SPLICE *)
 
 RENAME: [
@@ -2405,7 +2507,10 @@ RENAME: [
 | pattern100 pattern
 | match_constr term_match
 (*| impl_ident_tail impl_ident*)
-| ssexpr35 ssexpr (* strange in mlg, ssexpr50 is after this *)
+| ssexpr50 section_var_expr50
+| ssexpr0 section_var_expr0
+| section_subset_expr section_var_expr
+| fun_scheme_arg func_scheme_def
 
 | tactic_then_gen for_each_goal
 | ltac2_tactic_then_gen ltac2_for_each_goal
@@ -2415,7 +2520,7 @@ RENAME: [
 | BULLET bullet
 | fix_decl fix_body
 | cofix_decl cofix_body
-(* todo: it's confusing that Constr.constr and constr are different things *)
+(* todo: it's confusing that Constr.constr and constr mean different things *)
 | constr one_term
 | appl_arg arg
 | rec_definition fix_definition
@@ -2454,6 +2559,7 @@ RENAME: [
 | tac2expr1 ltac2_expr1
 | tac2expr0 ltac2_expr0
 | gmatch_list goal_match_list
+| starredidentref starred_ident_ref
 ]
 
 simple_tactic: [
diff --git a/doc/tools/docgram/doc_grammar.ml b/doc/tools/docgram/doc_grammar.ml
index 48b2b0b95a..b7f1e18d2b 100644
--- a/doc/tools/docgram/doc_grammar.ml
+++ b/doc/tools/docgram/doc_grammar.ml
@@ -1727,6 +1727,7 @@ let open_temp_bin file =
 
 let match_cmd_regex = Str.regexp "[a-zA-Z0-9_ ]+"
 let match_subscripts = Str.regexp "__[a-zA-Z0-9]+"
+let remove_subscrs str = Str.global_replace match_subscripts "" str
 
 let find_longest_match prods str =
   let get_pfx str = String.trim (if Str.string_match match_cmd_regex str 0 then Str.matched_string str else "") in
@@ -1740,7 +1741,6 @@ let find_longest_match prods str =
     in
     aux 0
   in
-  let remove_subscrs str = Str.global_replace match_subscripts "" str in
 
   let slen = String.length str in
   let str_pfx = get_pfx str in
@@ -1895,25 +1895,15 @@ let process_rst g file args seen tac_prods cmd_prods =
 (*    "doc/sphinx/proof-engine/ssreflect-proof-language.rst"]*)
 (*  in*)
 
-  let cmd_replace_files = [
-    "doc/sphinx/language/core/records.rst";
-    "doc/sphinx/language/core/sections.rst";
-    "doc/sphinx/language/extensions/implicit-arguments.rst";
-    "doc/sphinx/language/extensions/arguments-command.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/ltac2.rst";
-    "doc/sphinx/proof-engine/vernacular-commands.rst";
-    "doc/sphinx/user-extensions/syntax-extensions.rst";
-    "doc/sphinx/proof-engine/vernacular-commands.rst"
+  let cmd_exclude_files = [
+    "doc/sphinx/proof-engine/ssreflect-proof-language.rst";
+    "doc/sphinx/proof-engine/tactics.rst"
   ]
   in
 
   let save_n_get_more direc pfx first_rhs seen_map prods =
     let replace rhs prods =
-      if StringSet.is_empty prods || not (List.mem file cmd_replace_files) then
+      if StringSet.is_empty prods || (List.mem file cmd_exclude_files) then
         rhs (* no change *)
       else
         let mtch, multi, best = find_longest_match prods rhs in
@@ -1942,7 +1932,7 @@ let process_rst g file args seen tac_prods cmd_prods =
 
     fprintf new_rst "%s%s\n" pfx (replace first_rhs prods);
 
-    map := NTMap.add first_rhs (file, !linenum) !map;
+    map := NTMap.add (remove_subscrs first_rhs) (file, !linenum) !map;
     while
       let nextline = getline() in
       ignore (Str.string_match contin_regex nextline 0);
diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar
index 73641976e3..d3148b5e3a 100644
--- a/doc/tools/docgram/fullGrammar
+++ b/doc/tools/docgram/fullGrammar
@@ -90,7 +90,7 @@ operconstr90: [
 operconstr10: [
 | operconstr9 LIST1 appl_arg
 | "@" global univ_instance LIST0 operconstr9
-| "@" pattern_identref LIST1 identref
+| "@" pattern_ident LIST1 identref
 | operconstr9
 ]
 
@@ -155,7 +155,7 @@ binder_constr: [
 ]
 
 appl_arg: [
-| test_lpar_id_coloneq "(" ident ":=" lconstr ")"
+| test_lpar_id_coloneq "(" identref ":=" lconstr ")"
 | operconstr9
 ]
 
@@ -165,13 +165,13 @@ atomic_constr: [
 | NUMBER
 | string
 | "_"
-| "?" "[" ident "]"
+| "?" "[" identref "]"
 | "?" "[" pattern_ident "]"
 | pattern_ident evar_instance
 ]
 
 inst: [
-| ident ":=" lconstr
+| identref ":=" lconstr
 ]
 
 evar_instance: [
@@ -362,16 +362,12 @@ pattern_ident: [
 | LEFTQMARK ident
 ]
 
-pattern_identref: [
-| pattern_ident
-]
-
-var: [
+identref: [
 | ident
 ]
 
-identref: [
-| ident
+hyp: [
+| identref
 ]
 
 field: [
@@ -596,9 +592,9 @@ command: [
 | "Optimize" "Proof"
 | "Optimize" "Heap"
 | "Hint" "Cut" "[" hints_path "]" opthints
-| "Typeclasses" "Transparent" LIST0 reference
-| "Typeclasses" "Opaque" LIST0 reference
-| "Typeclasses" "eauto" ":=" debug eauto_search_strategy OPT integer
+| "Typeclasses" "Transparent" LIST1 reference
+| "Typeclasses" "Opaque" LIST1 reference
+| "Typeclasses" "eauto" ":=" debug eauto_search_strategy OPT natural
 | "Proof" "with" Pltac.tactic OPT [ "using" G_vernac.section_subset_expr ]
 | "Proof" "using" G_vernac.section_subset_expr OPT [ "with" Pltac.tactic ]
 | "Tactic" "Notation" OPT ltac_tactic_level LIST1 ltac_production_item ":=" tactic
@@ -615,6 +611,7 @@ command: [
 | "Solve" "Obligation" natural "of" ident "with" tactic
 | "Solve" "Obligation" natural "with" tactic
 | "Solve" "Obligations" "of" ident "with" tactic
+| "Solve" "Obligations" "of" ident
 | "Solve" "Obligations" "with" tactic
 | "Solve" "Obligations"
 | "Solve" "All" "Obligations" "with" tactic
@@ -1551,7 +1548,7 @@ simple_tactic: [
 | "notypeclasses" "refine" uconstr
 | "simple" "notypeclasses" "refine" uconstr
 | "solve_constraints"
-| "subst" LIST1 var
+| "subst" LIST1 hyp
 | "subst"
 | "simple" "subst"
 | "evar" test_lpar_id_colon "(" ident ":" lconstr ")"
@@ -1619,6 +1616,7 @@ simple_tactic: [
 | "convert_concl_no_check" constr
 | "typeclasses" "eauto" "bfs" OPT int_or_var "with" LIST1 preident
 | "typeclasses" "eauto" OPT int_or_var "with" LIST1 preident
+| "typeclasses" "eauto" "bfs" OPT int_or_var
 | "typeclasses" "eauto" OPT int_or_var
 | "head_of_constr" ident constr
 | "not_evar" constr
@@ -1811,7 +1809,7 @@ EXTRAARGS_natural: [
 
 occurrences: [
 | LIST1 integer
-| var
+| hyp
 ]
 
 glob: [
diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar
index 61befe9f1f..ff1efa5375 100644
--- a/doc/tools/docgram/orderedGrammar
+++ b/doc/tools/docgram/orderedGrammar
@@ -3,10 +3,6 @@ doc_grammar will modify this file to add/remove nonterminals and productions
 to match editedGrammar, which will remove comments.  Not compiled into Coq *)
 DOC_GRAMMAR
 
-tactic_mode: [
-| OPT ( toplevel_selector ":" ) "{"
-]
-
 term: [
 | term_forall_or_fun
 | term_let
@@ -191,6 +187,15 @@ where: [
 | "before" ident
 ]
 
+add_zify: [
+| [ "InjTyp" | "BinOp" | "UnOp" | "CstOp" | "BinRel" | "UnOpSpec" | "BinOpSpec" ]      (* Micromega plugin *)
+| [ "PropOp" | "PropBinOp" | "PropUOp" | "Saturate" ]      (* Micromega plugin *)
+]
+
+show_zify: [
+| [ "InjTyp" | "BinOp" | "UnOp" | "CstOp" | "BinRel" | "UnOpSpec" | "BinOpSpec" | "Spec" ]      (* Micromega plugin *)
+]
+
 REACHABLE: [
 | command
 | simple_tactic
@@ -448,9 +453,7 @@ vernac_aux: [
 ]
 
 subprf: [
-| bullet
 | "{"
-| "}"
 ]
 
 fix_definition: [
@@ -538,8 +541,12 @@ variant_definition: [
 | ident_decl LIST0 binder OPT [ "|" LIST0 binder ] OPT [ ":" type ] ":=" OPT "|" LIST1 constructor SEP "|" OPT decl_notations
 ]
 
+singleton_class_definition: [
+| OPT ">" ident_decl LIST0 binder OPT [ ":" sort ] ":=" constructor
+]
+
 record_definition: [
-| OPT ">" ident_decl LIST0 binder OPT [ ":" type ] OPT ident "{" LIST0 record_field SEP ";" OPT ";" "}" OPT decl_notations
+| OPT ">" ident_decl LIST0 binder OPT [ ":" sort ] OPT ( ":=" OPT ident "{" LIST0 record_field SEP ";" OPT ";" "}" )
 ]
 
 record_field: [
@@ -582,11 +589,8 @@ cofix_definition: [
 ]
 
 scheme_kind: [
-| "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
+| [ "Induction" | "Minimality" | "Elimination" | "Case" ] "for" reference "Sort" sort_family
 ]
 
 sort_family: [
@@ -714,7 +718,7 @@ simple_reserv: [
 ]
 
 command: [
-| "Goal" term
+| "Goal" type
 | "Pwd"
 | "Cd" OPT string
 | "Load" OPT "Verbose" [ string | ident ]
@@ -723,6 +727,8 @@ command: [
 | "Locate" "Term" reference
 | "Locate" "Module" qualid
 | "Info" natural ltac_expr
+| "Add" "Zify" add_zify one_term      (* Micromega plugin *)
+| "Show" "Zify" show_zify      (* Micromega plugin *)
 | "Locate" "Ltac" qualid
 | "Locate" "Library" qualid
 | "Locate" "File" string
@@ -798,7 +804,7 @@ command: [
 | "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" "Implicit" qualid "[" LIST0 [ ident | integer ] "]"      (* extraction plugin *)
 | "Extraction" "Blacklist" LIST1 ident      (* extraction plugin *)
 | "Print" "Extraction" "Blacklist"      (* extraction plugin *)
 | "Reset" "Extraction" "Blacklist"      (* extraction plugin *)
@@ -810,7 +816,7 @@ command: [
 | "Proof" "Mode" string
 | "Proof" term
 | "Abort" OPT [ "All" | ident ]
-| "Existential" natural OPT ( ":" term ) ":=" term
+| "Existential" natural OPT ( ":" type ) ":=" term
 | "Admitted"
 | "Qed"
 | "Save" ident
@@ -835,10 +841,10 @@ command: [
 | "Comments" LIST0 [ one_term | string | natural ]
 | "Declare" "Instance" ident_decl LIST0 binder ":" term OPT hint_info
 | "Declare" "Scope" scope_name
-| "Obligation" natural OPT ( "of" ident ) OPT ( ":" term OPT ( "with" ltac_expr ) )
+| "Obligation" natural OPT ( "of" ident ) OPT ( ":" type OPT ( "with" ltac_expr ) )
 | "Next" "Obligation" OPT ( "of" ident ) OPT ( "with" ltac_expr )
 | "Solve" "Obligation" natural OPT ( "of" ident ) "with" ltac_expr
-| "Solve" "Obligations" OPT ( OPT ( "of" ident ) "with" ltac_expr )
+| "Solve" "Obligations" OPT ( "of" ident ) OPT ( "with" ltac_expr )
 | "Solve" "All" "Obligations" OPT ( "with" ltac_expr )
 | "Admit" "Obligations" OPT ( "of" ident )
 | "Obligation" "Tactic" ":=" ltac_expr
@@ -862,17 +868,6 @@ command: [
 | "Reset" "Ltac" "Profile"
 | "Show" "Ltac" "Profile" OPT [ "CutOff" integer | 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 *)
@@ -884,25 +879,18 @@ command: [
 | "Add" "BinOpSpec" one_term      (* micromega plugin *)
 | "Add" "UnOpSpec" one_term      (* micromega plugin *)
 | "Add" "Saturate" one_term      (* micromega plugin *)
-| "Show" "Zify" "InjTyp"      (* micromega plugin *)
-| "Show" "Zify" "BinOp"      (* micromega plugin *)
-| "Show" "Zify" "UnOp"      (* micromega plugin *)
-| "Show" "Zify" "CstOp"      (* micromega plugin *)
-| "Show" "Zify" "BinRel"      (* micromega plugin *)
-| "Show" "Zify" "UnOpSpec"      (* micromega plugin *)
-| "Show" "Zify" "BinOpSpec"      (* micromega plugin *)
 | "Show" "Zify" "Spec"      (* micromega plugin *)
 | "Add" "Ring" ident ":" one_term OPT ( "(" LIST1 ring_mod SEP "," ")" )      (* ring plugin *)
 | "Print" "Rings"      (* ring plugin *)
 | "Add" "Field" ident ":" one_term OPT ( "(" LIST1 field_mod SEP "," ")" )      (* ring plugin *)
 | "Print" "Fields"      (* ring plugin *)
-| "Number" "Notation" qualid qualid qualid ":" ident OPT numeral_modifier
+| "Number" "Notation" qualid qualid qualid ":" scope_name OPT numeral_modifier
 | "Hint" "Cut" "[" hints_path "]" OPT ( ":" LIST1 ident )
-| "Typeclasses" "Transparent" LIST0 qualid
-| "Typeclasses" "Opaque" LIST0 qualid
-| "Typeclasses" "eauto" ":=" OPT "debug" OPT ( "(" eauto_search_strategy_name ")" ) OPT integer
-| "Proof" "with" ltac_expr OPT [ "using" section_subset_expr ]
-| "Proof" "using" section_subset_expr OPT [ "with" ltac_expr ]
+| "Typeclasses" "Transparent" LIST1 qualid
+| "Typeclasses" "Opaque" LIST1 qualid
+| "Typeclasses" "eauto" ":=" OPT "debug" OPT ( "(" [ "bfs" | "dfs" ] ")" ) OPT natural
+| "Proof" "with" ltac_expr OPT [ "using" section_var_expr ]
+| "Proof" "using" section_var_expr OPT [ "with" ltac_expr ]
 | "Tactic" "Notation" OPT ( "(" "at" "level" natural ")" ) LIST1 ltac_production_item ":=" ltac_expr
 | "Print" "Rewrite" "HintDb" ident
 | "Print" "Ltac" qualid
@@ -911,8 +899,8 @@ command: [
 | "Set" "Firstorder" "Solver" ltac_expr
 | "Print" "Firstorder" "Solver"
 | "Function" fix_definition LIST0 ( "with" fix_definition )
-| "Functional" "Scheme" fun_scheme_arg LIST0 ( "with" fun_scheme_arg )
-| "Functional" "Case" fun_scheme_arg      (* funind plugin *)
+| "Functional" "Scheme" func_scheme_def LIST0 ( "with" func_scheme_def )
+| "Functional" "Case" func_scheme_def      (* funind plugin *)
 | "Generate" "graph" "for" qualid      (* funind plugin *)
 | "Hint" "Rewrite" OPT [ "->" | "<-" ] LIST1 one_term OPT ( "using" ltac_expr ) OPT ( ":" LIST0 ident )
 | "Derive" "Inversion_clear" ident "with" one_term OPT ( "Sort" sort_family )
@@ -944,13 +932,14 @@ command: [
 | "CoInductive" inductive_definition LIST0 ( "with" inductive_definition )
 | "Variant" variant_definition LIST0 ( "with" variant_definition )
 | [ "Record" | "Structure" ] record_definition LIST0 ( "with" record_definition )
-| "Class" inductive_definition LIST0 ( "with" inductive_definition )
+| "Class" record_definition
+| "Class" singleton_class_definition
 | "Module" OPT [ "Import" | "Export" ] ident LIST0 module_binder OPT of_module_type OPT ( ":=" LIST1 module_expr_inl SEP "<+" )
 | "Module" "Type" ident LIST0 module_binder LIST0 ( "<:" module_type_inl ) OPT ( ":=" LIST1 module_type_inl SEP "<+" )
 | "Declare" "Module" OPT [ "Import" | "Export" ] ident LIST0 module_binder ":" module_type_inl
 | "Section" ident
 | "End" ident
-| "Collection" ident ":=" section_subset_expr
+| "Collection" ident ":=" section_var_expr
 | "Require" OPT [ "Import" | "Export" ] LIST1 qualid
 | "From" dirpath "Require" OPT [ "Import" | "Export" ] LIST1 qualid
 | "Import" LIST1 filtered_import
@@ -962,11 +951,11 @@ command: [
 | "Strategy" LIST1 [ strategy_level "[" LIST1 reference "]" ]
 | "Canonical" OPT "Structure" ident_decl def_body
 | "Canonical" OPT "Structure" reference
-| "Coercion" qualid OPT univ_decl def_body
+| "Coercion" ident OPT univ_decl def_body
 | "Identity" "Coercion" ident ":" class ">->" class
 | "Coercion" reference ":" class ">->" class
 | "Context" LIST1 binder
-| "Instance" OPT ( ident_decl LIST0 binder ) ":" term OPT hint_info OPT [ ":=" "{" LIST0 field_def "}" | ":=" term ]
+| "Instance" OPT ( ident_decl LIST0 binder ) ":" type OPT hint_info OPT [ ":=" "{" LIST0 field_def "}" | ":=" term ]
 | "Existing" "Instance" qualid OPT hint_info
 | "Existing" "Instances" LIST1 qualid OPT [ "|" natural ]
 | "Existing" "Class" qualid
@@ -1012,35 +1001,26 @@ command: [
 | "Show" "Goal" natural "at" natural
 ]
 
-section_subset_expr: [
-| LIST0 starredidentref
-| ssexpr
-]
-
-ssexpr: [
-| "-" ssexpr50
-| ssexpr50
+section_var_expr: [
+| LIST0 starred_ident_ref
+| OPT "-" section_var_expr50
 ]
 
-ssexpr50: [
-| ssexpr0 "-" ssexpr0
-| ssexpr0 "+" ssexpr0
-| ssexpr0
+section_var_expr50: [
+| section_var_expr0 "-" section_var_expr0
+| section_var_expr0 "+" section_var_expr0
+| section_var_expr0
 ]
 
-ssexpr0: [
-| starredidentref
-| "(" LIST0 starredidentref ")"
-| "(" LIST0 starredidentref ")" "*"
-| "(" ssexpr ")"
-| "(" ssexpr ")" "*"
+section_var_expr0: [
+| starred_ident_ref
+| "(" section_var_expr ")" OPT "*"
 ]
 
-starredidentref: [
-| ident
-| ident "*"
-| "Type"
-| "Type" "*"
+starred_ident_ref: [
+| ident OPT "*"
+| "Type" OPT "*"
+| "All"
 ]
 
 dirpath: [
@@ -1137,13 +1117,13 @@ lident: [
 
 destruction_arg: [
 | natural
-| constr_with_bindings
+| one_term OPT ( "with" bindings )
 | constr_with_bindings_arg
 ]
 
 constr_with_bindings_arg: [
-| ">" constr_with_bindings
-| constr_with_bindings
+| ">" one_term OPT ( "with" bindings )
+| one_term OPT ( "with" bindings )
 ]
 
 clause_dft_concl: [
@@ -1262,11 +1242,6 @@ qhyp: [
 | lident      (* Ltac2 plugin *)
 ]
 
-int_or_id: [
-| ident
-| integer      (* extraction plugin *)
-]
-
 language: [
 | "OCaml"      (* extraction plugin *)
 | "Haskell"      (* extraction plugin *)
@@ -1274,10 +1249,6 @@ language: [
 | "JSON"      (* extraction plugin *)
 ]
 
-fun_scheme_arg: [
-| ident ":=" "Induction" "for" qualid "Sort" sort_family      (* funind plugin *)
-]
-
 ring_mod: [
 | "decidable" one_term      (* ring plugin *)
 | "abstract"      (* ring plugin *)
@@ -1314,11 +1285,6 @@ hints_path: [
 | hints_path hints_path
 ]
 
-eauto_search_strategy_name: [
-| "bfs"
-| "dfs"
-]
-
 class: [
 | "Funclass"
 | "Sortclass"
@@ -1390,7 +1356,7 @@ simple_tactic: [
 | "eright" OPT ( "with" bindings )
 | "constructor" OPT int_or_var OPT ( "with" bindings )
 | "econstructor" OPT ( int_or_var OPT ( "with" bindings ) )
-| "specialize" constr_with_bindings OPT ( "as" simple_intropattern )
+| "specialize" one_term OPT ( "with" bindings ) OPT ( "as" simple_intropattern )
 | "symmetry" OPT ( "in" in_clause )
 | "split" OPT ( "with" bindings )
 | "esplit" OPT ( "with" bindings )
@@ -1411,6 +1377,10 @@ 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
+| "setoid_replace" one_term "with" one_term OPT ( "using" "relation" one_term ) OPT ( "in" ident ) OPT ( "at" LIST1 int_or_var ) OPT ( "by" ltac_expr3 )
+| OPT ( [ natural | "[" ident "]" ] ":" ) "{"
+| bullet
+| "}"
 | "try" ltac_expr3
 | "do" int_or_var ltac_expr3
 | "timeout" int_or_var ltac_expr3
@@ -1456,7 +1426,7 @@ simple_tactic: [
 | "decompose" "sum" one_term
 | "decompose" "record" one_term
 | "absurd" one_term
-| "contradiction" OPT constr_with_bindings
+| "contradiction" OPT ( one_term OPT ( "with" bindings ) )
 | "autorewrite" OPT "*" "with" LIST1 ident OPT clause_dft_concl OPT ( "using" ltac_expr )
 | "rewrite" "*" OPT [ "->" | "<-" ] one_term OPT ( "in" ident ) OPT ( "at" occurrences OPT ( "by" ltac_expr3 ) )
 | "rewrite" "*" OPT [ "->" | "<-" ] one_term "at" occurrences "in" ident OPT ( "by" ltac_expr3 )
@@ -1529,9 +1499,7 @@ simple_tactic: [
 | "autounfold_one" OPT hintbases OPT ( "in" ident )
 | "unify" one_term one_term OPT ( "with" ident )
 | "convert_concl_no_check" one_term
-| "typeclasses" "eauto" "bfs" OPT int_or_var "with" LIST1 ident
-| "typeclasses" "eauto" OPT int_or_var "with" LIST1 ident
-| "typeclasses" "eauto" OPT int_or_var
+| "typeclasses" "eauto" OPT "bfs" OPT int_or_var OPT ( "with" LIST1 ident )
 | "head_of_constr" ident one_term
 | "not_evar" one_term
 | "is_ground" one_term
@@ -1540,9 +1508,9 @@ simple_tactic: [
 | "progress_evars" ltac_expr
 | "rewrite_strat" rewstrategy OPT ( "in" ident )
 | "rewrite_db" ident OPT ( "in" ident )
-| "substitute" OPT [ "->" | "<-" ] constr_with_bindings
-| "setoid_rewrite" OPT [ "->" | "<-" ] constr_with_bindings OPT ( "at" occurrences ) OPT ( "in" ident )
-| "setoid_rewrite" OPT [ "->" | "<-" ] constr_with_bindings "in" ident "at" occurrences
+| "substitute" OPT [ "->" | "<-" ] one_term OPT ( "with" bindings )
+| "setoid_rewrite" OPT [ "->" | "<-" ] one_term OPT ( "with" bindings ) OPT ( "at" occurrences ) OPT ( "in" ident )
+| "setoid_rewrite" OPT [ "->" | "<-" ] one_term OPT ( "with" bindings ) "in" ident "at" occurrences
 | "setoid_symmetry" OPT ( "in" ident )
 | "setoid_reflexivity"
 | "setoid_transitivity" one_term
@@ -1555,8 +1523,8 @@ simple_tactic: [
 | "eapply" LIST1 constr_with_bindings_arg SEP "," OPT in_hyp_as
 | "simple" "apply" LIST1 constr_with_bindings_arg SEP "," OPT in_hyp_as
 | "simple" "eapply" LIST1 constr_with_bindings_arg SEP "," OPT in_hyp_as
-| "elim" constr_with_bindings_arg OPT ( "using" constr_with_bindings )
-| "eelim" constr_with_bindings_arg OPT ( "using" constr_with_bindings )
+| "elim" constr_with_bindings_arg OPT ( "using" one_term OPT ( "with" bindings ) )
+| "eelim" constr_with_bindings_arg OPT ( "using" one_term OPT ( "with" bindings ) )
 | "case" induction_clause_list
 | "ecase" induction_clause_list
 | "fix" ident natural OPT ( "with" LIST1 fixdecl )
@@ -1619,8 +1587,8 @@ simple_tactic: [
 | "firstorder" OPT ltac_expr firstorder_rhs
 | "gintuition" OPT ltac_expr
 | "functional" "inversion" [ ident | natural ] OPT qualid      (* 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 *)
+| "functional" "induction" term OPT ( "using" one_term OPT ( "with" bindings ) ) OPT ( "as" simple_intropattern )      (* funind plugin *)
+| "soft" "functional" "induction" LIST1 one_term OPT ( "using" one_term OPT ( "with" bindings ) ) OPT ( "as" simple_intropattern )      (* funind plugin *)
 | "psatz_Z" OPT int_or_var ltac_expr
 | "xlia" ltac_expr      (* micromega plugin *)
 | "xnlia" ltac_expr      (* micromega plugin *)
@@ -1663,14 +1631,14 @@ simple_tactic: [
 | "zify"
 | "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 )
+| "field" OPT ( "[" LIST1 one_term "]" )
+| "field_simplify" OPT ( "[" LIST1 one_term "]" ) LIST1 one_term OPT ( "in" ident )
+| "field_simplify_eq" OPT ( "[" LIST1 one_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 )
+| "nsatz" OPT ( "with" "radicalmax" ":=" one_term "strategy" ":=" one_term "parameters" ":=" one_term "variables" ":=" one_term )
+| "psatz" one_term OPT int_or_var
+| "ring" OPT ( "[" LIST1 one_term "]" )
+| "ring_simplify" OPT ( "[" LIST1 one_term "]" ) LIST1 one_term OPT ( "in" ident )
 | "match" ltac2_expr5 "with" OPT ltac2_branches "end"
 | qualid LIST1 tactic_arg
 ]
@@ -1718,7 +1686,7 @@ induction_clause: [
 ]
 
 induction_clause_list: [
-| LIST1 induction_clause SEP "," OPT ( "using" constr_with_bindings ) OPT opt_clause
+| LIST1 induction_clause SEP "," OPT ( "using" one_term OPT ( "with" bindings ) ) OPT opt_clause
 ]
 
 auto_using: [
@@ -1764,13 +1732,8 @@ simple_intropattern_closed: [
 | naming_intropattern
 ]
 
-simple_binding: [
-| "(" ident ":=" term ")"
-| "(" natural ":=" term ")"
-]
-
 bindings: [
-| LIST1 simple_binding
+| LIST1 ( "(" [ ident | natural ] ":=" term ")" )
 | LIST1 one_term
 ]
 
@@ -2184,10 +2147,6 @@ cofixdecl: [
 | "(" ident LIST0 simple_binder ":" term ")"
 ]
 
-constr_with_bindings: [
-| one_term OPT ( "with" bindings )
-]
-
 conversion: [
 | one_term
 | one_term "with" one_term
@@ -2200,12 +2159,8 @@ firstorder_using: [
 | "using" qualid qualid LIST0 qualid
 ]
 
-fun_ind_using: [
-| "using" constr_with_bindings      (* funind plugin *)
-]
-
-with_names: [
-| "as" simple_intropattern      (* funind plugin *)
+func_scheme_def: [
+| ident ":=" "Induction" "for" qualid "Sort" sort_family      (* funind plugin *)
 ]
 
 occurrences: [