Convert misc chapters to prodn

1 files changed, 138 insertions, 32 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: [