Convert 2nd part of rewriting chapter to prodn

3 files changed, 560 insertions, 526 deletions

diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg
index 27144fd1ad..24ecc65e9b 100644
--- a/doc/tools/docgram/common.edit_mlg
+++ b/doc/tools/docgram/common.edit_mlg
@@ -62,8 +62,8 @@ SPLICE: [
 ]
 
 RENAME: [
-| G_LTAC2_delta_flag ltac2_delta_flag
-| G_LTAC2_strategy_flag ltac2_strategy_flag
+| G_LTAC2_delta_flag ltac2_delta_reductions
+| G_LTAC2_strategy_flag ltac2_reductions
 | G_LTAC2_binder ltac2_binder
 | G_LTAC2_branches ltac2_branches
 | G_LTAC2_let_clause ltac2_let_clause
@@ -640,7 +640,7 @@ delta_flag: [
 | OPTINREF
 ]
 
-ltac2_delta_flag: [
+ltac2_delta_reductions: [
 | EDIT ADD_OPT "-" "[" refglobals "]"      (* Ltac2 plugin *)
 ]
 
@@ -924,6 +924,10 @@ where: [
 | "before" ident
 ]
 
+simple_occurrences: [
+(* placeholder (yuck) *)
+]
+
 simple_tactic: [
 | REPLACE "eauto" OPT nat_or_var OPT nat_or_var auto_using hintbases
 | WITH "eauto" OPT nat_or_var auto_using hintbases
@@ -937,6 +941,26 @@ simple_tactic: [
 | DELETE "autorewrite" "*" "with" LIST1 preident clause
 | REPLACE "autorewrite" "*" "with" LIST1 preident clause "using" tactic
 | WITH "autorewrite" OPT "*" "with" LIST1 preident clause OPT ( "using" tactic )
+| REPLACE "autounfold" hintbases clause_dft_concl
+| WITH "autounfold" hintbases OPT simple_occurrences
+| REPLACE "red" clause_dft_concl
+| WITH "red" simple_occurrences
+| REPLACE "simpl" OPT delta_flag OPT ref_or_pattern_occ clause_dft_concl
+| WITH "simpl" OPT delta_flag OPT ref_or_pattern_occ simple_occurrences
+| REPLACE "hnf" clause_dft_concl
+| WITH "hnf" simple_occurrences
+| REPLACE "cbv" strategy_flag clause_dft_concl
+| WITH "cbv" strategy_flag simple_occurrences
+| PRINT
+| REPLACE "compute" OPT delta_flag clause_dft_concl
+| WITH "compute" OPT delta_flag simple_occurrences
+| REPLACE "lazy" strategy_flag clause_dft_concl
+| WITH "lazy" strategy_flag simple_occurrences
+| REPLACE "cbn" strategy_flag clause_dft_concl
+| WITH "cbn" strategy_flag simple_occurrences
+| REPLACE "fold" LIST1 constr clause_dft_concl
+| WITH "fold" LIST1 constr simple_occurrences
+
 | DELETE "cofix" ident
 | REPLACE "cofix" ident "with" LIST1 cofixdecl
 | WITH "cofix" ident OPT ( "with" LIST1 cofixdecl )
@@ -2460,6 +2484,10 @@ clause_dft_concl: [
 | WITH occs
 ]
 
+simple_occurrences: [
+| clause_dft_concl   (* semantically restricted: no "at" clause *)
+]
+
 occs_nums: [
 | EDIT ADD_OPT "-" LIST1 nat_or_var
 ]
@@ -2471,10 +2499,8 @@ variance_identref: [
 conversion: [
 | DELETE constr
 | DELETE constr "with" constr
-| PRINT
 | REPLACE constr "at" occs_nums "with" constr
 | WITH OPT ( constr OPT ( "at" occs_nums ) "with" ) constr
-| PRINT
 ]
 
 SPLICE: [
@@ -2762,6 +2788,10 @@ RENAME: [
 | hypident_occ hyp_occs
 | concl_occ concl_occs
 | constr_with_bindings_arg one_term_with_bindings
+| red_flag reduction
+| strategy_flag reductions
+| delta_flag delta_reductions
+| q_strategy_flag q_reductions
 ]
 
 simple_tactic: [
@@ -2806,7 +2836,7 @@ NOTINRSTS: [
 | q_destruction_arg
 | q_with_bindings
 | q_bindings
-| q_strategy_flag
+| q_reductions
 | q_reference
 | q_clause
 | q_occurrences
diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar
index bc6b803bbb..be1b9d80fb 100644
--- a/doc/tools/docgram/fullGrammar
+++ b/doc/tools/docgram/fullGrammar
@@ -1,492 +1,6 @@
 (* Coq grammar generated from .mlg files.  Do not edit by hand.  Not compiled into Coq *)
 DOC_GRAMMAR
 
-Constr.ident: [
-| Prim.ident
-]
-
-Prim.name: [
-| "_"
-]
-
-global: [
-| Prim.reference
-]
-
-constr_pattern: [
-| constr
-]
-
-cpattern: [
-| lconstr
-]
-
-sort: [
-| "Set"
-| "Prop"
-| "SProp"
-| "Type"
-| "Type" "@{" "_" "}"
-| "Type" "@{" universe "}"
-]
-
-sort_family: [
-| "Set"
-| "Prop"
-| "SProp"
-| "Type"
-]
-
-universe_increment: [
-| "+" natural
-|
-]
-
-universe_name: [
-| global
-| "Set"
-| "Prop"
-]
-
-universe_expr: [
-| universe_name universe_increment
-]
-
-universe: [
-| "max" "(" LIST1 universe_expr SEP "," ")"
-| universe_expr
-]
-
-lconstr: [
-| term200
-]
-
-constr: [
-| term8
-| "@" global univ_annot
-]
-
-term200: [
-| binder_constr
-| term100
-]
-
-term100: [
-| term99 "<:" term200
-| term99 "<<:" term200
-| term99 ":" term200
-| term99 ":>"
-| term99
-]
-
-term99: [
-| term90
-]
-
-term90: [
-| term10
-]
-
-term10: [
-| term9 LIST1 arg
-| "@" global univ_annot LIST0 term9
-| "@" pattern_ident LIST1 identref
-| term9
-]
-
-term9: [
-| ".." term0 ".."
-| term8
-]
-
-term8: [
-| term1
-]
-
-term1: [
-| term0 ".(" global LIST0 arg ")"
-| term0 ".(" "@" global LIST0 ( term9 ) ")"
-| term0 "%" IDENT
-| term0
-]
-
-term0: [
-| atomic_constr
-| term_match
-| "(" term200 ")"
-| "{|" record_declaration bar_cbrace
-| "{" binder_constr "}"
-| "`{" term200 "}"
-| test_array_opening "[" "|" array_elems "|" lconstr type_cstr test_array_closing "|" "]" univ_annot
-| "`(" term200 ")"
-| "ltac" ":" "(" Pltac.ltac_expr ")"
-]
-
-array_elems: [
-| LIST0 lconstr SEP ";"
-]
-
-record_declaration: [
-| fields_def
-]
-
-fields_def: [
-| field_def ";" fields_def
-| field_def
-|
-]
-
-field_def: [
-| global binders ":=" lconstr
-]
-
-binder_constr: [
-| "forall" open_binders "," term200
-| "fun" open_binders "=>" term200
-| "let" name binders let_type_cstr ":=" term200 "in" term200
-| "let" "fix" fix_decl "in" term200
-| "let" "cofix" cofix_body "in" term200
-| "let" [ "(" LIST0 name SEP "," ")" | "()" ] as_return_type ":=" term200 "in" term200
-| "let" "'" pattern200 ":=" term200 "in" term200
-| "let" "'" pattern200 ":=" term200 case_type "in" term200
-| "let" "'" pattern200 "in" pattern200 ":=" term200 case_type "in" term200
-| "if" term200 as_return_type "then" term200 "else" term200
-| "fix" fix_decls
-| "cofix" cofix_decls
-| "if" term200 "is" ssr_dthen ssr_else      (* SSR plugin *)
-| "if" term200 "isn't" ssr_dthen ssr_else      (* SSR plugin *)
-| "let" ":" ssr_mpat ":=" lconstr "in" lconstr      (* SSR plugin *)
-| "let" ":" ssr_mpat ":=" lconstr ssr_rtype "in" lconstr      (* SSR plugin *)
-| "let" ":" ssr_mpat "in" pattern200 ":=" lconstr ssr_rtype "in" lconstr      (* SSR plugin *)
-]
-
-arg: [
-| test_lpar_id_coloneq "(" identref ":=" lconstr ")"
-| term9
-]
-
-atomic_constr: [
-| global univ_annot
-| sort
-| NUMBER
-| string
-| "_"
-| "?" "[" identref "]"
-| "?" "[" pattern_ident "]"
-| pattern_ident evar_instance
-]
-
-inst: [
-| identref ":=" lconstr
-]
-
-evar_instance: [
-| "@{" LIST1 inst SEP ";" "}"
-|
-]
-
-univ_annot: [
-| "@{" LIST0 universe_level "}"
-|
-]
-
-universe_level: [
-| "Set"
-| "Prop"
-| "Type"
-| "_"
-| global
-]
-
-fix_decls: [
-| fix_decl
-| fix_decl "with" LIST1 fix_decl SEP "with" "for" identref
-]
-
-cofix_decls: [
-| cofix_body
-| cofix_body "with" LIST1 cofix_body SEP "with" "for" identref
-]
-
-fix_decl: [
-| identref binders_fixannot type_cstr ":=" term200
-]
-
-cofix_body: [
-| identref binders type_cstr ":=" term200
-]
-
-term_match: [
-| "match" LIST1 case_item SEP "," OPT case_type "with" branches "end"
-]
-
-case_item: [
-| term100 OPT [ "as" name ] OPT [ "in" pattern200 ]
-]
-
-case_type: [
-| "return" term100
-]
-
-as_return_type: [
-| OPT [ OPT [ "as" name ] case_type ]
-]
-
-branches: [
-| OPT "|" LIST0 eqn SEP "|"
-]
-
-mult_pattern: [
-| LIST1 pattern200 SEP ","
-]
-
-eqn: [
-| LIST1 mult_pattern SEP "|" "=>" lconstr
-]
-
-record_pattern: [
-| global ":=" pattern200
-]
-
-record_patterns: [
-| record_pattern ";" record_patterns
-| record_pattern
-|
-]
-
-pattern200: [
-| pattern100
-]
-
-pattern100: [
-| pattern99 ":" term200
-| pattern99
-]
-
-pattern99: [
-| pattern90
-]
-
-pattern90: [
-| pattern10
-]
-
-pattern10: [
-| pattern1 "as" name
-| pattern1 LIST1 pattern1
-| "@" Prim.reference LIST0 pattern1
-| pattern1
-]
-
-pattern1: [
-| pattern0 "%" IDENT
-| pattern0
-]
-
-pattern0: [
-| Prim.reference
-| "{|" record_patterns bar_cbrace
-| "_"
-| "(" pattern200 ")"
-| "(" pattern200 "|" LIST1 pattern200 SEP "|" ")"
-| NUMBER
-| string
-]
-
-fixannot: [
-| "{" "struct" identref "}"
-| "{" "wf" constr identref "}"
-| "{" "measure" constr OPT identref OPT constr "}"
-]
-
-binders_fixannot: [
-| ensure_fixannot fixannot
-| binder binders_fixannot
-|
-]
-
-open_binders: [
-| name LIST0 name ":" lconstr
-| name LIST0 name binders
-| name ".." name
-| closed_binder binders
-]
-
-binders: [
-| LIST0 binder
-| Pcoq.Constr.binders
-]
-
-binder: [
-| name
-| closed_binder
-]
-
-closed_binder: [
-| "(" name LIST1 name ":" lconstr ")"
-| "(" name ":" lconstr ")"
-| "(" name ":=" lconstr ")"
-| "(" name ":" lconstr ":=" lconstr ")"
-| "{" name "}"
-| "{" name LIST1 name ":" lconstr "}"
-| "{" name ":" lconstr "}"
-| "{" name LIST1 name "}"
-| "[" name "]"
-| "[" name LIST1 name ":" lconstr "]"
-| "[" name ":" lconstr "]"
-| "[" name LIST1 name "]"
-| "`(" LIST1 typeclass_constraint SEP "," ")"
-| "`{" LIST1 typeclass_constraint SEP "," "}"
-| "`[" LIST1 typeclass_constraint SEP "," "]"
-| "'" pattern0
-| [ "of" | "&" ] term99      (* SSR plugin *)
-]
-
-one_open_binder: [
-| name
-| name ":" lconstr
-| one_closed_binder
-]
-
-one_closed_binder: [
-| "(" name ":" lconstr ")"
-| "{" name "}"
-| "{" name ":" lconstr "}"
-| "[" name "]"
-| "[" name ":" lconstr "]"
-| "'" pattern0
-]
-
-typeclass_constraint: [
-| "!" term200
-| "{" name "}" ":" [ "!" | ] term200
-| test_name_colon name ":" [ "!" | ] term200
-| term200
-]
-
-type_cstr: [
-| ":" lconstr
-|
-]
-
-let_type_cstr: [
-| OPT [ ":" lconstr ]
-]
-
-preident: [
-| IDENT
-]
-
-ident: [
-| IDENT
-]
-
-pattern_ident: [
-| LEFTQMARK ident
-]
-
-identref: [
-| ident
-]
-
-hyp: [
-| identref
-]
-
-field: [
-| FIELD
-]
-
-fields: [
-| field fields
-| field
-]
-
-fullyqualid: [
-| ident fields
-| ident
-]
-
-name: [
-| "_"
-| ident
-]
-
-reference: [
-| ident fields
-| ident
-]
-
-qualid: [
-| reference
-]
-
-by_notation: [
-| ne_string OPT [ "%" IDENT ]
-]
-
-smart_global: [
-| reference
-| by_notation
-]
-
-ne_string: [
-| STRING
-]
-
-ne_lstring: [
-| ne_string
-]
-
-dirpath: [
-| ident LIST0 field
-]
-
-string: [
-| STRING
-]
-
-lstring: [
-| string
-]
-
-integer: [
-| bigint
-]
-
-natural: [
-| bignat
-]
-
-bigint: [
-| bignat
-| test_minus_nat "-" bignat
-]
-
-bignat: [
-| NUMBER
-]
-
-bar_cbrace: [
-| test_pipe_closedcurly "|" "}"
-]
-
-strategy_level: [
-| "expand"
-| "opaque"
-| integer
-| "transparent"
-]
-
-vernac_toplevel: [
-| "Drop" "."
-| "Quit" "."
-| "BackTo" natural "."
-| test_show_goal "Show" "Goal" natural "at" natural "."
-| "Show" "Proof" "Diffs" OPT "removed" "."
-| Pvernac.Vernac_.main_entry
-]
-
 opt_hintbases: [
 |
 | ":" LIST1 IDENT
@@ -1467,6 +981,492 @@ binder_interp: [
 | "as" "strict" "pattern"
 ]
 
+vernac_toplevel: [
+| "Drop" "."
+| "Quit" "."
+| "BackTo" natural "."
+| test_show_goal "Show" "Goal" natural "at" natural "."
+| "Show" "Proof" "Diffs" OPT "removed" "."
+| Pvernac.Vernac_.main_entry
+]
+
+Constr.ident: [
+| Prim.ident
+]
+
+Prim.name: [
+| "_"
+]
+
+global: [
+| Prim.reference
+]
+
+constr_pattern: [
+| constr
+]
+
+cpattern: [
+| lconstr
+]
+
+sort: [
+| "Set"
+| "Prop"
+| "SProp"
+| "Type"
+| "Type" "@{" "_" "}"
+| "Type" "@{" universe "}"
+]
+
+sort_family: [
+| "Set"
+| "Prop"
+| "SProp"
+| "Type"
+]
+
+universe_increment: [
+| "+" natural
+|
+]
+
+universe_name: [
+| global
+| "Set"
+| "Prop"
+]
+
+universe_expr: [
+| universe_name universe_increment
+]
+
+universe: [
+| "max" "(" LIST1 universe_expr SEP "," ")"
+| universe_expr
+]
+
+lconstr: [
+| term200
+]
+
+constr: [
+| term8
+| "@" global univ_annot
+]
+
+term200: [
+| binder_constr
+| term100
+]
+
+term100: [
+| term99 "<:" term200
+| term99 "<<:" term200
+| term99 ":" term200
+| term99 ":>"
+| term99
+]
+
+term99: [
+| term90
+]
+
+term90: [
+| term10
+]
+
+term10: [
+| term9 LIST1 arg
+| "@" global univ_annot LIST0 term9
+| "@" pattern_ident LIST1 identref
+| term9
+]
+
+term9: [
+| ".." term0 ".."
+| term8
+]
+
+term8: [
+| term1
+]
+
+term1: [
+| term0 ".(" global LIST0 arg ")"
+| term0 ".(" "@" global LIST0 ( term9 ) ")"
+| term0 "%" IDENT
+| term0
+]
+
+term0: [
+| atomic_constr
+| term_match
+| "(" term200 ")"
+| "{|" record_declaration bar_cbrace
+| "{" binder_constr "}"
+| "`{" term200 "}"
+| test_array_opening "[" "|" array_elems "|" lconstr type_cstr test_array_closing "|" "]" univ_annot
+| "`(" term200 ")"
+| "ltac" ":" "(" Pltac.ltac_expr ")"
+]
+
+array_elems: [
+| LIST0 lconstr SEP ";"
+]
+
+record_declaration: [
+| fields_def
+]
+
+fields_def: [
+| field_def ";" fields_def
+| field_def
+|
+]
+
+field_def: [
+| global binders ":=" lconstr
+]
+
+binder_constr: [
+| "forall" open_binders "," term200
+| "fun" open_binders "=>" term200
+| "let" name binders let_type_cstr ":=" term200 "in" term200
+| "let" "fix" fix_decl "in" term200
+| "let" "cofix" cofix_body "in" term200
+| "let" [ "(" LIST0 name SEP "," ")" | "()" ] as_return_type ":=" term200 "in" term200
+| "let" "'" pattern200 ":=" term200 "in" term200
+| "let" "'" pattern200 ":=" term200 case_type "in" term200
+| "let" "'" pattern200 "in" pattern200 ":=" term200 case_type "in" term200
+| "if" term200 as_return_type "then" term200 "else" term200
+| "fix" fix_decls
+| "cofix" cofix_decls
+| "if" term200 "is" ssr_dthen ssr_else      (* SSR plugin *)
+| "if" term200 "isn't" ssr_dthen ssr_else      (* SSR plugin *)
+| "let" ":" ssr_mpat ":=" lconstr "in" lconstr      (* SSR plugin *)
+| "let" ":" ssr_mpat ":=" lconstr ssr_rtype "in" lconstr      (* SSR plugin *)
+| "let" ":" ssr_mpat "in" pattern200 ":=" lconstr ssr_rtype "in" lconstr      (* SSR plugin *)
+]
+
+arg: [
+| test_lpar_id_coloneq "(" identref ":=" lconstr ")"
+| term9
+]
+
+atomic_constr: [
+| global univ_annot
+| sort
+| NUMBER
+| string
+| "_"
+| "?" "[" identref "]"
+| "?" "[" pattern_ident "]"
+| pattern_ident evar_instance
+]
+
+inst: [
+| identref ":=" lconstr
+]
+
+evar_instance: [
+| "@{" LIST1 inst SEP ";" "}"
+|
+]
+
+univ_annot: [
+| "@{" LIST0 universe_level "}"
+|
+]
+
+universe_level: [
+| "Set"
+| "Prop"
+| "Type"
+| "_"
+| global
+]
+
+fix_decls: [
+| fix_decl
+| fix_decl "with" LIST1 fix_decl SEP "with" "for" identref
+]
+
+cofix_decls: [
+| cofix_body
+| cofix_body "with" LIST1 cofix_body SEP "with" "for" identref
+]
+
+fix_decl: [
+| identref binders_fixannot type_cstr ":=" term200
+]
+
+cofix_body: [
+| identref binders type_cstr ":=" term200
+]
+
+term_match: [
+| "match" LIST1 case_item SEP "," OPT case_type "with" branches "end"
+]
+
+case_item: [
+| term100 OPT [ "as" name ] OPT [ "in" pattern200 ]
+]
+
+case_type: [
+| "return" term100
+]
+
+as_return_type: [
+| OPT [ OPT [ "as" name ] case_type ]
+]
+
+branches: [
+| OPT "|" LIST0 eqn SEP "|"
+]
+
+mult_pattern: [
+| LIST1 pattern200 SEP ","
+]
+
+eqn: [
+| LIST1 mult_pattern SEP "|" "=>" lconstr
+]
+
+record_pattern: [
+| global ":=" pattern200
+]
+
+record_patterns: [
+| record_pattern ";" record_patterns
+| record_pattern
+|
+]
+
+pattern200: [
+| pattern100
+]
+
+pattern100: [
+| pattern99 ":" term200
+| pattern99
+]
+
+pattern99: [
+| pattern90
+]
+
+pattern90: [
+| pattern10
+]
+
+pattern10: [
+| pattern1 "as" name
+| pattern1 LIST1 pattern1
+| "@" Prim.reference LIST0 pattern1
+| pattern1
+]
+
+pattern1: [
+| pattern0 "%" IDENT
+| pattern0
+]
+
+pattern0: [
+| Prim.reference
+| "{|" record_patterns bar_cbrace
+| "_"
+| "(" pattern200 ")"
+| "(" pattern200 "|" LIST1 pattern200 SEP "|" ")"
+| NUMBER
+| string
+]
+
+fixannot: [
+| "{" "struct" identref "}"
+| "{" "wf" constr identref "}"
+| "{" "measure" constr OPT identref OPT constr "}"
+]
+
+binders_fixannot: [
+| ensure_fixannot fixannot
+| binder binders_fixannot
+|
+]
+
+open_binders: [
+| name LIST0 name ":" lconstr
+| name LIST0 name binders
+| name ".." name
+| closed_binder binders
+]
+
+binders: [
+| LIST0 binder
+| Pcoq.Constr.binders
+]
+
+binder: [
+| name
+| closed_binder
+]
+
+closed_binder: [
+| "(" name LIST1 name ":" lconstr ")"
+| "(" name ":" lconstr ")"
+| "(" name ":=" lconstr ")"
+| "(" name ":" lconstr ":=" lconstr ")"
+| "{" name "}"
+| "{" name LIST1 name ":" lconstr "}"
+| "{" name ":" lconstr "}"
+| "{" name LIST1 name "}"
+| "[" name "]"
+| "[" name LIST1 name ":" lconstr "]"
+| "[" name ":" lconstr "]"
+| "[" name LIST1 name "]"
+| "`(" LIST1 typeclass_constraint SEP "," ")"
+| "`{" LIST1 typeclass_constraint SEP "," "}"
+| "`[" LIST1 typeclass_constraint SEP "," "]"
+| "'" pattern0
+| [ "of" | "&" ] term99      (* SSR plugin *)
+]
+
+one_open_binder: [
+| name
+| name ":" lconstr
+| one_closed_binder
+]
+
+one_closed_binder: [
+| "(" name ":" lconstr ")"
+| "{" name "}"
+| "{" name ":" lconstr "}"
+| "[" name "]"
+| "[" name ":" lconstr "]"
+| "'" pattern0
+]
+
+typeclass_constraint: [
+| "!" term200
+| "{" name "}" ":" [ "!" | ] term200
+| test_name_colon name ":" [ "!" | ] term200
+| term200
+]
+
+type_cstr: [
+| ":" lconstr
+|
+]
+
+let_type_cstr: [
+| OPT [ ":" lconstr ]
+]
+
+preident: [
+| IDENT
+]
+
+ident: [
+| IDENT
+]
+
+pattern_ident: [
+| LEFTQMARK ident
+]
+
+identref: [
+| ident
+]
+
+hyp: [
+| identref
+]
+
+field: [
+| FIELD
+]
+
+fields: [
+| field fields
+| field
+]
+
+fullyqualid: [
+| ident fields
+| ident
+]
+
+name: [
+| "_"
+| ident
+]
+
+reference: [
+| ident fields
+| ident
+]
+
+qualid: [
+| reference
+]
+
+by_notation: [
+| ne_string OPT [ "%" IDENT ]
+]
+
+smart_global: [
+| reference
+| by_notation
+]
+
+ne_string: [
+| STRING
+]
+
+ne_lstring: [
+| ne_string
+]
+
+dirpath: [
+| ident LIST0 field
+]
+
+string: [
+| STRING
+]
+
+lstring: [
+| string
+]
+
+integer: [
+| bigint
+]
+
+natural: [
+| bignat
+]
+
+bigint: [
+| bignat
+| test_minus_nat "-" bignat
+]
+
+bignat: [
+| NUMBER
+]
+
+bar_cbrace: [
+| test_pipe_closedcurly "|" "}"
+]
+
+strategy_level: [
+| "expand"
+| "opaque"
+| integer
+| "transparent"
+]
+
 simple_tactic: [
 | "btauto"
 | "congruence"
diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar
index a34e96ac16..5674d28139 100644
--- a/doc/tools/docgram/orderedGrammar
+++ b/doc/tools/docgram/orderedGrammar
@@ -337,7 +337,7 @@ NOTINRSTS: [
 | q_destruction_arg
 | q_with_bindings
 | q_bindings
-| q_strategy_flag
+| q_reductions
 | q_reference
 | q_clause
 | q_occurrences
@@ -550,9 +550,9 @@ term_generalizing: [
 ]
 
 term_cast: [
+| term10 ":" type
 | term10 "<:" type
 | term10 "<<:" type
-| term10 ":" type
 | term10 ":>"
 ]
 
@@ -627,38 +627,38 @@ reduce: [
 ]
 
 red_expr: [
-| "red"
-| "hnf"
-| "simpl" OPT delta_flag OPT [ reference_occs | pattern_occs ]
-| "cbv" OPT strategy_flag
-| "cbn" OPT strategy_flag
-| "lazy" OPT strategy_flag
-| "compute" OPT delta_flag
+| "lazy" OPT reductions
+| "cbv" OPT reductions
+| "compute" OPT delta_reductions
 | "vm_compute" OPT [ reference_occs | pattern_occs ]
 | "native_compute" OPT [ reference_occs | pattern_occs ]
+| "red"
+| "hnf"
+| "simpl" OPT delta_reductions OPT [ reference_occs | pattern_occs ]
+| "cbn" OPT reductions
 | "unfold" LIST1 reference_occs SEP ","
 | "fold" LIST1 one_term
 | "pattern" LIST1 pattern_occs SEP ","
 | ident
 ]
 
-delta_flag: [
-| OPT "-" "[" LIST1 reference "]"
-]
-
-strategy_flag: [
-| LIST1 red_flag
-| delta_flag
+reductions: [
+| LIST1 reduction
+| delta_reductions
 ]
 
-red_flag: [
+reduction: [
 | "beta"
-| "iota"
+| "delta" OPT delta_reductions
 | "match"
 | "fix"
 | "cofix"
+| "iota"
 | "zeta"
-| "delta" OPT delta_flag
+]
+
+delta_reductions: [
+| OPT "-" "[" LIST1 reference "]"
 ]
 
 reference_occs: [
@@ -1242,6 +1242,10 @@ occurrences: [
 | "in" goal_occurrences
 ]
 
+simple_occurrences: [
+| occurrences
+]
+
 occs_nums: [
 | OPT "-" LIST1 nat_or_var
 ]
@@ -1741,7 +1745,7 @@ simple_tactic: [
 | "info_eauto" OPT nat_or_var OPT auto_using OPT hintbases
 | "dfs" "eauto" OPT nat_or_var OPT auto_using OPT hintbases
 | "bfs" "eauto" OPT nat_or_var OPT auto_using OPT hintbases
-| "autounfold" OPT hintbases OPT occurrences
+| "autounfold" OPT hintbases OPT simple_occurrences
 | "autounfold_one" OPT hintbases OPT ( "in" ident )
 | "unify" one_term one_term OPT ( "with" ident )
 | "typeclasses" "eauto" OPT "bfs" OPT nat_or_var OPT ( "with" LIST1 ident )
@@ -1811,17 +1815,17 @@ simple_tactic: [
 | "inversion" [ ident | natural ] OPT as_or_and_ipat OPT ( "in" LIST1 ident )
 | "inversion_clear" [ ident | natural ] OPT as_or_and_ipat OPT ( "in" LIST1 ident )
 | "inversion" [ ident | natural ] "using" one_term OPT ( "in" LIST1 ident )
-| "red" OPT occurrences
-| "hnf" OPT occurrences
-| "simpl" OPT delta_flag OPT [ reference_occs | pattern_occs ] OPT occurrences
-| "cbv" OPT strategy_flag OPT occurrences
-| "cbn" OPT strategy_flag OPT occurrences
-| "lazy" OPT strategy_flag OPT occurrences
-| "compute" OPT delta_flag OPT occurrences
+| "red" simple_occurrences
+| "hnf" simple_occurrences
+| "simpl" OPT delta_reductions OPT [ reference_occs | pattern_occs ] simple_occurrences
+| "cbv" OPT reductions simple_occurrences
+| "cbn" OPT reductions simple_occurrences
+| "lazy" OPT reductions simple_occurrences
+| "compute" OPT delta_reductions simple_occurrences
 | "vm_compute" OPT [ reference_occs | pattern_occs ] OPT occurrences
 | "native_compute" OPT [ reference_occs | pattern_occs ] OPT occurrences
 | "unfold" LIST1 reference_occs SEP "," OPT occurrences
-| "fold" LIST1 one_term OPT occurrences
+| "fold" LIST1 one_term simple_occurrences
 | "pattern" LIST1 pattern_occs SEP "," OPT occurrences
 | "change" OPT ( one_term OPT ( "at" occs_nums ) "with" ) one_term OPT occurrences
 | "change_no_check" OPT ( one_term OPT ( "at" occs_nums ) "with" ) one_term OPT occurrences
@@ -2139,13 +2143,13 @@ ltac2_goal_tactics: [
 | LIST0 ( OPT ltac2_expr ) SEP "|"      (* Ltac2 plugin *)
 ]
 
-q_strategy_flag: [
-| ltac2_strategy_flag      (* Ltac2 plugin *)
+q_reductions: [
+| ltac2_reductions      (* Ltac2 plugin *)
 ]
 
-ltac2_strategy_flag: [
+ltac2_reductions: [
 | LIST1 ltac2_red_flag      (* Ltac2 plugin *)
-| OPT ltac2_delta_flag      (* Ltac2 plugin *)
+| OPT ltac2_delta_reductions      (* Ltac2 plugin *)
 ]
 
 ltac2_red_flag: [
@@ -2155,10 +2159,10 @@ ltac2_red_flag: [
 | "fix"      (* Ltac2 plugin *)
 | "cofix"      (* Ltac2 plugin *)
 | "zeta"      (* Ltac2 plugin *)
-| "delta" OPT ltac2_delta_flag      (* Ltac2 plugin *)
+| "delta" OPT ltac2_delta_reductions      (* Ltac2 plugin *)
 ]
 
-ltac2_delta_flag: [
+ltac2_delta_reductions: [
 | OPT "-" "[" LIST1 refglobal "]"
 ]