4 files changed, 40 insertions, 23 deletions
diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg
index 116fcaa87b..816acba4c1 100644
--- a/doc/tools/docgram/common.edit_mlg
+++ b/doc/tools/docgram/common.edit_mlg
@@ -1939,11 +1939,6 @@ tac2rec_fields: [
 | LIST1 tac2rec_field SEP ";" OPT ";" TAG Ltac2
 ]
 
-(* todo: weird productions, ints only after an initial "-"??:
-  occs_nums: [
-  | LIST1 [ natural | ident ]
-  | "-" [ natural | ident ] LIST0 int_or_var
-*)
 ltac2_occs_nums: [
 | DELETE LIST1 nat_or_anti      (* Ltac2 plugin *)
 | REPLACE "-" nat_or_anti LIST0 nat_or_anti      (* Ltac2 plugin *)
@@ -2481,7 +2476,6 @@ SPLICE: [
 | binders
 | casted_constr
 | check_module_types
-| constr_pattern
 | decl_sep
 | function_fix_definition (* loses funind annotation *)
 | glob
@@ -2655,6 +2649,7 @@ RENAME: [
 | ssrfwd ssrdefbody
 | ssrclauses ssr_in
 | ssrcpat ssrblockpat
+| constr_pattern one_pattern
 ]
 
 simple_tactic: [
diff --git a/doc/tools/docgram/dune b/doc/tools/docgram/dune
index 2a7b283f55..1c07d00d4f 100644
--- a/doc/tools/docgram/dune
+++ b/doc/tools/docgram/dune
@@ -12,7 +12,6 @@
    (glob_files %{project_root}/parsing/*.mlg)
    (glob_files %{project_root}/toplevel/*.mlg)
    (glob_files %{project_root}/vernac/*.mlg)
-   ; All plugins except SSReflect for now (mimicking what is done in Makefile.doc)
    (glob_files %{project_root}/plugins/btauto/*.mlg)
    (glob_files %{project_root}/plugins/cc/*.mlg)
    (glob_files %{project_root}/plugins/derive/*.mlg)
@@ -23,8 +22,11 @@
    (glob_files %{project_root}/plugins/micromega/*.mlg)
    (glob_files %{project_root}/plugins/nsatz/*.mlg)
    (glob_files %{project_root}/plugins/omega/*.mlg)
-   (glob_files %{project_root}/plugins/rtauto/*.mlg)
    (glob_files %{project_root}/plugins/ring/*.mlg)
+   (glob_files %{project_root}/plugins/rtauto/*.mlg)
+   (glob_files %{project_root}/plugins/ssr/*.mlg)
+   (glob_files %{project_root}/plugins/ssrmatching/*.mlg)
+   (glob_files %{project_root}/plugins/ssrsearch/*.mlg)
    (glob_files %{project_root}/plugins/syntax/*.mlg)
    (glob_files %{project_root}/user-contrib/Ltac2/*.mlg)
    ; Sphinx files
diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar
index a787d769fb..03a20d621b 100644
--- a/doc/tools/docgram/fullGrammar
+++ b/doc/tools/docgram/fullGrammar
@@ -480,6 +480,7 @@ opt_hintbases: [
 command: [
 | "Goal" lconstr
 | "Proof"
+| "Proof" "using" G_vernac.section_subset_expr
 | "Proof" "Mode" string
 | "Proof" lconstr
 | "Abort"
@@ -604,7 +605,7 @@ command: [
 | "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 ]
+| "Proof" "using" G_vernac.section_subset_expr "with" Pltac.tactic
 | "Tactic" "Notation" OPT ltac_tactic_level LIST1 ltac_production_item ":=" tactic
 | "Print" "Ltac" reference
 | "Locate" "Ltac" reference
@@ -764,6 +765,7 @@ attribute: [
 
 attr_value: [
 | "=" string
+| "=" IDENT
 | "(" attribute_list ")"
 |
 ]
@@ -1623,6 +1625,7 @@ simple_tactic: [
 | "debug" "eauto" OPT int_or_var OPT int_or_var auto_using hintbases
 | "info_eauto" OPT int_or_var OPT int_or_var auto_using hintbases
 | "dfs" "eauto" OPT int_or_var auto_using hintbases
+| "bfs" "eauto" OPT int_or_var auto_using hintbases
 | "autounfold" hintbases clause_dft_concl
 | "autounfold_one" hintbases "in" hyp
 | "autounfold_one" hintbases
@@ -2326,7 +2329,7 @@ conversion: [
 
 occs_nums: [
 | LIST1 nat_or_var
-| "-" nat_or_var LIST0 int_or_var
+| "-" LIST1 nat_or_var
 ]
 
 occs: [
@@ -2536,6 +2539,7 @@ or_and_intropattern_loc: [
 
 as_or_and_ipat: [
 | "as" or_and_intropattern_loc
+| "as" equality_intropattern
 |
 ]
 
diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar
index 6b12d90d5d..0209cf762a 100644
--- a/doc/tools/docgram/orderedGrammar
+++ b/doc/tools/docgram/orderedGrammar
@@ -383,6 +383,7 @@ attribute: [
 
 attr_value: [
 | "=" string
+| "=" ident
 | "(" LIST0 attribute SEP "," ")"
 ]
 
@@ -434,6 +435,10 @@ univ_decl: [
 | "@{" LIST0 ident OPT "+" OPT [ "|" LIST0 univ_constraint SEP "," OPT "+" ] "}"
 ]
 
+cumul_univ_decl: [
+| "@{" LIST0 ( OPT [ "=" | "+" | "*" ] ident ) OPT "+" OPT [ "|" LIST0 univ_constraint SEP "," OPT "+" ] "}"
+]
+
 univ_constraint: [
 | universe_name [ "<" | "=" | "<=" ] universe_name
 ]
@@ -648,7 +653,7 @@ ref_or_pattern_occ: [
 
 occs_nums: [
 | LIST1 [ natural | ident ]
-| "-" [ natural | ident ] LIST0 int_or_var
+| "-" LIST1 [ natural | ident ]
 ]
 
 int_or_var: [
@@ -695,7 +700,7 @@ field_def: [
 ]
 
 inductive_definition: [
-| OPT ">" ident_decl LIST0 binder OPT [ "|" LIST0 binder ] OPT [ ":" type ] OPT ( ":=" OPT constructors_or_record ) OPT decl_notations
+| OPT ">" cumul_ident_decl LIST0 binder OPT [ "|" LIST0 binder ] OPT [ ":" type ] OPT ( ":=" OPT constructors_or_record ) OPT decl_notations
 ]
 
 constructors_or_record: [
@@ -707,6 +712,10 @@ constructor: [
 | ident LIST0 binder OPT of_type
 ]
 
+cumul_ident_decl: [
+| ident OPT cumul_univ_decl
+]
+
 filtered_import: [
 | qualid OPT [ "(" LIST1 ( qualid OPT [ "(" ".." ")" ] ) SEP "," ")" ]
 ]
@@ -728,7 +737,11 @@ sort_family: [
 ]
 
 hint_info: [
-| "|" OPT natural OPT one_term
+| "|" OPT natural OPT one_pattern
+]
+
+one_pattern: [
+| one_term
 ]
 
 module_binder: [
@@ -940,6 +953,7 @@ 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 ]
@@ -1015,12 +1029,12 @@ command: [
 | "Prenex" "Implicits" LIST1 qualid      (* SSR plugin *)
 | "Print" "Hint" "View" OPT ssrviewpos      (* SSR plugin *)
 | "Hint" "View" OPT ssrviewpos LIST1 ( one_term OPT ( "|" natural ) )      (* SSR plugin *)
-| "Search" OPT LIST1 ( "-" [ string OPT ( "%" ident ) | one_term ] ) OPT ( "in" LIST1 ( OPT "-" qualid ) )      (* SSR plugin *)
+| "Search" OPT LIST1 ( "-" [ string OPT ( "%" ident ) | one_pattern ] ) OPT ( "in" LIST1 ( OPT "-" qualid ) )      (* SSR plugin *)
 | "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 ]
+| "Proof" "using" section_var_expr "with" ltac_expr
 | "Tactic" "Notation" OPT ( "(" "at" "level" natural ")" ) LIST1 ltac_production_item ":=" ltac_expr
 | "Print" "Rewrite" "HintDb" ident
 | "Print" "Ltac" qualid
@@ -1111,9 +1125,9 @@ command: [
 | "Compute" term
 | "Check" term
 | "About" reference OPT univ_name_list
-| "SearchHead" one_term OPT ( [ "inside" | "outside" ] LIST1 qualid )
-| "SearchPattern" one_term OPT ( [ "inside" | "outside" ] LIST1 qualid )
-| "SearchRewrite" one_term OPT ( [ "inside" | "outside" ] LIST1 qualid )
+| "SearchHead" one_pattern OPT ( [ "inside" | "outside" ] LIST1 qualid )
+| "SearchPattern" one_pattern OPT ( [ "inside" | "outside" ] LIST1 qualid )
+| "SearchRewrite" one_pattern OPT ( [ "inside" | "outside" ] LIST1 qualid )
 | "Search" LIST1 ( search_query ) OPT ( [ "inside" | "outside" ] LIST1 qualid )
 | "Ltac2" OPT "mutable" OPT "rec" tac2def_body LIST0 ( "with" tac2def_body )
 | "Ltac2" "Type" OPT "rec" tac2typ_def LIST0 ( "with" tac2typ_def )
@@ -1171,7 +1185,7 @@ search_query: [
 
 search_item: [
 | OPT ( [ "head" | "hyp" | "concl" | "headhyp" | "headconcl" ] ":" ) string OPT ( "%" scope_key )
-| OPT ( [ "head" | "hyp" | "concl" | "headhyp" | "headconcl" ] ":" ) one_term
+| OPT ( [ "head" | "hyp" | "concl" | "headhyp" | "headconcl" ] ":" ) one_pattern
 | "is" ":" logical_kind
 ]
 
@@ -1200,7 +1214,7 @@ hint: [
 | "Mode" qualid LIST1 [ "+" | "!" | "-" ]
 | "Unfold" LIST1 qualid
 | "Constructors" LIST1 qualid
-| "Extern" natural OPT one_term "=>" ltac_expr
+| "Extern" natural OPT one_pattern "=>" ltac_expr
 ]
 
 tacdef_body: [
@@ -1750,6 +1764,7 @@ simple_tactic: [
 | "debug" "eauto" OPT int_or_var OPT int_or_var OPT auto_using OPT hintbases
 | "info_eauto" OPT int_or_var OPT int_or_var OPT auto_using OPT hintbases
 | "dfs" "eauto" OPT int_or_var OPT auto_using OPT hintbases
+| "bfs" "eauto" OPT int_or_var OPT auto_using OPT hintbases
 | "autounfold" OPT hintbases OPT clause_dft_concl
 | "autounfold_one" OPT hintbases OPT ( "in" ident )
 | "unify" one_term one_term OPT ( "with" ident )
@@ -1955,6 +1970,7 @@ or_and_intropattern_loc: [
 
 as_or_and_ipat: [
 | "as" or_and_intropattern_loc
+| "as" equality_intropattern
 ]
 
 eqn_ipat: [
@@ -2408,9 +2424,9 @@ tac2mode: [
 | "Compute" term
 | "Check" term
 | "About" reference OPT univ_name_list
-| "SearchHead" one_term OPT ( [ "inside" | "outside" ] LIST1 qualid )
-| "SearchPattern" one_term OPT ( [ "inside" | "outside" ] LIST1 qualid )
-| "SearchRewrite" one_term OPT ( [ "inside" | "outside" ] LIST1 qualid )
+| "SearchHead" one_pattern OPT ( [ "inside" | "outside" ] LIST1 qualid )
+| "SearchPattern" one_pattern OPT ( [ "inside" | "outside" ] LIST1 qualid )
+| "SearchRewrite" one_pattern OPT ( [ "inside" | "outside" ] LIST1 qualid )
 | "Search" LIST1 ( search_query ) OPT ( [ "inside" | "outside" ] LIST1 qualid )
 ]