Add global version of OPTINREF

5 files changed, 27 insertions, 242 deletions

diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst
index b912bcbdf8..81c497d60a 100644
--- a/doc/sphinx/proof-engine/ltac2.rst
+++ b/doc/sphinx/proof-engine/ltac2.rst
@@ -1633,7 +1633,7 @@ Here is the syntax for the :n:`q_*` nonterminals:
 .. insertprodn ltac2_oriented_rewriter ltac2_rewriter
 
 .. prodn::
-   ltac2_oriented_rewriter ::= {| -> | <- } @ltac2_rewriter
+   ltac2_oriented_rewriter ::= {? {| -> | <- } } @ltac2_rewriter
    ltac2_rewriter ::= {? @natural } {? {| ? | ! } } @ltac2_constr_with_bindings
 
 .. insertprodn ltac2_for_each_goal ltac2_goal_tactics
diff --git a/doc/tools/docgram/README.md b/doc/tools/docgram/README.md
index dbb04bb6a6..6c507e1d57 100644
--- a/doc/tools/docgram/README.md
+++ b/doc/tools/docgram/README.md
@@ -179,6 +179,8 @@ grammar with its productions and removing the non-terminal. Each should appear
 as a separate production.  (Doesn't work recursively; splicing for both
 `A: [ | B ]` and `B: [ | C ]` must be done in separate SPLICE operations.)
 
+`OPTINREF` - applies the local `OPTINREF` edit to every nonterminal
+
 `EXPAND` - expands LIST0, LIST1, LIST* ... SEP and OPT constructs into
 new non-terminals
 
diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg
index 97d479b238..76a41828f7 100644
--- a/doc/tools/docgram/common.edit_mlg
+++ b/doc/tools/docgram/common.edit_mlg
@@ -202,10 +202,6 @@ for_each_goal: [
 | OPT ( goal_tactics "|" ) OPT ltac_expr5 ".." OPT ( "|" goal_tactics )
 ]
 
-tactic_then_last: [
-| OPTINREF
-]
-
 ltac2_tactic_then_last: [
 | REPLACE "|" LIST0 ( OPT ltac2_expr6 ) SEP "|"      (* Ltac2 plugin *)
 | WITH LIST0 (  "|" OPT ltac2_expr6 )  TAG Ltac2
@@ -222,10 +218,6 @@ ltac2_for_each_goal: [
 | OPT ( ltac2_goal_tactics "|" ) OPT ltac2_expr6 ".." OPT ( "|" ltac2_goal_tactics )  TAG Ltac2
 ]
 
-ltac2_tactic_then_last: [
-| OPTINREF
-]
-
 reference: [ | DELETENT ]
 
 reference: [
@@ -530,14 +522,6 @@ eqn: [
 | WITH LIST1 [ LIST1 pattern100 SEP "," ] SEP "|" "=>" lconstr
 ]
 
-universe_increment: [
-| OPTINREF
-]
-
-evar_instance: [
-| OPTINREF
-]
-
 (* No constructor syntax, OPT [ "|" binders ] is not supported for Record *)
 record_definition: [
 | opt_coercion ident_decl binders OPT [ ":" sort ] OPT ( ":=" OPT [ identref ] "{" record_fields "}" )
@@ -632,14 +616,6 @@ def_body: [
 | WITH LIST0 binder ":" type
 ]
 
-reduce: [
-| OPTINREF
-]
-
-occs: [
-| OPTINREF
-]
-
 delta_flag: [
 | REPLACE "-" "[" LIST1 smart_global "]"
 | WITH OPT "-" "[" LIST1 smart_global "]"
@@ -653,7 +629,6 @@ ltac2_delta_flag: [
 
 ltac2_branches: [
 | EDIT ADD_OPT "|" LIST1 branch SEP "|"      (* Ltac2 plugin *)
-| OPTINREF
 ]
 
 strategy_flag: [
@@ -662,7 +637,6 @@ strategy_flag: [
 (*| REPLACE LIST1 red_flags
 | WITH LIST1 red_flag*)
 | (* empty *)
-| OPTINREF
 ]
 
 filtered_import: [
@@ -671,20 +645,14 @@ filtered_import: [
 | DELETE global
 ]
 
-functor_app_annot: [
-| OPTINREF
-]
-
 is_module_expr: [
 | REPLACE ":=" module_expr_inl LIST0 ext_module_expr
 | WITH ":=" LIST1 module_expr_inl SEP "<+"
-| OPTINREF
 ]
 
 is_module_type: [
 | REPLACE ":=" module_type_inl LIST0 ext_module_type
 | WITH ":=" LIST1 module_type_inl SEP "<+"
-| OPTINREF
 ]
 
 gallina_ext: [
@@ -729,10 +697,6 @@ gallina_ext: [
 | WITH "From" dirpath "Require" export_token LIST1 global
 ]
 
-export_token: [
-| OPTINREF
-]
-
 (* lexer stuff *)
 LEFTQMARK: [
 | "?"
@@ -1319,10 +1283,6 @@ command: [
 | WITH "Goal" type
 ]
 
-option_setting: [
-| OPTINREF
-]
-
 syntax: [
 | REPLACE "Open" "Scope" IDENT
 | WITH "Open" "Scope" scope
@@ -1435,7 +1395,6 @@ cofix_definition: [
 type_cstr: [
 | REPLACE ":" lconstr
 | WITH ":" type
-| OPTINREF
 ]
 
 inductive_definition: [
@@ -1460,10 +1419,6 @@ record_binder: [
 | DELETE name
 ]
 
-at_level_opt: [
-| OPTINREF
-]
-
 query_command: [
 | REPLACE "Eval" red_expr "in" lconstr "."
 | WITH "Eval" red_expr "in" lconstr
@@ -1498,10 +1453,6 @@ vernac_toplevel: [
 | DELETE vernac_control
 ]
 
-in_or_out_modules: [
-| OPTINREF
-]
-
 vernac_control: [
 (* replacing vernac_control with command is cheating a little;
    they can't refer to the vernac_toplevel commands.
@@ -1517,90 +1468,8 @@ vernac_control: [
 | DELETE decorated_vernac
 ]
 
-orient: [
-| OPTINREF
-]
-
-in_hyp_as: [
-| OPTINREF
-]
-
-as_name: [
-| OPTINREF
-]
-
-hloc: [
-| OPTINREF
-]
-
-as_or_and_ipat: [
-| OPTINREF
-]
-
-hintbases: [
-| OPTINREF
-]
-
-as_ipat: [
-| OPTINREF
-]
-
-auto_using: [
-| OPTINREF
-]
-
-with_bindings: [
-| OPTINREF
-]
-
-eqn_ipat: [
-| OPTINREF
-]
-
-withtac: [
-| OPTINREF
-]
-
 of_module_type: [
 | (* empty *)
-| OPTINREF
-]
-
-
-clause_dft_all: [
-| OPTINREF
-]
-
-opt_clause: [
-| OPTINREF
-]
-
-with_names: [
-| OPTINREF
-]
-
-in_hyp_list: [
-| OPTINREF
-]
-
-struct_annot: [
-| OPTINREF
-]
-
-firstorder_using: [
-| OPTINREF
-]
-
-fun_ind_using: [
-| OPTINREF
-]
-
-by_arg_tac: [
-| OPTINREF
-]
-
-by_tactic: [
-| OPTINREF
 ]
 
 rewriter: [
@@ -1647,43 +1516,18 @@ record_declaration: [
 
 fields_def: [ | DELETENT ]
 
-hint_info: [
-| OPTINREF
-]
-
-debug: [
-| OPTINREF
-]
-
-eauto_search_strategy: [
-| OPTINREF
-]
-
-
 constr_body: [
 | DELETE ":=" lconstr
 | REPLACE ":" lconstr ":=" lconstr
 | WITH OPT ( ":" type ) ":=" lconstr
 ]
 
-opt_hintbases: [
-| OPTINREF
-]
-
-opthints: [
-| OPTINREF
-]
-
 scheme: [
 | DELETE scheme_kind
 | REPLACE identref ":=" scheme_kind
 | WITH OPT ( identref ":=" ) scheme_kind
 ]
 
-instance_name: [
-| OPTINREF
-]
-
 simple_reserv: [
 | REPLACE LIST1 identref ":" lconstr
 | WITH LIST1 identref ":" type
@@ -1702,22 +1546,9 @@ ltac2_in_clause: [
 | DELETE LIST0 ltac2_hypident_occ SEP ","      (* Ltac2 plugin *)
 ]
 
-concl_occ: [
-| OPTINREF
-]
-
-opt_coercion: [
-| OPTINREF
-]
-
-opt_constructors_or_fields: [
-| OPTINREF
-]
-
 decl_notations: [
 | REPLACE "where" LIST1 decl_notation SEP decl_sep
 | WITH "where" decl_notation LIST0 (decl_sep decl_notation )
-| OPTINREF
 ]
 
 module_expr: [
@@ -1778,15 +1609,6 @@ decl_notation: [
 | WITH ne_lstring ":=" constr syntax_modifiers OPT [ ":" scope_name ]
 ]
 
-syntax_modifiers: [
-| OPTINREF
-]
-
-
-only_parsing: [
-| OPTINREF
-]
-
 ltac_production_item: [
 | REPLACE ident "(" ident OPT ltac_production_sep ")"
 | WITH ident OPT ( "(" ident OPT ltac_production_sep ")" )
@@ -2024,10 +1846,6 @@ DELETE: [
 | test_ltac1_env
 ]
 
-mut_flag: [
-| OPTINREF
-]
-
 rec_flag: [
 | OPTINREF
 ]
@@ -2081,7 +1899,6 @@ tac2rec_fieldexprs: [
 | DELETE tac2rec_fieldexpr ";"
 | DELETE tac2rec_fieldexpr
 | LIST1 tac2rec_fieldexpr OPT ";"
-| OPTINREF
 ]
 
 tac2rec_fields: [
@@ -2089,7 +1906,6 @@ tac2rec_fields: [
 | DELETE tac2rec_field ";"
 | DELETE tac2rec_field
 | LIST1 tac2rec_field SEP ";" OPT ";" TAG Ltac2
-| OPTINREF
 ]
 
 (* todo: weird productions, ints only after an initial "-"??:
@@ -2103,46 +1919,6 @@ ltac2_occs_nums: [
 | 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
@@ -2177,14 +1953,9 @@ SPLICE: [
 | 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
@@ -2233,8 +2004,8 @@ q_clause: [
 ]
 
 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
+| REPLACE ltac2_destruction_arg ltac2_as_or_and_ipat ltac2_eqn_ipat OPT clause      (* Ltac2 plugin *)
+| WITH ltac2_destruction_arg ltac2_as_or_and_ipat ltac2_eqn_ipat OPT ltac2_clause  TAG Ltac2
 ]
 
 starredidentref: [
@@ -2464,6 +2235,11 @@ SPLICE: [
 | number_string_mapping
 | number_options
 | string_option
+| tac2type_body
+| tac2rec_fields
+| mut_flag
+| tac2rec_fieldexprs
+| syn_level
 ] (* end SPLICE *)
 
 RENAME: [
@@ -2500,11 +2276,6 @@ simple_tactic: [
 | qualid LIST1 tactic_arg
 ]
 
-(* todo: doesn't work if up above... maybe because 'clause' doesn't exist? *)
-clause_dft_concl: [
-| OPTINREF
-]
-
 SPLICE: [
 | gallina
 | gallina_ext
diff --git a/doc/tools/docgram/doc_grammar.ml b/doc/tools/docgram/doc_grammar.ml
index 92bcd51528..96eaff2895 100644
--- a/doc/tools/docgram/doc_grammar.ml
+++ b/doc/tools/docgram/doc_grammar.ml
@@ -1190,6 +1190,15 @@ let edit_all_prods g op eprods =
   | "DELETE" -> do_it op eprods 1; true
   | "SPLICE" -> do_it op eprods 1; true
   | "MERGE" -> do_it op eprods 2; true
+  | "OPTINREF" ->
+      List.iter (fun nt ->
+        let prods = NTMap.find nt !g.map in
+        if has_match [] prods then begin
+          let prods' = remove_prod [] prods nt in
+          g_update_prods g nt prods';
+          global_repl g [(Snterm nt)] [(Sopt (Snterm nt))]
+        end)
+      !g.order; true
   | "EXPAND" ->
     if List.length eprods > 1 || List.length (List.hd eprods) <> 0 then
       error "'EXPAND:' expects a single empty production\n";
@@ -2007,10 +2016,13 @@ let report_omitted_prods g seen label split =
         (if first = "" then nt else first), nt, n + 1, total + 1)
     ("", "", 0, 0) !g.order in
   maybe_warn first last n;
-(*    List.iter (fun nt ->
-        if not (NTMap.mem nt seen || (List.mem nt included)) then
-          warn "%s %s not included in .rst files\n" "Nonterminal" nt)
-      !g.order;*)
+  (*
+  Printf.printf "\n";
+  NTMap.iter (fun nt _ ->
+      if not (NTMap.mem nt seen || (List.mem nt included)) then
+        warn "%s %s not included in .rst files\n" "Nonterminal" nt)
+    !g.map;
+  *)
   if total <> 0 then
     Printf.eprintf "TOTAL %ss not included = %d\n" label total
 
diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar
index 75c0ca1453..94a6fa730b 100644
--- a/doc/tools/docgram/orderedGrammar
+++ b/doc/tools/docgram/orderedGrammar
@@ -1837,7 +1837,7 @@ q_rewriting: [
 ]
 
 ltac2_oriented_rewriter: [
-| [ "->" | "<-" ] ltac2_rewriter      (* Ltac2 plugin *)
+| OPT [ "->" | "<-" ] ltac2_rewriter      (* Ltac2 plugin *)
 ]
 
 ltac2_rewriter: [