so that it compiles with mathcomp 1.12

math-comp · Dec 5, 2020 · dad6faf · dad6faf
1 parent c894652
commit dad6faf
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].