From 691e0c20a8934343a6840f2a19735acea6e79d05 Mon Sep 17 00:00:00 2001
From: Reynald Affeldt
Date: Wed, 8 Apr 2020 00:47:30 +0900
Subject: - switching long suffixes to short suffixes   + `odd_add` -> `oddD`  
 + `odd_sub` -> `oddB`   + `take_addn` -> `takeD`   + `rot_addn` -> `rotD`   +
 `nseq_addn` -> `nseqD`

fixes #359
---
 mathcomp/ssreflect/div.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'mathcomp/ssreflect/div.v')

diff --git a/mathcomp/ssreflect/div.v b/mathcomp/ssreflect/div.v
index b366055..9047a44 100644
--- a/mathcomp/ssreflect/div.v
+++ b/mathcomp/ssreflect/div.v
@@ -329,7 +329,7 @@ Proof. by rewrite [in RHS](divn_eq m 2) modn2 muln2 addnC half_bit_double. Qed.
 
 Lemma odd_mod m d : odd d = false -> odd (m %% d) = odd m.
 Proof.
-by move=> d_even; rewrite [in RHS](divn_eq m d) odd_add odd_mul d_even andbF.
+by move=> d_even; rewrite [in RHS](divn_eq m d) oddD odd_mul d_even andbF.
 Qed.
 
 Lemma modnXm m n a : (a %% n) ^ m = a ^ m %[mod n].
-- 
cgit v1.2.3