From c889b050705f52eb802e83b6e5f15f1140d784ba Mon Sep 17 00:00:00 2001
From: Reynald Affeldt <reynald.affeldt@aist.go.jp>
Date: Wed, 24 Apr 2024 22:14:55 +0900
Subject: [PATCH] rm mulr_rev stuff

---
 CHANGELOG_UNRELEASED.md    |  9 ++++++++-
 classical/mathcomp_extra.v |  4 ++--
 theories/derive.v          | 10 ----------
 theories/forms.v           |  2 +-
 4 files changed, 11 insertions(+), 14 deletions(-)

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 9fd65798f..69d041b0d 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -39,6 +39,9 @@
 - move from `derive.v` to `mathcomp_extra.v`:
   + canonical `rev_mulr`
 
+- in `forms.v`:
+  + notation ``` u ``_ _ ````
+
 ### Renamed
 
 - in `constructive_ereal.v`:
@@ -98,8 +101,12 @@
 - in `measure.v`:
   + lemmas `prod_salgebra_set0`, `prod_salgebra_setC`, `prod_salgebra_bigcup`
     (use `measurable0`, `measurableC`, `measurable_bigcup` instead)
-- in `forms.v`:
+- in `derive.v`:
   + definition `mulr_rev`
+  + canonical `rev_mulr`
+  + lemmas `mulr_is_linear`, `mulr_rev_is_linear`
+- in `forms.v`:
+  + structure `revop`
 
 ### Infrastructure
 
diff --git a/classical/mathcomp_extra.v b/classical/mathcomp_extra.v
index 52a68652d..394267dfe 100644
--- a/classical/mathcomp_extra.v
+++ b/classical/mathcomp_extra.v
@@ -613,9 +613,9 @@ Qed.
 
 End order_min.
 
-Structure revop X Y Z (f : Y -> X -> Z) := RevOp {
+(*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 }.
 
 Canonical rev_mulr {R : ringType} :=
-  @RevOp _ _ _ (@GRing.mul R^c) (@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 d9c2e85e0..66ec8b403 100644
--- a/theories/derive.v
+++ b/theories/derive.v
@@ -826,16 +826,6 @@ Proof.
 by move=> fc; apply/diff_locallyP; rewrite diff_bilin //; apply: dbilin p fc.
 Qed.
 
-Lemma mulr_is_linear x : linear (@GRing.mul R x : R -> R).
-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 (@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 :
   bilinear_for
     (GRing.Scale.Law.clone _ _ *:%R _) (GRing.Scale.Law.clone _ _ *:%R _)
diff --git a/theories/forms.v b/theories/forms.v
index 096515c22..7a5a989ca 100644
--- a/theories/forms.v
+++ b/theories/forms.v
@@ -27,7 +27,7 @@ Reserved Notation "A ^_|_"    (at level 8, format "A ^_|_").
 Reserved Notation "A _|_ B" (at level 69, format "A  _|_  B").
 Reserved Notation "eps_theta .-sesqui" (at level 2, format "eps_theta .-sesqui").
 
-Notation "u '``_' i" := (u (GRing.zero [the zmodType of 'I_1]) i) : ring_scope.
+Notation "u '``_' i" := (u (0 : 'I_1) i) : ring_scope.
 Notation "''e_' i" := (delta_mx 0 i)
  (format "''e_' i", at level 3) : ring_scope.