fix

coq-community · Aug 2, 2024 · 7f79944 · 7f79944
1 parent 3e64a32
commit 7f79944
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/refinements/binord.v b/refinements/binord.v
@@ -118,7 +118,7 @@ Local Arguments mul_ord /.
 
 #[export] Instance Rord_mul n1 n2 (rn : nat_R n1 n2) :
   refines (Rord (nat_R_S_R rn) ==> Rord (nat_R_S_R rn) ==> Rord (nat_R_S_R rn))
-  (@Zp_mul n1.+1) *%C.
+  (@Zp_mul _) *%C.
 Proof.
   rewrite refinesE=> x x' hx y y' hy /=.
   exact: refinesP.