diff --git a/doc/changelog/07-ssreflect/18374-backport-mathcomp.rst b/doc/changelog/07-ssreflect/18374-backport-mathcomp.rst
new file mode 100644
index 000000000000..4f2562d1babc
--- /dev/null
+++ b/doc/changelog/07-ssreflect/18374-backport-mathcomp.rst
@@ -0,0 +1,5 @@
+- **Deprecated:**
+  The ``fun_scope`` notation scope declared in `ssrfun.v` is deprecated. Use
+  ``function_scope`` instead
+  (`#18374 <https://github.com/coq/coq/pull/18374>`_,
+  by Kazuhiko Sakaguchi).
diff --git a/theories/ssr/ssrbool.v b/theories/ssr/ssrbool.v
index add970edb2cb..2f71223a6850 100644
--- a/theories/ssr/ssrbool.v
+++ b/theories/ssr/ssrbool.v
@@ -1309,13 +1309,14 @@ Definition predC {T} (p : pred T) := SimplPred (xpredC p).
 Definition predD {T} (p1 p2 : pred T) := SimplPred (xpredD p1 p2).
 Definition preim {aT rT} (f : aT -> rT) (d : pred rT) := SimplPred (xpreim f d).
 
-Notation "[ 'pred' : T | E ]" := (SimplPred (fun _ : T => E%B)) : fun_scope.
-Notation "[ 'pred' x | E ]" := (SimplPred (fun x => E%B)) : fun_scope.
-Notation "[ 'pred' x | E1 & E2 ]" := [pred x | E1 && E2 ] : fun_scope.
+Notation "[ 'pred' : T | E ]" := (SimplPred (fun _ : T => E%B)) :
+  function_scope.
+Notation "[ 'pred' x | E ]" := (SimplPred (fun x => E%B)) : function_scope.
+Notation "[ 'pred' x | E1 & E2 ]" := [pred x | E1 && E2 ] : function_scope.
 Notation "[ 'pred' x : T | E ]" :=
-  (SimplPred (fun x : T => E%B)) (only parsing) : fun_scope.
+  (SimplPred (fun x : T => E%B)) (only parsing) : function_scope.
 Notation "[ 'pred' x : T | E1 & E2 ]" :=
-  [pred x : T | E1 && E2 ] (only parsing) : fun_scope.
+  [pred x : T | E1 && E2 ] (only parsing) : function_scope.
 
 (** Coercions for simpl_pred.
    As simpl_pred T values are used both applicatively and collectively we
@@ -1387,9 +1388,9 @@ Definition relU {T} (r1 r2 : rel T) := SimplRel (xrelU r1 r2).
 Definition relpre {aT rT} (f : aT -> rT) (r : rel rT) := SimplRel (xrelpre f r).
 
 Notation "[ 'rel' x y | E ]" := (SimplRel (fun x y => E%B))
-  (only parsing) : fun_scope.
+  (only parsing) : function_scope.
 Notation "[ 'rel' x y : T | E ]" :=
-  (SimplRel (fun x y : T => E%B)) (only parsing) : fun_scope.
+  (SimplRel (fun x y : T => E%B)) (only parsing) : function_scope.
 
 Lemma subrelUl T (r1 r2 : rel T) : subrel r1 (relU r1 r2).
 Proof. by move=> x y r1xy; apply/orP; left. Qed.
@@ -1450,25 +1451,29 @@ Notation "x \notin A" := (~~ (x \in A)) : bool_scope.
 Notation "A =i B" := (eq_mem (mem A) (mem B)) : type_scope.
 Notation "{ 'subset' A <= B }" := (sub_mem (mem A) (mem B)) : type_scope.
 
+Notation "[ 'in' A ]" := (in_mem^~ (mem A))
+  (at level 0, format "[ 'in'  A ]") : function_scope.
+
 Notation "[ 'mem' A ]" :=
-  (pred_of_simpl (simpl_of_mem (mem A))) (only parsing) : fun_scope.
-
-Notation "[ 'predI' A & B ]" := (predI [mem A] [mem B]) : fun_scope.
-Notation "[ 'predU' A & B ]" := (predU [mem A] [mem B]) : fun_scope.
-Notation "[ 'predD' A & B ]" := (predD [mem A] [mem B]) : fun_scope.
-Notation "[ 'predC' A ]" := (predC [mem A]) : fun_scope.
-Notation "[ 'preim' f 'of' A ]" := (preim f [mem A]) : fun_scope.
-Notation "[ 'pred' x 'in' A ]" := [pred x | x \in A] : fun_scope.
-Notation "[ 'pred' x 'in' A | E ]" := [pred x | x \in A & E] : fun_scope.
+  (pred_of_simpl (simpl_of_mem (mem A))) (only parsing) : function_scope.
+
+Notation "[ 'predI' A & B ]" := (predI [in A] [in B]) : function_scope.
+Notation "[ 'predU' A & B ]" := (predU [in A] [in B]) : function_scope.
+Notation "[ 'predD' A & B ]" := (predD [in A] [in B]) : function_scope.
+Notation "[ 'predC' A ]" := (predC [in A]) : function_scope.
+Notation "[ 'preim' f 'of' A ]" := (preim f [in A]) : function_scope.
+
+Notation "[ 'pred' x 'in' A ]" := [pred x | x \in A] : function_scope.
+Notation "[ 'pred' x 'in' A | E ]" := [pred x | x \in A & E] : function_scope.
 Notation "[ 'pred' x 'in' A | E1 & E2 ]" :=
-  [pred x | x \in A & E1 && E2 ] : fun_scope.
+  [pred x | x \in A & E1 && E2 ] : function_scope.
 
 Notation "[ 'rel' x y 'in' A & B | E ]" :=
-  [rel x y | (x \in A) && (y \in B) && E] : fun_scope.
+  [rel x y | (x \in A) && (y \in B) && E] : function_scope.
 Notation "[ 'rel' x y 'in' A & B ]" :=
-  [rel x y | (x \in A) && (y \in B)] : fun_scope.
-Notation "[ 'rel' x y 'in' A | E ]" := [rel x y in A & A | E] : fun_scope.
-Notation "[ 'rel' x y 'in' A ]" := [rel x y in A & A] : fun_scope.
+  [rel x y | (x \in A) && (y \in B)] : function_scope.
+Notation "[ 'rel' x y 'in' A | E ]" := [rel x y in A & A | E] : function_scope.
+Notation "[ 'rel' x y 'in' A ]" := [rel x y in A & A] : function_scope.
 
 (** Aliases of pred T that let us tag instances of simpl_pred as applicative
   or collective, via bespoke coercions. This tagging will give control over
diff --git a/theories/ssr/ssreflect.v b/theories/ssr/ssreflect.v
index 5e0563e992aa..a0a31fa22115 100644
--- a/theories/ssr/ssreflect.v
+++ b/theories/ssr/ssreflect.v
@@ -59,13 +59,20 @@ Declare ML Module "ssreflect_plugin:coq-core.plugins.ssreflect".
      This minimizes the comparison overhead for foo, while still allowing
      rewrite unlock to expose big_foo_expression.
 
+         #[#elaborate x#]# == triggers Coq elaboration to fill the holes of the term x
+                          The main use case is to trigger typeclass inference in
+                          the body of a ssreflect have := #[#elaborate body#]#.
+
   Additionally we provide default intro pattern ltac views:
   - top of the stack actions:
-    => /[apply]     := => hyp {}/hyp
-    => /[swap]      := => x y; move: y x
+    => /#[#apply#]#     := => hyp {}/hyp
+    => /#[#swap#]#      := => x y; move: y x
                       (also swap and preserves let bindings)
-    => /[dup]       := => x; have copy := x; move: copy x
+    => /#[#dup#]#       := => x; have copy := x; move: copy x
                       (also copies and preserves let bindings)
+  - calling rewrite from an intro pattern, use with parsimony:
+    => /#[#1! rules#]#  := rewrite rules
+    => /#[#! rules#]#   := rewrite !rules
 
  More information about these definitions and their use can be found in the
  ssreflect manual, and in specific comments below.                           **)
@@ -124,6 +131,8 @@ Reserved Notation "[ 'unlockable' 'of' C ]" (at level 0,
 Reserved Notation "[ 'unlockable' 'fun' C ]" (at level 0,
   format "[ 'unlockable'  'fun'  C ]").
 
+Reserved Notation "[ 'elaborate' x ]" (at level 0).
+
 (**
  To define notations for tactic in intro patterns.
  When "=> /t" is parsed, "t:%ssripat" is actually interpreted. **)
@@ -433,6 +442,9 @@ Canonical locked_with_unlockable T k x :=
 Lemma unlock_with T k x : unlocked (locked_with_unlockable k x) = x :> T.
 Proof. exact: unlock. Qed.
 
+(**  Notation to trigger Coq elaboration to fill the holes **)
+Notation "[ 'elaborate' x ]" := (ltac:(refine x)) (only parsing).
+
 (**  Internal N-ary congruence lemmas for the congr tactic.  **)
 
 Fixpoint nary_congruence_statement (n : nat)
@@ -653,4 +665,21 @@ Notation "'[' 'dup' ']'" := (ltac:(move;
   end))
   (at level 0, only parsing) : ssripat_scope.
 
+Notation "'[' '1' '!' rules ']'"     := (ltac:(rewrite rules))
+  (at level 0, rules at level 200, only parsing) : ssripat_scope.
+Notation "'[' '!' rules ']'"         := (ltac:(rewrite !rules))
+  (at level 0, rules at level 200, only parsing) : ssripat_scope.
+
 End ipat.
+
+(* A class to trigger reduction by rewriting.                           *)
+(* Usage: rewrite [pattern]vm_compute.                                  *)
+(* Alternatively one may redefine a lemma as in algebra/rat.v :         *)
+(* Lemma rat_vm_compute n (x : rat) : vm_compute_eq n%:Q x -> n%:Q = x. *)
+(* Proof. exact. Qed.                                                   *)
+
+Class vm_compute_eq {T : Type} (x y : T) := vm_compute : x = y.
+
+#[global]
+Hint Extern 0 (@vm_compute_eq _ _ _) =>
+       vm_compute; reflexivity : typeclass_instances.
diff --git a/theories/ssr/ssrfun.v b/theories/ssr/ssrfun.v
index e6de19798f48..6c8261741aa3 100644
--- a/theories/ssr/ssrfun.v
+++ b/theories/ssr/ssrfun.v
@@ -387,13 +387,17 @@ Canonical wrap T x := @Wrap T x.
 
 Prenex Implicits unwrap wrap Wrap.
 
+(**
+ fun_scope below is deprecated and should eventually be
+ removed. Use function_scope instead.                    **)
 Declare Scope fun_scope.
 Delimit Scope fun_scope with FUN.
 Open Scope fun_scope.
+Open Scope function_scope.
 
 (**  Notations for argument transpose  **)
-Notation "f ^~ y" := (fun x => f x y) : fun_scope.
-Notation "@^~ x" := (fun f => f x) : fun_scope.
+Notation "f ^~ y" := (fun x => f x y) : function_scope.
+Notation "@^~ x" := (fun f => f x) : function_scope.
 
 (**
  Definitions and notation for explicit functions with simplification,
@@ -412,19 +416,19 @@ End SimplFun.
 
 Coercion fun_of_simpl : simpl_fun >-> Funclass.
 
-Notation "[ 'fun' : T => E ]" := (SimplFun (fun _ : T => E)) : fun_scope.
-Notation "[ 'fun' x => E ]" := (SimplFun (fun x => E)) : fun_scope.
-Notation "[ 'fun' x y => E ]" := (fun x => [fun y => E]) : fun_scope.
+Notation "[ 'fun' : T => E ]" := (SimplFun (fun _ : T => E)) : function_scope.
+Notation "[ 'fun' x => E ]" := (SimplFun (fun x => E)) : function_scope.
+Notation "[ 'fun' x y => E ]" := (fun x => [fun y => E]) : function_scope.
 Notation "[ 'fun' x : T => E ]" := (SimplFun (fun x : T => E))
-  (only parsing) : fun_scope.
+  (only parsing) : function_scope.
 Notation "[ 'fun' x y : T => E ]" := (fun x : T => [fun y : T => E])
-  (only parsing) : fun_scope.
+  (only parsing) : function_scope.
 Notation "[ 'fun' ( x : T ) y => E ]" := (fun x : T => [fun y => E])
-  (only parsing) : fun_scope.
+  (only parsing) : function_scope.
 Notation "[ 'fun' x ( y : T ) => E ]" := (fun x => [fun y : T => E])
-  (only parsing) : fun_scope.
+  (only parsing) : function_scope.
 Notation "[ 'fun' ( x : T ) ( y : U ) => E ]" := (fun x : T => [fun y : U => E])
-  (only parsing) : fun_scope.
+  (only parsing) : function_scope.
 
 (**  For delta functions in eqtype.v.  **)
 Definition SimplFunDelta aT rT (f : aT -> aT -> rT) := [fun z => f z z].
@@ -456,10 +460,10 @@ Global Typeclasses Opaque eqfun eqrel.
 #[global]
 Hint Resolve frefl rrefl : core.
 
-Notation "f1 =1 f2" := (eqfun f1 f2) : fun_scope.
-Notation "f1 =1 f2 :> A" := (f1 =1 (f2 : A)) : fun_scope.
-Notation "f1 =2 f2" := (eqrel f1 f2) : fun_scope.
-Notation "f1 =2 f2 :> A" := (f1 =2 (f2 : A)) : fun_scope.
+Notation "f1 =1 f2" := (eqfun f1 f2) : type_scope.
+Notation "f1 =1 f2 :> A" := (f1 =1 (f2 : A)) : type_scope.
+Notation "f1 =2 f2" := (eqrel f1 f2) : type_scope.
+Notation "f1 =2 f2 :> A" := (f1 =2 (f2 : A)) : type_scope.
 
 Section Composition.
 
@@ -476,19 +480,20 @@ End Composition.
 
 Arguments comp {A B C} f g x /.
 Arguments catcomp {A B C} g f x /.
-Notation "f1 \o f2" := (comp f1 f2) : fun_scope.
-Notation "f1 \; f2" := (catcomp f1 f2) : fun_scope.
+Notation "f1 \o f2" := (comp f1 f2) : function_scope.
+Notation "f1 \; f2" := (catcomp f1 f2) : function_scope.
 
 Lemma compA {A B C D : Type} (f : B -> A) (g : C -> B) (h : D -> C) :
   f \o (g \o h) = (f \o g) \o h.
 Proof. by []. Qed.
 
-Notation "[ 'eta' f ]" := (fun x => f x) : fun_scope.
+Notation "[ 'eta' f ]" := (fun x => f x) : function_scope.
 
-Notation "'fun' => E" := (fun _ => E) : fun_scope.
+Notation "'fun' => E" := (fun _ => E) : function_scope.
 
 Notation id := (fun x => x).
-Notation "@ 'id' T" := (fun x : T => x) (only parsing) : fun_scope.
+
+Notation "@ 'id' T" := (fun x : T => x) (only parsing) : function_scope.
 
 Definition idfun T x : T := x.
 Arguments idfun {T} x /.
@@ -568,8 +573,8 @@ Proof. by case/all_tag=> f /all_pair[]; exists f. Qed.
 (**  Refinement types.  **)
 
 (**  Prenex Implicits and renaming.  **)
-Notation "@ 'sval'" := (@proj1_sig) (at level 10, format "@ 'sval'").
 Notation sval := (@proj1_sig _ _).
+Notation "@ 'sval'" := (@proj1_sig) (only parsing) : function_scope.
 
 Section Sig.