From 6eb8368a8272872b4cec770dfe054f01126410ad Mon Sep 17 00:00:00 2001
From: Reynald Affeldt <reynald.affeldt@aist.go.jp>
Date: Mon, 1 Jan 2024 17:32:10 +0900
Subject: [PATCH] use R^c

---
 CHANGELOG_UNRELEASED.md    | 18 ------------------
 classical/mathcomp_extra.v |  5 ++---
 2 files changed, 2 insertions(+), 21 deletions(-)

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 22d4dbfcf..7a4665d86 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -25,24 +25,6 @@
 
 ### Changed
 
-- in `normedtype.v`:
-  + lemmas `vitali_lemma_finite` and `vitali_lemma_finite_cover` now returns
-    duplicate-free lists of indices
-
-- moved from `lebesgue_integral.v` to `measure.v`:
-  + definition `ae_eq`
-  + lemmas
-	`ae_eq0`,
-	`ae_eq_comp`,
-	`ae_eq_funeposneg`,
-	`ae_eq_refl`,
-	`ae_eq_trans`,
-	`ae_eq_sub`,
-	`ae_eq_mul2r`,
-	`ae_eq_mul2l`,
-	`ae_eq_mul1l`,
-	`ae_eq_abse`
-
 - move from `forms.v` to `mathcomp_extra.v`:
   + structure `revop`
 
diff --git a/classical/mathcomp_extra.v b/classical/mathcomp_extra.v
index 9ffaa68da..ac4b1722e 100644
--- a/classical/mathcomp_extra.v
+++ b/classical/mathcomp_extra.v
@@ -605,9 +605,8 @@ End order_min.
 
 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
-}.
+  _ : forall x, f x =1 fun_of_revop^~ x }.
 
-Definition mulr_rev {R : ringType} (y x : R) := x * y.
+Definition mulr_rev {R : ringType} := @GRing.mul R^c.
 Canonical rev_mulr {R : ringType} :=
   @RevOp _ _ _ mulr_rev (@GRing.mul R) (fun _ _ => erefl).