diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 7a4665d866..ac08e36f9b 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -29,7 +29,6 @@
   + structure `revop`
 
 - move from `derive.v` to `mathcomp_extra.v`:
-  + definition `mulr_rev`
   + canonical `rev_mulr`
 
 ### Renamed
@@ -73,6 +72,9 @@
 - in `lebesgue_integral.v`:
   + `integrablerM`, `integrableMr` (were deprecated since version 0.6.4)
 
+- in `forms.v`:
+  + definition `mulr_rev`
+
 ### Infrastructure
 
 ### Misc
diff --git a/classical/mathcomp_extra.v b/classical/mathcomp_extra.v
index ac4b1722e4..b7cc2a26ed 100644
--- a/classical/mathcomp_extra.v
+++ b/classical/mathcomp_extra.v
@@ -607,6 +607,5 @@ Structure revop X Y Z (f : Y -> X -> Z) := RevOp {
   fun_of_revop :> X -> Y -> Z;
   _ : forall x, f x =1 fun_of_revop^~ x }.
 
-Definition mulr_rev {R : ringType} := @GRing.mul R^c.
 Canonical rev_mulr {R : ringType} :=
-  @RevOp _ _ _ mulr_rev (@GRing.mul R) (fun _ _ => erefl).
+  @RevOp _ _ _ (@GRing.mul R^c) (@GRing.mul R) (fun _ _ => erefl).
diff --git a/theories/derive.v b/theories/derive.v
index 99fb5ee376..2abd2d9c56 100644
--- a/theories/derive.v
+++ b/theories/derive.v
@@ -831,9 +831,9 @@ Proof. by move=> ? ? ?; rewrite mulrDr scalerAr. Qed.
 HB.instance Definition _ x := GRing.isLinear.Build R R R _ ( *%R x)
   (mulr_is_linear x).
 
-Lemma mulr_rev_is_linear y : linear (mulr_rev y : R -> R).
-Proof. by move=> ? ? ?; rewrite /mulr_rev mulrDr scalerAl. Qed.
-HB.instance Definition _ y := GRing.isLinear.Build R R R _ (mulr_rev y)
+Lemma mulr_rev_is_linear y : linear (@GRing.mul R^c y : R -> R).
+Proof. by move=> ? ? ?; rewrite mulrDr scalerAl. Qed.
+HB.instance Definition _ y := GRing.isLinear.Build R R R _ (@GRing.mul R^c y)
   (mulr_rev_is_linear y).
 
 Lemma mulr_is_bilinear :