4 files changed, 38 insertions, 15 deletions
diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg
index 4ad32e15eb..4c1956d172 100644
--- a/doc/tools/docgram/common.edit_mlg
+++ b/doc/tools/docgram/common.edit_mlg
@@ -285,9 +285,12 @@ term_let: [
 (* Don't need to document that "( )" is equivalent to "()" *)
 | REPLACE "let" [ "(" LIST0 name SEP "," ")" | "()" ] as_return_type ":=" term200 "in" term200
 | WITH "let" "(" LIST0 name SEP "," ")" as_return_type ":=" term200 "in" term200
+| MOVETO destructuring_let "let" "(" LIST0 name SEP "," ")" as_return_type ":=" term200 "in" term200
 | REPLACE "let" "'" pattern200 ":=" term200 "in" term200
-| WITH  "let" "'" pattern200 ":=" term200 OPT case_type "in" term200
+| WITH "let" "'" pattern200 ":=" term200 OPT case_type "in" term200
 | DELETE "let" "'" pattern200 ":=" term200 case_type "in" term200
+| MOVETO destructuring_let "let" "'" pattern200 ":=" term200 OPT case_type "in" term200
+| MOVETO destructuring_let "let" "'" pattern200 "in" pattern200 ":=" term200 case_type "in" term200
 ]
 
 atomic_constr: [
@@ -2478,7 +2481,6 @@ SPLICE: [
 | binders
 | casted_constr
 | check_module_types
-| constr_pattern
 | decl_sep
 | function_fix_definition (* loses funind annotation *)
 | glob
@@ -2652,6 +2654,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..033ece04de 100644
--- a/doc/tools/docgram/fullGrammar
+++ b/doc/tools/docgram/fullGrammar
@@ -1623,6 +1623,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
diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar
index c697043f27..dfd3a18908 100644
--- a/doc/tools/docgram/orderedGrammar
+++ b/doc/tools/docgram/orderedGrammar
@@ -434,6 +434,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
 ]
@@ -473,6 +477,10 @@ ssr_dpat: [
 term_let: [
 | "let" name OPT ( ":" type ) ":=" term "in" term
 | "let" name LIST1 binder OPT ( ":" type ) ":=" term "in" term
+| destructuring_let
+]
+
+destructuring_let: [
 | "let" "(" LIST0 name SEP "," ")" OPT [ OPT [ "as" name ] "return" term100 ] ":=" term "in" term
 | "let" "'" pattern ":=" term OPT ( "return" term100 ) "in" term
 | "let" "'" pattern "in" pattern ":=" term "return" term100 "in" term
@@ -691,7 +699,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: [
@@ -703,6 +711,10 @@ constructor: [
 | ident LIST0 binder OPT of_type
 ]
 
+cumul_ident_decl: [
+| ident OPT cumul_univ_decl
+]
+
 filtered_import: [
 | qualid OPT [ "(" LIST1 ( qualid OPT [ "(" ".." ")" ] ) SEP "," ")" ]
 ]
@@ -724,7 +736,11 @@ sort_family: [
 ]
 
 hint_info: [
-| "|" OPT natural OPT one_term
+| "|" OPT natural OPT one_pattern
+]
+
+one_pattern: [
+| one_term
 ]
 
 module_binder: [
@@ -1011,7 +1027,7 @@ 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
@@ -1107,9 +1123,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 )
@@ -1167,7 +1183,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
 ]
 
@@ -1196,7 +1212,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: [
@@ -1746,6 +1762,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 )
@@ -2404,9 +2421,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 )
 ]