diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 3025d70f92..2691cf1150 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -80,6 +80,9 @@
 - in `ereal.v`:
   + `ereal_sup_le` -> `ereal_sup_ge`
 
+- in `pseudometric_normed_Zmodule.v`:
+  + `opp_continuous` -> `oppr_continuous`
+
 ### Generalized
 
 - in `normedtype.v`:
diff --git a/theories/measurable_realfun.v b/theories/measurable_realfun.v
index ad7f02c589..b6b5fb6d01 100644
--- a/theories/measurable_realfun.v
+++ b/theories/measurable_realfun.v
@@ -895,7 +895,7 @@ Implicit Types D : set R.
 Lemma oppr_measurable D : measurable_fun D -%R.
 Proof.
 apply: measurable_funTS => /=; apply: continuous_measurable_fun.
-exact: opp_continuous.
+exact: oppr_continuous.
 Qed.
 
 Lemma normr_measurable D : measurable_fun D (@normr _ R).
diff --git a/theories/normedtype_theory/pseudometric_normed_Zmodule.v b/theories/normedtype_theory/pseudometric_normed_Zmodule.v
index b42cfb8d96..2c93a3da7e 100644
--- a/theories/normedtype_theory/pseudometric_normed_Zmodule.v
+++ b/theories/normedtype_theory/pseudometric_normed_Zmodule.v
@@ -516,7 +516,7 @@ continuous on pseudoMetricNormedZmodType *)
 Section continuity_pseudoMetricNormedZmodType.
 Context {K : numFieldType} {V : pseudoMetricNormedZmodType K}.
 
-Lemma opp_continuous : continuous (@GRing.opp V).
+Lemma oppr_continuous : continuous (@GRing.opp V).
 Proof.
 move=> x; apply/cvgrPdist_lt=> e e0; near do rewrite -opprD normrN.
 exact: cvgr_dist_lt.
@@ -542,6 +542,8 @@ by exists e => //= y; exact/le_lt_trans/ler_dist_dist.
 Qed.
 
 End continuity_pseudoMetricNormedZmodType.
+#[deprecated(since="mathcomp-analysis 1.11.0", note="renamed to `oppr_continuous`")]
+Notation opp_continuous := oppr_continuous (only parsing).
 
 (* TODO: generalize to R : numFieldType *)
 Section hausdorff.
@@ -1115,7 +1117,7 @@ Context (F : set_system T) {FF : Filter F}.
 Implicit Types (f g : T -> V) (s : T -> K) (k : K) (x : T) (a b : V).
 
 Lemma cvgN f a : f @ F --> a -> - f @ F --> - a.
-Proof. by move=> ?; apply: continuous_cvg => //; exact: opp_continuous. Qed.
+Proof. by move=> ?; apply: continuous_cvg => //; exact: oppr_continuous. Qed.
 
 Lemma cvgNP f a : - f @ F --> - a <-> f @ F --> a.
 Proof. by split=> /cvgN//; rewrite !opprK. Qed.
diff --git a/theories/realfun.v b/theories/realfun.v
index 23ca76c590..78a09f82e0 100644
--- a/theories/realfun.v
+++ b/theories/realfun.v
@@ -1377,7 +1377,7 @@ apply: (@segment_can_le (- b) (- a) (f \o -%R) (- g));
     rewrite /= ?lerN2 ?opprK //.
   pose fun_neg : subspace `[-b,-a] -> subspace `[a,b] := itvN_oppr a b.
   move=> z; apply: (@continuous_comp _ _ _ [fun of fun_neg]); last exact: fC.
-  exact/subspaceT_continuous/continuous_subspaceT/opp_continuous.
+  exact/subspaceT_continuous/continuous_subspaceT/oppr_continuous.
 by move=> z zab; rewrite -[- g]/(@GRing.opp _ \o g)/= fK ?opprK// oppr_itvcc.
 Qed.
 
diff --git a/theories/topology_theory/separation_axioms.v b/theories/topology_theory/separation_axioms.v
index bbacd47f90..eb5338396d 100644
--- a/theories/topology_theory/separation_axioms.v
+++ b/theories/topology_theory/separation_axioms.v
@@ -51,7 +51,6 @@ From mathcomp Require Import connected supremum_topology sigT_topology.
 (*                            includes `iter n split_ent E`.                  *)
 (*                            Critically, `gauge E` forms a uniform space     *)
 (*                            with a countable uniformity.                    *)
-(*          perfect_set A  := closed A /\ limit_point A = A                   *)
 (* ```                                                                        *)
 (******************************************************************************)