Merge PR #13343: Update syntax in auto.rst chapter

Reviewed-by: Zimmi48
Ack-by: JasonGross

5 files changed, 287 insertions, 356 deletions

diff --git a/doc/tools/docgram/README.md b/doc/tools/docgram/README.md
index 6c507e1d57..ba5876ff76 100644
--- a/doc/tools/docgram/README.md
+++ b/doc/tools/docgram/README.md
@@ -181,9 +181,6 @@ as a separate production.  (Doesn't work recursively; splicing for both
 
 `OPTINREF` - applies the local `OPTINREF` edit to every nonterminal
 
-`EXPAND` - expands LIST0, LIST1, LIST* ... SEP and OPT constructs into
-new non-terminals
-
 ### Local edits
 
 `DELETE <production>` - removes the specified production from the grammar
@@ -201,6 +198,9 @@ that appear in the specified production:
   The current version handles a single USE_NT or ADD_OPT per EDIT.  These symbols
   may appear in the middle of the production given in the EDIT.
 
+`APPENDALL <symbols>` - inserts <symbols> at the end of every production in
+<edited_nt>.
+
 `INSERTALL <symbols>` - inserts <symbols> at the beginning of every production in
 <edited_nt>.
 
@@ -212,10 +212,12 @@ that appear in the specified production:
 | WITH <newprod>
 ```
 
+`COPYALL <destination>` - creates a new nonterminal `<destination>` and copies
+all the productions in the nonterminal to `<destination>`.
+
 `MOVETO <destination> <production>` - moves the production to `<destination>` and,
  if needed, creates a new production <edited_nt> -> \<destination>.
 
-
 `MOVEALLBUT <destination>` - moves all the productions in the nonterminal to `<destination>`
 *except* for the productions following the `MOVEALLBUT` production in the edit script
 (terminated only by the closing `]`).
diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg
index 4080eaae08..8efda825de 100644
--- a/doc/tools/docgram/common.edit_mlg
+++ b/doc/tools/docgram/common.edit_mlg
@@ -19,8 +19,22 @@ lglob: [
 ]
 
 hint: [
+| REPLACE "Resolve" "->" LIST1 global OPT natural
+| WITH "Resolve" [ "->" | "<-" ] LIST1 global OPT natural
+| DELETE "Resolve" "<-" LIST1 global OPT natural
+| REPLACE "Variables" "Transparent"
+| WITH [ "Constants" | "Variables" ] [ "Transparent" | "Opaque" ]
+| DELETE "Variables" "Opaque"
+| DELETE "Constants" "Transparent"
+| DELETE "Constants" "Opaque"
+| REPLACE "Transparent" LIST1 global
+| WITH [ "Transparent" | "Opaque" ] LIST1 global
+| DELETE "Opaque" LIST1 global
+
 | REPLACE "Extern" natural OPT Constr.constr_pattern "=>" Pltac.tactic
 | WITH "Extern" natural OPT constr_pattern "=>" tactic
+| INSERTALL "Hint"
+| APPENDALL opt_hintbases
 ]
 
 (* todo: does ARGUMENT EXTEND make the symbol global? It is in both extraargs and extratactics *)
@@ -149,6 +163,7 @@ DELETE: [
 | ensure_fixannot
 | test_array_opening
 | test_array_closing
+| test_variance_ident
 
   (* SSR *)
 | ssr_null_entry
@@ -267,7 +282,7 @@ binder_constr: [
 | REPLACE "if" term200 "is" ssr_dthen ssr_else
 | WITH "if" term200 [ "is" | "isn't" ] ssr_dthen ssr_else  TAG SSR
 | DELETE "if" term200 "isn't" ssr_dthen ssr_else
-| DELETE "if" term200 [ "is" | "isn't" ] ssr_dthen ssr_else  TAG SSR  (* todo: restore for SSR *)
+| DELETE "if" term200 [ "is" | "isn't" ] ssr_dthen ssr_else  TAG SSR  (* todo: restore as "MOVETO term_if" for SSR *)
 | MOVETO term_fix "let" "fix" fix_decl "in" term200
 | MOVETO term_cofix "let" "cofix" cofix_body "in" term200
 | MOVETO term_let "let" [ "(" LIST0 name SEP "," ")" | "()" ] as_return_type ":=" term200 "in" term200
@@ -597,6 +612,11 @@ univ_decl: [
 | WITH    "@{" LIST0 identref  OPT "+"  OPT [ "|" LIST0 univ_constraint SEP "," OPT "+" ] "}"
 ]
 
+cumul_univ_decl: [
+| REPLACE "@{" LIST0 variance_identref [ "+" | ]     [ "|" LIST0 univ_constraint SEP "," [ "+" | ] "}" | [ "}" | bar_cbrace ] ]
+| WITH "@{" LIST0 variance_identref    OPT "+"   OPT [ "|" LIST0 univ_constraint SEP "," OPT "+" ] "}"
+]
+
 of_type: [
 | DELETENT
 ]
@@ -905,12 +925,13 @@ where: [
 ]
 
 simple_tactic: [
-| DELETE "intros"
-| REPLACE "intros" ne_intropatterns
-| WITH "intros" intropatterns
-| DELETE "eintros"
-| REPLACE "eintros" ne_intropatterns
-| WITH "eintros" intropatterns
+| REPLACE "eauto" OPT nat_or_var OPT nat_or_var auto_using hintbases
+| WITH "eauto" OPT nat_or_var auto_using hintbases
+| REPLACE "debug" "eauto" OPT nat_or_var OPT nat_or_var auto_using hintbases
+| WITH "debug" "eauto" OPT nat_or_var auto_using hintbases
+| REPLACE "info_eauto" OPT nat_or_var OPT nat_or_var auto_using hintbases
+| WITH "info_eauto" OPT nat_or_var auto_using hintbases
+
 | DELETE "autorewrite" "with" LIST1 preident clause
 | DELETE "autorewrite" "with" LIST1 preident clause "using" tactic
 | DELETE "autorewrite" "*" "with" LIST1 preident clause
@@ -966,6 +987,12 @@ simple_tactic: [
 | DELETE "intro" "after" hyp
 | DELETE "intro" "before" hyp
 | "intro" OPT ident OPT where
+| DELETE "intros"
+| REPLACE "intros" ne_intropatterns
+| WITH "intros" intropatterns
+| DELETE "eintros"
+| REPLACE "eintros" ne_intropatterns
+| WITH "eintros" intropatterns
 | DELETE "move" hyp "at" "top"
 | DELETE "move" hyp "at" "bottom"
 | DELETE "move" hyp "after" hyp
@@ -1139,6 +1166,10 @@ printable: [
 | REPLACE [ "Sorted" | ] "Universes" OPT printunivs_subgraph OPT ne_string
 | WITH OPT "Sorted" "Universes" OPT printunivs_subgraph OPT ne_string
 | DELETE "Term" smart_global OPT univ_name_list  (* readded in commands *)
+| REPLACE "Hint"
+| WITH "Hint" OPT [ "*" | smart_global ]
+| DELETE "Hint" smart_global
+| DELETE "Hint" "*"
 
 | INSERTALL "Print"
 ]
@@ -1163,6 +1194,8 @@ scheme_kind: [
 command: [
 | REPLACE "Print" printable
 | WITH printable
+| REPLACE "Hint" hint opt_hintbases
+| WITH hint
 | "SubClass" ident_decl def_body
 | REPLACE "Ltac" LIST1 ltac_tacdef_body SEP "with"
 | WITH "Ltac" ltac_tacdef_body LIST0 ( "with" ltac_tacdef_body )
@@ -1242,6 +1275,9 @@ command: [
 | REPLACE "Preterm" "of" ident
 | WITH "Preterm" OPT ( "of" ident )
 | DELETE "Preterm"
+| REPLACE "Proof" "using" section_var_expr "with" Pltac.tactic
+| WITH "Proof" "using" section_subset_expr OPT [ "with" ltac_expr5 ]
+| DELETE "Proof" "using" section_var_expr
 
 (* hide the fact that table names are limited to 2 IDENTs *)
 | REPLACE "Remove" IDENT IDENT LIST1 table_value
@@ -1441,8 +1477,8 @@ 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
+| REPLACE opt_coercion cumul_ident_decl binders OPT [ "|" binders ] OPT [ ":" lconstr ] opt_constructors_or_fields decl_notations
+| WITH    opt_coercion cumul_ident_decl binders OPT [ "|" binders ] OPT [ ":" type ]    opt_constructors_or_fields decl_notations
 ]
 
 (* note that constructor -> identref constructor_type *)
@@ -1578,9 +1614,12 @@ simple_reserv: [
 
 in_clause: [
 | DELETE in_clause'
-| REPLACE LIST0 hypident_occ SEP "," "|-" concl_occ
-| WITH LIST0 hypident_occ SEP "," OPT ( "|-" concl_occ )
-| DELETE LIST0 hypident_occ SEP ","
+| REPLACE LIST1 hypident_occ SEP "," "|-" concl_occ
+| WITH LIST1 hypident_occ SEP "," OPT ( "|-" concl_occ )
+| DELETE LIST1 hypident_occ SEP ","
+| REPLACE "*" occs
+| WITH concl_occ
+(* todo: perhaps concl_occ should be "*" | "at" occs_nums *)
 ]
 
 ltac2_in_clause: [
@@ -1791,6 +1830,7 @@ tactic_notation_tactics: [
 | "field_simplify" OPT ( "[" LIST1 constr "]" ) LIST1 constr OPT ( "in" ident )
 | "field_simplify_eq" OPT ( "[" LIST1 constr "]" ) OPT ( "in" ident )
 | "intuition" OPT ltac_expr5  (* todo: Not too keen on things like "with_power_flags" in tauto.ml, not easy to follow *)
+| "now" ltac_expr5
 | "nsatz" OPT ( "with" "radicalmax" ":=" constr "strategy" ":=" constr "parameters" ":=" constr "variables" ":=" constr )
 | "psatz" constr OPT nat_or_var
 | "ring" OPT ( "[" LIST1 constr "]" )
@@ -1942,6 +1982,18 @@ tac2rec_fields: [
 | LIST1 tac2rec_field SEP ";" OPT ";" TAG Ltac2
 ]
 
+int_or_var: [
+| REPLACE integer
+| WITH [ integer | identref ]
+| DELETE identref
+]
+
+nat_or_var: [
+| REPLACE natural
+| WITH [ natural | identref ]
+| DELETE identref
+]
+
 ltac2_occs_nums: [
 | DELETE LIST1 nat_or_anti      (* Ltac2 plugin *)
 | REPLACE "-" nat_or_anti LIST0 nat_or_anti      (* Ltac2 plugin *)
@@ -2387,6 +2439,33 @@ attribute: [
 | DELETE "using" OPT attr_value
 ]
 
+hypident: [
+(* todo: restore for SSR *)
+| DELETE "(" "type" "of" ident ")"      (* SSR plugin *)
+| DELETE "(" "value" "of" ident ")"      (* SSR plugin *)
+]
+
+ref_or_pattern_occ: [
+| DELETE smart_global OPT occs
+| DELETE constr OPT occs
+| unfold_occ
+| pattern_occ
+]
+
+clause_dft_concl: [
+(* omit an OPT since clause_dft_concl is always OPT *)
+| REPLACE OPT occs
+| WITH occs
+]
+
+occs_nums: [
+| EDIT ADD_OPT "-" LIST1 nat_or_var
+]
+
+variance_identref: [
+| EDIT ADD_OPT variance identref
+]
+
 SPLICE: [
 | clause
 | noedit_mode
@@ -2526,6 +2605,7 @@ SPLICE: [
 | eliminator  (* todo: splice or not? *)
 | quoted_attributes  (* todo: splice or not? *)
 | printable
+| hint
 | only_parsing
 | record_fields
 | constructor_type
@@ -2606,9 +2686,18 @@ SPLICE: [
 | syn_level
 | firstorder_rhs
 | firstorder_using
+| hints_path_atom
+| ref_or_pattern_occ
+| cumul_ident_decl
+| variance
+| variance_identref
 ] (* end SPLICE *)
 
 RENAME: [
+| occurrences rewrite_occs
+]
+
+RENAME: [
 | 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 *)
@@ -2652,6 +2741,13 @@ RENAME: [
 | ssrclauses ssr_in
 | ssrcpat ssrblockpat
 | constr_pattern one_pattern
+| hints_path hints_regexp
+| clause_dft_concl occurrences
+| in_clause goal_occurrences
+| unfold_occ reference_occs
+| pattern_occ pattern_occs
+| hypident_occ hyp_occs
+| concl_occ concl_occs
 ]
 
 simple_tactic: [
diff --git a/doc/tools/docgram/doc_grammar.ml b/doc/tools/docgram/doc_grammar.ml
index 92a745c863..dd7990368e 100644
--- a/doc/tools/docgram/doc_grammar.ml
+++ b/doc/tools/docgram/doc_grammar.ml
@@ -527,28 +527,28 @@ let rec edit_SELF nt cur_level next_level right_assoc inner prod =
   prod
 
 
-let autoloaded_mlgs = [ (* in the order they are loaded by Coq *)
+let autoloaded_mlgs = [ (* productions from other mlgs are marked with TAGs *)
  "parsing/g_constr.mlg";
  "parsing/g_prim.mlg";
- "vernac/g_vernac.mlg";
- "vernac/g_proofs.mlg";
- "toplevel/g_toplevel.mlg";
- "plugins/ltac/extraargs.mlg";
- "plugins/ltac/g_obligations.mlg";
+ "plugins/btauto/g_btauto.mlg";
+ "plugins/cc/g_congruence.mlg";
+ "plugins/firstorder/g_ground.mlg";
  "plugins/ltac/coretactics.mlg";
+ "plugins/ltac/extraargs.mlg";
  "plugins/ltac/extratactics.mlg";
- "plugins/ltac/profile_ltac_tactics.mlg";
  "plugins/ltac/g_auto.mlg";
  "plugins/ltac/g_class.mlg";
- "plugins/ltac/g_rewrite.mlg";
  "plugins/ltac/g_eqdecide.mlg";
- "plugins/ltac/g_tactic.mlg";
  "plugins/ltac/g_ltac.mlg";
- "plugins/btauto/g_btauto.mlg";
+ "plugins/ltac/g_obligations.mlg";
+ "plugins/ltac/g_rewrite.mlg";
+ "plugins/ltac/g_tactic.mlg";
+ "plugins/ltac/profile_ltac_tactics.mlg";
  "plugins/rtauto/g_rtauto.mlg";
- "plugins/cc/g_congruence.mlg";
- "plugins/firstorder/g_ground.mlg";
  "plugins/syntax/g_number_string.mlg";
+ "toplevel/g_toplevel.mlg";
+ "vernac/g_proofs.mlg";
+ "vernac/g_vernac.mlg";
 ]
 
 
@@ -1020,7 +1020,7 @@ let rec gen_nt_name sym =
   good_name name
 
 (* create a new nt for LIST* or OPT with the specified name *)
-let rec maybe_add_nt g insert_after name sym queue =
+let maybe_add_nt g insert_after name sym queue =
   let empty = [Snterm "empty"] in
   let maybe_unwrap ?(multi=false) sym =
     match sym with
@@ -1094,65 +1094,6 @@ let rec maybe_add_nt g insert_after name sym queue =
   end;
   new_nt
 
-(* expand LIST*, OPT and add "empty" *)
-(* todo: doesn't handle recursive expansions well, such as syntax_modifier_opt *)
-and expand_rule g edited_nt queue =
-  let rule = NTMap.find edited_nt !g.map in
-  let insert_after = ref edited_nt in
-  let rec expand rule =
-    let rec aux syms res =
-      match syms with
-      | [] -> res
-      | sym0 :: tl ->
-        let new_sym = match sym0 with
-          | Sterm _
-          | Snterm _ ->
-            sym0
-          | Slist1 sym
-          | Slist1sep (sym, _)
-          | Slist0 sym
-          | Slist0sep (sym, _)
-          | Sopt sym ->
-            let name = gen_nt_name sym in
-            if name <> "" then begin
-              let new_nt = maybe_add_nt g insert_after name sym0 queue in
-              Snterm new_nt
-            end else sym0
-          | Sparen slist -> Sparen (expand slist)
-          | Sprod slistlist ->
-            let has_empty = List.length (List.hd (List.rev slistlist)) = 0 in
-            let name = gen_nt_name sym0 in
-            if name <> "" then begin
-              let new_nt = maybe_add_nt g insert_after name
-                  (if has_empty then (Sopt (Sprod (List.rev (List.tl (List.rev slistlist))) ))
-                  else sym0) queue
-              in
-              Snterm new_nt
-            end else
-              Sprod (List.map expand slistlist)
-          | Sedit _
-          | Sedit2 _ ->
-            sym0 (* these constructors not used here *)
-        in
-        aux tl (new_sym :: res)
-    in
-    List.rev (aux rule (if edited_nt <> "empty" && ematch rule [] then [Snterm "empty"] else []))
-  in
-  let rule' = List.map expand rule in
-  g_update_prods g edited_nt rule'
-
-let expand_lists g =
-  (* todo: use Queue.of_seq w OCaml 4.07+ *)
-  let queue = Queue.create () in
-  List.iter (fun nt -> Queue.add nt queue) !g.order;
-  try
-    while true do
-      let nt = Queue.pop queue in
-      expand_rule g nt queue
-    done
-  with
-  | Queue.Empty -> ()
-
 let apply_merge g edit_map =
   List.iter (fun b ->
       let (from_nt, to_nt) = b in
@@ -1213,10 +1154,6 @@ let edit_all_prods g op eprods =
           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";
-    expand_lists g; true
   | _ -> false
 
 let edit_single_prod g edit0 prods nt =
@@ -1281,6 +1218,11 @@ let apply_edit_file g edits =
             with Not_found -> prods in
             let prods' = moveto nt dest_nt oprod prods in
             aux tl prods' add_nt
+          | [Snterm "COPYALL"; Snterm dest_nt] :: tl ->
+            if NTMap.mem dest_nt !g.map then
+              error "COPYALL target nonterminal `%s` already exists\n" dest_nt;
+            g_maybe_add g dest_nt prods;
+            aux tl prods add_nt
           | [Snterm "MOVEALLBUT"; Snterm dest_nt] :: tl ->
             List.iter (fun tlprod ->
                 if not (List.mem tlprod prods) then
@@ -1300,6 +1242,8 @@ let apply_edit_file g edits =
             aux tl (remove_prod [] prods nt) add_nt
           | (Snterm "INSERTALL" :: syms) :: tl ->
             aux tl (List.map (fun p -> syms @ p) prods) add_nt
+          | (Snterm "APPENDALL" :: syms) :: tl ->
+            aux tl (List.map (fun p -> p @ syms) prods) add_nt
           | (Snterm "PRINT" :: _) :: tl ->
             pr_prods nt prods;
             aux tl prods add_nt
@@ -1395,56 +1339,6 @@ let nt_subset_in_orig_order g nts =
   let subset = StringSet.of_list nts in
   List.filter (fun nt -> StringSet.mem nt subset) !g.order
 
-let print_chunk out g seen fmt title starts ends =
-  fprintf out "\n\n%s:\n%s\n" title header;
-  List.iter (fun start ->
-      let nts = (nt_closure g start ends) in
-      print_in_order out g fmt (nt_subset_in_orig_order g nts) !seen;
-      seen := StringSet.union !seen (StringSet.of_list nts))
-    starts
-
-let print_chunks g out fmt () =
-  let seen = ref StringSet.empty in
-  print_chunk out g seen fmt "lconstr" ["lconstr"] ["binder_constr"; "tactic_expr5"];
-  print_chunk out g seen fmt "Gallina syntax of terms" ["binder_constr"] ["tactic_expr5"];
-  print_chunk out g seen fmt "Gallina The Vernacular" ["gallina"] ["tactic_expr5"];
-  print_chunk out g seen fmt "intropattern_list_opt" ["intropattern_list"; "or_and_intropattern_loc"] ["operconstr"; "tactic_expr5"];
-  print_chunk out g seen fmt "simple_tactic" ["simple_tactic"]
-    ["tactic_expr5"; "tactic_expr3"; "tactic_expr2"; "tactic_expr1"; "tactic_expr0"];
-
-  (*print_chunk out g seen fmt "Ltac" ["tactic_expr5"] [];*)
-  print_chunk out g seen fmt "Ltac" ["tactic_expr5"] ["tactic_expr4"];
-  print_chunk out g seen fmt "Ltac 4" ["tactic_expr4"] ["tactic_expr3"; "tactic_expr2"];
-  print_chunk out g seen fmt "Ltac 3" ["tactic_expr3"] ["tactic_expr2"];
-  print_chunk out g seen fmt "Ltac 2" ["tactic_expr2"] ["tactic_expr1"];
-  print_chunk out g seen fmt "Ltac 1" ["tactic_expr1"] ["tactic_expr0"];
-  print_chunk out g seen fmt "Ltac 0" ["tactic_expr0"] [];
-
-
-  print_chunk out g seen fmt "command" ["command"] [];
-  print_chunk out g seen fmt "vernac_toplevel" ["vernac_toplevel"] [];
-  print_chunk out g seen fmt "vernac_control" ["vernac_control"] []
-
-  (*
-    let ssr_tops = ["ssr_dthen"; "ssr_else"; "ssr_mpat"; "ssr_rtype"] in
-    seen := StringSet.union !seen (StringSet.of_list ssr_tops);
-
-    print_chunk out g seen fmt "ssrindex" ["ssrindex"] [];
-    print_chunk out g seen fmt "command" ["command"] [];
-    print_chunk out g seen fmt "binder_constr" ["binder_constr"] [];
-    (*print_chunk out g seen fmt "closed_binder" ["closed_binder"] [];*)
-    print_chunk out g seen fmt "gallina_ext" ["gallina_ext"] [];
-    (*print_chunk out g seen fmt "hloc" ["hloc"] [];*)
-    (*print_chunk out g seen fmt "hypident" ["hypident"] [];*)
-    print_chunk out g seen fmt "simple_tactic" ["simple_tactic"] [];
-    print_chunk out g seen fmt "tactic_expr" ["tactic_expr4"; "tactic_expr1"; "tactic_expr0"] [];
-    fprintf out "\n\nRemainder:\n";
-    print_in_order g (List.filter (fun x -> not (StringSet.mem x !seen)) !g.order) StringSet.empty;
-  *)
-
-
-    (*seen := StringSet.diff !seen (StringSet.of_list ssr_tops);*)
-    (*print_chunk out g seen fmt "vernac_toplevel" ["vernac_toplevel"] [];*)
 let index_of str list =
   let rec index_of_r str list index =
     match list with
@@ -1478,89 +1372,6 @@ let get_range g start end_ =
 
 let get_rangeset g start end_ = StringSet.of_list (get_range g start end_)
 
-let print_dominated g =
-  let info nt rangeset exclude =
-    let reachable = StringSet.of_list (nt_closure g nt exclude) in
-    let unreachable = StringSet.of_list (nt_closure g (List.hd start_symbols) (nt::exclude)) in
-    let dominated = StringSet.diff reachable unreachable in
-    Printf.printf "For %s, 'attribute' is: reachable = %b, unreachable = %b, dominated = %b\n" nt
-        (StringSet.mem "attribute" reachable)
-        (StringSet.mem "attribute" unreachable)
-        (StringSet.mem "attribute" dominated);
-    Printf.printf "  rangeset = %b excluded = %b\n"
-        (StringSet.mem "attribute" rangeset)
-        (List.mem "attribute" exclude);
-    reachable, dominated
-  in
-  let pr3 nt rangeset reachable dominated =
-    let missing = StringSet.diff dominated rangeset in
-    if not (StringSet.is_empty missing) then begin
-      Printf.printf "\nMissing in range for '%s':\n" nt;
-      StringSet.iter (fun nt -> Printf.printf "  %s\n" nt) missing
-    end;
-
-    let unneeded = StringSet.diff rangeset reachable in
-    if not (StringSet.is_empty unneeded) then begin
-      Printf.printf "\nUnneeded in range for '%s':\n" nt;
-      StringSet.iter (fun nt -> Printf.printf "  %s\n" nt) unneeded
-    end;
-  in
-  let pr2 nt rangeset exclude =
-    let reachable, dominated = info nt rangeset exclude in
-    pr3 nt rangeset reachable dominated
-  in
-  let pr nt end_ = pr2 nt (get_rangeset g nt end_) [] in
-
-  let ssr_ltac = ["ssr_first_else"; "ssrmmod"; "ssrdotac"; "ssrortacarg";
-      "ssrparentacarg"] in
-  let ssr_tac = ["ssrintrosarg"; "ssrhintarg"; "ssrtclarg"; "ssrseqarg"; "ssrmovearg";
-      "ssrrpat"; "ssrclauses"; "ssrcasearg"; "ssrarg"; "ssrapplyarg"; "ssrexactarg";
-      "ssrcongrarg"; "ssrterm"; "ssrrwargs"; "ssrunlockargs"; "ssrfixfwd"; "ssrcofixfwd";
-      "ssrfwdid"; "ssrposefwd"; "ssrsetfwd"; "ssrdgens"; "ssrhavefwdwbinders"; "ssrhpats_nobs";
-      "ssrhavefwd"; "ssrsufffwd"; "ssrwlogfwd"; "ssrhint"; "ssrclear"; "ssr_idcomma";
-      "ssrrwarg"; "ssrintros_ne"; "ssrhint3arg" ] @ ssr_ltac in
-  let ssr_cmd = ["ssr_modlocs"; "ssr_search_arg"; "ssrhintref"; "ssrhintref_list";
-      "ssrviewpos"; "ssrviewposspc"] in
-  let ltac = ["ltac_expr"; "ltac_expr0"; "ltac_expr1"; "ltac_expr2"; "ltac_expr3"] in
-  let term = ["term"; "term0"; "term1"; "term10"; "term100"; "term9";
-      "pattern"; "pattern0"; "pattern1"; "pattern10"] in
-
-  pr "term" "constr";
-
-  let ltac_rangeset = List.fold_left StringSet.union StringSet.empty
-                            [(get_rangeset g "ltac_expr" "tactic_atom");
-                            (get_rangeset g "toplevel_selector" "range_selector");
-                            (get_rangeset g "ltac_match_term" "match_pattern");
-                            (get_rangeset g "ltac_match_goal" "match_pattern_opt")] in
-  pr2 "ltac_expr" ltac_rangeset ("simple_tactic" :: ssr_tac);
-
-  let dec_vern_rangeset = get_rangeset g "decorated_vernac" "opt_coercion" in
-  let dev_vern_excl =
-      ["gallina_ext"; "command"; "tactic_mode"; "syntax"; "command_entry"] @ term @ ltac @ ssr_tac in
-  pr2 "decorated_vernac" dec_vern_rangeset dev_vern_excl;
-
-  let simp_tac_range = get_rangeset g "simple_tactic" "hypident_occ_list_comma" in
-  let simp_tac_excl = ltac @ ssr_tac in
-  pr2 "simple_tactic" simp_tac_range simp_tac_excl;
-
-  let cmd_range = get_rangeset g "command" "int_or_id_list_opt" in
-  let cmd_excl = ssr_tac @ ssr_cmd in
-  pr2 "command" cmd_range cmd_excl;
-
-  let syn_range = get_rangeset g "syntax" "constr_as_binder_kind" in
-  let syn_excl = ssr_tac @ ssr_cmd in
-  pr2 "syntax" syn_range syn_excl;
-
-  let gext_range = get_rangeset g "gallina_ext" "Structure_opt" in
-  let gext_excl = ssr_tac @ ssr_cmd in
-  pr2 "gallina_ext" gext_range gext_excl;
-
-  let qry_range = get_rangeset g "query_command" "searchabout_query_list" in
-  let qry_excl = ssr_tac @ ssr_cmd in
-  pr2 "query_command" qry_range qry_excl
-
-  (* todo: tactic_mode *)
-
 let check_range_consistency g start end_ =
   let defined_list = get_range g start end_ in
   let defined = StringSet.of_list defined_list in
@@ -1913,13 +1724,8 @@ let process_rst g file args seen tac_prods cmd_prods =
     end
   in
 
-(*  let skip_files = ["doc/sphinx/proof-engine/ltac.rst"; "doc/sphinx/proof-engine/ltac2.rst";*)
-(*    "doc/sphinx/proof-engine/ssreflect-proof-language.rst"]*)
-(*  in*)
-
   let cmd_exclude_files = [
     "doc/sphinx/proof-engine/ssreflect-proof-language.rst";
-    "doc/sphinx/proofs/automatic-tactics/auto.rst";
     "doc/sphinx/proofs/writing-proofs/rewriting.rst";
     "doc/sphinx/proofs/writing-proofs/proof-mode.rst";
     "doc/sphinx/proof-engine/tactics.rst";
@@ -2101,7 +1907,6 @@ let process_grammar args =
       close_out out;
       finish_with_file (dir "orderedGrammar") args;
 (*      check_singletons g*)
-(*      print_dominated g*)
 
       let seen = ref { nts=NTMap.empty; tacs=NTMap.empty; tacvs=NTMap.empty; cmds=NTMap.empty; cmdvs=NTMap.empty } in
       let args = { args with no_update = false } in (* always update rsts in place for now *)
diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar
index d01f66c6d7..cf90eea5a1 100644
--- a/doc/tools/docgram/fullGrammar
+++ b/doc/tools/docgram/fullGrammar
@@ -342,6 +342,21 @@ closed_binder: [
 | [ "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
@@ -875,10 +890,29 @@ univ_decl: [
 | "@{" LIST0 identref [ "+" | ] [ "|" LIST0 univ_constraint SEP "," [ "+" | ] "}" | [ "}" | bar_cbrace ] ]
 ]
 
+variance: [
+| "+"
+| "="
+| "*"
+]
+
+variance_identref: [
+| identref
+| test_variance_ident variance identref
+]
+
+cumul_univ_decl: [
+| "@{" LIST0 variance_identref [ "+" | ] [ "|" LIST0 univ_constraint SEP "," [ "+" | ] "}" | [ "}" | bar_cbrace ] ]
+]
+
 ident_decl: [
 | identref OPT univ_decl
 ]
 
+cumul_ident_decl: [
+| identref OPT cumul_univ_decl
+]
+
 finite_token: [
 | "Inductive"
 | "CoInductive"
@@ -918,7 +952,7 @@ opt_constructors_or_fields: [
 ]
 
 inductive_definition: [
-| opt_coercion ident_decl binders OPT [ "|" binders ] OPT [ ":" lconstr ] opt_constructors_or_fields decl_notations
+| opt_coercion cumul_ident_decl binders OPT [ "|" binders ] OPT [ ":" lconstr ] opt_constructors_or_fields decl_notations
 ]
 
 constructors_or_record: [
@@ -1914,8 +1948,9 @@ in_clause: [
 | in_clause'
 | "*" occs
 | "*" "|-" concl_occ
-| LIST0 hypident_occ SEP "," "|-" concl_occ
-| LIST0 hypident_occ SEP ","
+| "|-" concl_occ
+| LIST1 hypident_occ SEP "," "|-" concl_occ
+| LIST1 hypident_occ SEP ","
 ]
 
 test_lpar_id_colon: [
@@ -2493,7 +2528,7 @@ in_hyp_list: [
 ]
 
 in_hyp_as: [
-| "in" id_or_meta as_ipat
+| "in" LIST1 [ id_or_meta as_ipat ] SEP ","
 |
 ]
 
diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar
index f62dd8f731..7c709baa48 100644
--- a/doc/tools/docgram/orderedGrammar
+++ b/doc/tools/docgram/orderedGrammar
@@ -436,7 +436,7 @@ univ_decl: [
 ]
 
 cumul_univ_decl: [
-| "@{" LIST0 ( OPT [ "=" | "+" | "*" ] ident ) OPT "+" OPT [ "|" LIST0 univ_constraint SEP "," OPT "+" ] "}"
+| "@{" LIST0 ( OPT [ "+" | "=" | "*" ] ident ) OPT "+" OPT [ "|" LIST0 univ_constraint SEP "," OPT "+" ] "}"
 ]
 
 univ_constraint: [
@@ -512,6 +512,21 @@ binder: [
 | "'" pattern0
 ]
 
+one_open_binder: [
+| name
+| name ":" term
+| one_closed_binder
+]
+
+one_closed_binder: [
+| "(" name ":" term ")"
+| "{" name "}"
+| "{" name ":" term "}"
+| "[" name "]"
+| "[" name ":" term "]"
+| "'" pattern0
+]
+
 implicit_binders: [
 | "{" LIST1 name OPT ( ":" type ) "}"
 | "[" LIST1 name OPT ( ":" type ) "]"
@@ -614,16 +629,16 @@ reduce: [
 red_expr: [
 | "red"
 | "hnf"
-| "simpl" OPT delta_flag OPT ref_or_pattern_occ
+| "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
-| "vm_compute" OPT ref_or_pattern_occ
-| "native_compute" OPT ref_or_pattern_occ
-| "unfold" LIST1 unfold_occ SEP ","
+| "vm_compute" OPT [ reference_occs | pattern_occs ]
+| "native_compute" OPT [ reference_occs | pattern_occs ]
+| "unfold" LIST1 reference_occs SEP ","
 | "fold" LIST1 one_term
-| "pattern" LIST1 pattern_occ SEP ","
+| "pattern" LIST1 pattern_occs SEP ","
 | ident
 ]
 
@@ -646,31 +661,11 @@ red_flag: [
 | "delta" OPT delta_flag
 ]
 
-ref_or_pattern_occ: [
+reference_occs: [
 | reference OPT ( "at" occs_nums )
-| one_term OPT ( "at" occs_nums )
-]
-
-occs_nums: [
-| LIST1 nat_or_var
-| "-" LIST1 nat_or_var
-]
-
-int_or_var: [
-| integer
-| ident
 ]
 
-nat_or_var: [
-| natural
-| ident
-]
-
-unfold_occ: [
-| reference OPT ( "at" occs_nums )
-]
-
-pattern_occ: [
+pattern_occs: [
 | one_term OPT ( "at" occs_nums )
 ]
 
@@ -705,7 +700,7 @@ field_def: [
 ]
 
 inductive_definition: [
-| OPT ">" cumul_ident_decl LIST0 binder OPT [ "|" LIST0 binder ] OPT [ ":" type ] OPT ( ":=" OPT constructors_or_record ) OPT decl_notations
+| OPT ">" ident OPT cumul_univ_decl LIST0 binder OPT [ "|" LIST0 binder ] OPT [ ":" type ] OPT ( ":=" OPT constructors_or_record ) OPT decl_notations
 ]
 
 constructors_or_record: [
@@ -717,10 +712,6 @@ constructor: [
 | ident LIST0 binder OPT of_type
 ]
 
-cumul_ident_decl: [
-| ident OPT cumul_univ_decl
-]
-
 filtered_import: [
 | qualid OPT [ "(" LIST1 ( qualid OPT [ "(" ".." ")" ] ) SEP "," ")" ]
 ]
@@ -901,9 +892,7 @@ command: [
 | "Print" "Typing" "Flags"
 | "Print" "Tables"
 | "Print" "Options"
-| "Print" "Hint"
-| "Print" "Hint" reference
-| "Print" "Hint" "*"
+| "Print" "Hint" OPT [ "*" | reference ]
 | "Print" "HintDb" ident
 | "Print" "Scopes"
 | "Print" "Scope" scope_name
@@ -958,7 +947,6 @@ command: [
 | "Extract" "Inductive" qualid "=>" [ ident | string ] "[" LIST0 [ ident | string ] "]" OPT string      (* extraction plugin *)
 | "Show" "Extraction"      (* extraction plugin *)
 | "Proof"
-| "Proof" "using" section_var_expr
 | "Proof" "Mode" string
 | "Proof" term
 | "Abort" OPT [ "All" | ident ]
@@ -983,7 +971,6 @@ command: [
 | "Guarded"
 | "Create" "HintDb" ident OPT "discriminated"
 | "Remove" "Hints" LIST1 qualid OPT ( ":" LIST1 ident )
-| "Hint" hint OPT ( ":" LIST1 ident )
 | "Comments" LIST0 [ one_term | string | natural ]
 | "Declare" "Instance" ident_decl LIST0 binder ":" term OPT hint_info
 | "Declare" "Scope" scope_name
@@ -1030,7 +1017,7 @@ command: [
 | "Print" "Rings"      (* ring plugin *)
 | "Add" "Field" ident ":" one_term OPT ( "(" LIST1 field_mod SEP "," ")" )      (* ring plugin *)
 | "Print" "Fields"      (* ring plugin *)
-| "Hint" "Cut" "[" hints_path "]" OPT ( ":" LIST1 ident )
+| "Hint" "Cut" "[" hints_regexp "]" OPT ( ":" LIST1 ident )
 | "Prenex" "Implicits" LIST1 qualid      (* SSR plugin *)
 | "Print" "Hint" "View" OPT ssrviewpos      (* SSR plugin *)
 | "Hint" "View" OPT ssrviewpos LIST1 ( one_term OPT ( "|" natural ) )      (* SSR plugin *)
@@ -1039,7 +1026,7 @@ command: [
 | "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 "with" ltac_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
@@ -1142,6 +1129,15 @@ command: [
 | "Ltac2" "Notation" [ string | lident ] ":=" ltac2_expr      (* Ltac2 plugin *)
 | "Ltac2" "Eval" ltac2_expr      (* Ltac2 plugin *)
 | "Print" "Ltac2" qualid      (* Ltac2 plugin *)
+| "Hint" "Resolve" LIST1 [ qualid | one_term ] OPT hint_info OPT ( ":" LIST1 ident )
+| "Hint" "Resolve" [ "->" | "<-" ] LIST1 qualid OPT natural OPT ( ":" LIST1 ident )
+| "Hint" "Immediate" LIST1 [ qualid | one_term ] OPT ( ":" LIST1 ident )
+| "Hint" [ "Constants" | "Variables" ] [ "Transparent" | "Opaque" ] OPT ( ":" LIST1 ident )
+| "Hint" [ "Transparent" | "Opaque" ] LIST1 qualid OPT ( ":" LIST1 ident )
+| "Hint" "Mode" qualid LIST1 [ "+" | "!" | "-" ] OPT ( ":" LIST1 ident )
+| "Hint" "Unfold" LIST1 qualid OPT ( ":" LIST1 ident )
+| "Hint" "Constructors" LIST1 qualid OPT ( ":" LIST1 ident )
+| "Hint" "Extern" natural OPT one_pattern "=>" ltac_expr OPT ( ":" LIST1 ident )
 | "Time" sentence
 | "Redirect" string sentence
 | "Timeout" natural sentence
@@ -1205,23 +1201,6 @@ univ_name_list: [
 | "@{" LIST0 name "}"
 ]
 
-hint: [
-| "Resolve" LIST1 [ qualid | one_term ] OPT hint_info
-| "Resolve" "->" LIST1 qualid OPT natural
-| "Resolve" "<-" LIST1 qualid OPT natural
-| "Immediate" LIST1 [ qualid | one_term ]
-| "Variables" "Transparent"
-| "Variables" "Opaque"
-| "Constants" "Transparent"
-| "Constants" "Opaque"
-| "Transparent" LIST1 qualid
-| "Opaque" LIST1 qualid
-| "Mode" qualid LIST1 [ "+" | "!" | "-" ]
-| "Unfold" LIST1 qualid
-| "Constructors" LIST1 qualid
-| "Extern" natural OPT one_pattern "=>" ltac_expr
-]
-
 tacdef_body: [
 | qualid LIST0 name [ ":=" | "::=" ] ltac_expr
 ]
@@ -1275,28 +1254,37 @@ constr_with_bindings_arg: [
 | OPT ">" one_term OPT ( "with" bindings )      (* SSR plugin *)
 ]
 
-clause_dft_concl: [
-| "in" in_clause
-| OPT ( "at" occs_nums )
+occurrences: [
+| "at" occs_nums
+| "in" goal_occurrences
 ]
 
-in_clause: [
-| "*" OPT ( "at" occs_nums )
-| "*" "|-" OPT concl_occ
-| LIST0 hypident_occ SEP "," OPT ( "|-" OPT concl_occ )
+occs_nums: [
+| OPT "-" LIST1 nat_or_var
 ]
 
-hypident_occ: [
+nat_or_var: [
+| [ natural | ident ]
+]
+
+goal_occurrences: [
+| LIST1 hyp_occs SEP "," OPT ( "|-" OPT concl_occs )
+| "*" "|-" OPT concl_occs
+| "|-" OPT concl_occs
+| OPT concl_occs
+]
+
+hyp_occs: [
 | hypident OPT ( "at" occs_nums )
 ]
 
 hypident: [
 | ident
-| "(" "type" "of" ident ")"      (* SSR plugin *)
-| "(" "value" "of" ident ")"      (* SSR plugin *)
+| "(" "type" "of" ident ")"
+| "(" "value" "of" ident ")"
 ]
 
-concl_occ: [
+concl_occs: [
 | "*" OPT ( "at" occs_nums )
 ]
 
@@ -1545,15 +1533,15 @@ number_string_via: [
 | "via" qualid "mapping" "[" LIST1 [ qualid "=>" qualid | "[" qualid "]" "=>" qualid ] SEP "," "]"
 ]
 
-hints_path: [
-| "(" hints_path ")"
-| hints_path "*"
-| "emp"
-| "eps"
-| hints_path "|" hints_path
+hints_regexp: [
 | LIST1 qualid
 | "_"
-| hints_path hints_path
+| hints_regexp "|" hints_regexp
+| hints_regexp hints_regexp
+| hints_regexp "*"
+| "emp"
+| "eps"
+| "(" hints_regexp ")"
 ]
 
 class: [
@@ -1630,7 +1618,7 @@ simple_tactic: [
 | "constructor" OPT nat_or_var OPT ( "with" bindings )
 | "econstructor" OPT ( nat_or_var OPT ( "with" bindings ) )
 | "specialize" one_term OPT ( "with" bindings ) OPT ( "as" simple_intropattern )
-| "symmetry" OPT ( "in" in_clause )
+| "symmetry" OPT ( "in" goal_occurrences )
 | "split" OPT ( "with" bindings )
 | "esplit" OPT ( "with" bindings )
 | "exists" OPT ( LIST1 bindings SEP "," )
@@ -1648,8 +1636,8 @@ simple_tactic: [
 | "clear" "-" LIST1 ident
 | "clearbody" LIST1 ident
 | "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
+| "replace" one_term "with" one_term OPT occurrences OPT ( "by" ltac_expr3 )
+| "replace" OPT [ "->" | "<-" ] one_term OPT occurrences
 | "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
@@ -1701,9 +1689,9 @@ simple_tactic: [
 | "decompose" "record" one_term
 | "absurd" one_term
 | "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 )
+| "autorewrite" OPT "*" "with" LIST1 ident OPT occurrences OPT ( "using" ltac_expr )
+| "rewrite" "*" OPT [ "->" | "<-" ] one_term OPT ( "in" ident ) OPT ( "at" rewrite_occs OPT ( "by" ltac_expr3 ) )
+| "rewrite" "*" OPT [ "->" | "<-" ] one_term "at" rewrite_occs "in" ident OPT ( "by" ltac_expr3 )
 | "refine" one_term
 | "simple" "refine" one_term
 | "notypeclasses" "refine" one_term
@@ -1764,13 +1752,13 @@ simple_tactic: [
 | "auto" OPT nat_or_var OPT auto_using OPT hintbases
 | "info_auto" OPT nat_or_var OPT auto_using OPT hintbases
 | "debug" "auto" OPT nat_or_var OPT auto_using OPT hintbases
-| "eauto" OPT nat_or_var OPT nat_or_var OPT auto_using OPT hintbases
+| "eauto" OPT nat_or_var OPT auto_using OPT hintbases
 | "new" "auto" OPT nat_or_var OPT auto_using OPT hintbases
-| "debug" "eauto" OPT nat_or_var OPT nat_or_var OPT auto_using OPT hintbases
-| "info_eauto" OPT nat_or_var OPT nat_or_var OPT auto_using OPT hintbases
+| "debug" "eauto" OPT nat_or_var OPT auto_using OPT hintbases
+| "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 clause_dft_concl
+| "autounfold" OPT hintbases OPT occurrences
 | "autounfold_one" OPT hintbases OPT ( "in" ident )
 | "unify" one_term one_term OPT ( "with" ident )
 | "convert_concl_no_check" one_term
@@ -1784,8 +1772,8 @@ simple_tactic: [
 | "rewrite_strat" rewstrategy OPT ( "in" ident )
 | "rewrite_db" ident OPT ( "in" ident )
 | "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_rewrite" OPT [ "->" | "<-" ] one_term OPT ( "with" bindings ) OPT ( "at" rewrite_occs ) OPT ( "in" ident )
+| "setoid_rewrite" OPT [ "->" | "<-" ] one_term OPT ( "with" bindings ) "in" ident "at" rewrite_occs
 | "setoid_symmetry" OPT ( "in" ident )
 | "setoid_reflexivity"
 | "setoid_transitivity" one_term
@@ -1808,10 +1796,10 @@ simple_tactic: [
 | "pose" one_term OPT as_name
 | "epose" bindings_with_parameters
 | "epose" one_term OPT as_name
-| "set" bindings_with_parameters OPT clause_dft_concl
-| "set" one_term OPT as_name OPT clause_dft_concl
-| "eset" bindings_with_parameters OPT clause_dft_concl
-| "eset" one_term OPT as_name OPT clause_dft_concl
+| "set" bindings_with_parameters OPT occurrences
+| "set" one_term OPT as_name OPT occurrences
+| "eset" bindings_with_parameters OPT occurrences
+| "eset" one_term OPT as_name OPT occurrences
 | "remember" one_term OPT as_name OPT eqn_ipat OPT clause_dft_all
 | "eremember" one_term OPT as_name OPT eqn_ipat OPT clause_dft_all
 | "assert" "(" ident ":=" term ")"
@@ -1829,32 +1817,32 @@ simple_tactic: [
 | "enough" one_term OPT as_ipat OPT ( "by" ltac_expr3 )
 | "eenough" one_term OPT as_ipat OPT ( "by" ltac_expr3 )
 | "generalize" one_term OPT ( LIST1 one_term )
-| "generalize" one_term OPT ( "at" occs_nums ) OPT as_name LIST0 [ "," pattern_occ OPT as_name ]
+| "generalize" one_term OPT ( "at" occs_nums ) OPT as_name LIST0 [ "," pattern_occs OPT as_name ]
 | "induction" induction_clause_list
 | "einduction" induction_clause_list
 | "destruct" induction_clause_list
 | "edestruct" induction_clause_list
-| "rewrite" LIST1 oriented_rewriter SEP "," OPT clause_dft_concl OPT ( "by" ltac_expr3 )
-| "erewrite" LIST1 oriented_rewriter SEP "," OPT clause_dft_concl OPT ( "by" ltac_expr3 )
+| "rewrite" LIST1 oriented_rewriter SEP "," OPT occurrences OPT ( "by" ltac_expr3 )
+| "erewrite" LIST1 oriented_rewriter SEP "," OPT occurrences OPT ( "by" ltac_expr3 )
 | "dependent" [ "simple" "inversion" | "inversion" | "inversion_clear" ] [ ident | natural ] OPT as_or_and_ipat OPT [ "with" one_term ]
 | "simple" "inversion" [ ident | natural ] OPT as_or_and_ipat OPT ( "in" LIST1 ident )
 | "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 clause_dft_concl
-| "hnf" OPT clause_dft_concl
-| "simpl" OPT delta_flag OPT ref_or_pattern_occ OPT clause_dft_concl
-| "cbv" OPT strategy_flag OPT clause_dft_concl
-| "cbn" OPT strategy_flag OPT clause_dft_concl
-| "lazy" OPT strategy_flag OPT clause_dft_concl
-| "compute" OPT delta_flag OPT clause_dft_concl
-| "vm_compute" OPT ref_or_pattern_occ OPT clause_dft_concl
-| "native_compute" OPT ref_or_pattern_occ OPT clause_dft_concl
-| "unfold" LIST1 unfold_occ SEP "," OPT clause_dft_concl
-| "fold" LIST1 one_term OPT clause_dft_concl
-| "pattern" LIST1 pattern_occ SEP "," OPT clause_dft_concl
-| "change" conversion OPT clause_dft_concl
-| "change_no_check" conversion OPT clause_dft_concl
+| "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
+| "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
+| "pattern" LIST1 pattern_occs SEP "," OPT occurrences
+| "change" conversion OPT occurrences
+| "change_no_check" conversion OPT occurrences
 | "btauto"
 | "rtauto"
 | "congruence" OPT natural OPT ( "with" LIST1 one_term )
@@ -1946,6 +1934,7 @@ simple_tactic: [
 | "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
+| "now" ltac_expr
 | "nsatz" OPT ( "with" "radicalmax" ":=" one_term "strategy" ":=" one_term "parameters" ":=" one_term "variables" ":=" one_term )
 | "psatz" one_term OPT nat_or_var
 | "ring" OPT ( "[" LIST1 one_term "]" )
@@ -1998,19 +1987,24 @@ induction_clause_list: [
 | LIST1 induction_clause SEP "," OPT ( "using" one_term OPT ( "with" bindings ) ) OPT opt_clause
 ]
 
-induction_clause: [
-| destruction_arg OPT as_or_and_ipat OPT eqn_ipat OPT opt_clause
-]
-
 opt_clause: [
-| "in" in_clause
+| "in" goal_occurrences
 | "at" occs_nums
 ]
 
+induction_clause: [
+| destruction_arg OPT as_or_and_ipat OPT eqn_ipat OPT opt_clause
+]
+
 auto_using: [
 | "using" LIST1 one_term SEP ","
 ]
 
+hintbases: [
+| "with" "*"
+| "with" LIST1 ident
+]
+
 or_and_intropattern: [
 | "[" intropattern_or_list_or "]"
 | "(" LIST0 simple_intropattern SEP "," ")"
@@ -2055,6 +2049,10 @@ bindings: [
 | LIST1 one_term
 ]
 
+int_or_var: [
+| [ integer | ident ]
+]
+
 comparison: [
 | "="
 | "<"
@@ -2063,11 +2061,6 @@ comparison: [
 | ">="
 ]
 
-hintbases: [
-| "with" "*"
-| "with" LIST1 ident
-]
-
 bindings_with_parameters: [
 | "(" ident LIST0 simple_binder ":=" term ")"
 ]
@@ -2436,11 +2429,11 @@ tac2mode: [
 ]
 
 clause_dft_all: [
-| "in" in_clause
+| "in" goal_occurrences
 ]
 
 in_hyp_as: [
-| "in" ident OPT as_ipat
+| "in" LIST1 [ ident OPT as_ipat ] SEP ","
 ]
 
 simple_binder: [
@@ -2470,7 +2463,7 @@ func_scheme_def: [
 | ident ":=" "Induction" "for" qualid "Sort" sort_family      (* funind plugin *)
 ]
 
-occurrences: [
+rewrite_occs: [
 | LIST1 integer
 | ident
 ]