use R^c

math-comp · Apr 16, 2024 · 6eb8368 · 6eb8368
1 parent adcb3da
commit 6eb8368
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 21 deletions.
diff --git 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
@@ -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).