so that it compiles with mathcomp 1.12

math-comp · Dec 9, 2020 · 0e6cff2 · 0e6cff2
1 parent e80caf5
commit 0e6cff2
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/theories/forms.v b/theories/forms.v
@@ -253,7 +253,7 @@ End BidirectionalLinearZ.
 
 End BilinearTheory.
 
-Canonical rev_mulmx (R : ringType) m n p := @RevOp _ _ _ (@mulmxr_head R m n p tt)
+Canonical rev_mulmx (R : ringType) m n p := @RevOp _ _ _ (@mulmxr R m n p)
   (@mulmx R m n p) (fun _ _ => erefl).
 
 Canonical mulmx_bilinear (R : comRingType) m n p := [bilinear of @mulmx R m n p].