fix

math-comp · Apr 24, 2024 · cee5635 · cee5635
1 parent ce49faf
commit cee5635
Show file tree

Hide file tree

Showing 3 changed files with 4 additions and 10 deletions.
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
@@ -36,9 +36,6 @@
 - in `forms.v`:
   + notation ``` u ``_ _ ```
 
-- moved from `forms.v` to `matchomp_extra.v`:
-  + structure `revop`
-
 ### Renamed
 
 - in `constructive_ereal.v`:
@@ -103,6 +100,10 @@
   + canonical `rev_mulr`
   + lemmas `mulr_is_linear`, `mulr_rev_is_linear`
 
+- in `forms.v`
+  + canonical `rev_mulmx`
+  + structure `revop`
+
 ### Infrastructure
 
 ### Misc
diff --git a/classical/mathcomp_extra.v b/classical/mathcomp_extra.v
@@ -612,7 +612,3 @@ rewrite /Order.min/=; case: ifPn => xz; case: ifPn => yz; rewrite ?ltxx//.
 Qed.
 
 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 }.
diff --git a/theories/forms.v b/theories/forms.v
@@ -188,9 +188,6 @@ End BidirectionalLinearZ.
 
 End BilinearTheory.
 
-Canonical rev_mulmx (R : ringType) m n p := @RevOp _ _ _ (@mulmxr R m n p)
-  (@mulmx R m n p) (fun _ _ => erefl).
-
 Lemma mulmx_is_bilinear (R : comRingType) m n p :
   bilinear_for
     (GRing.Scale.Law.clone _ _ *:%R _) (GRing.Scale.Law.clone _ _ *:%R _)