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/algebra/matrix.v | 2 +-
 mathcomp/algebra/mxpoly.v | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

(limited to 'mathcomp/algebra')

diff --git a/mathcomp/algebra/matrix.v b/mathcomp/algebra/matrix.v
index 0725885..ca82f38 100644
--- a/mathcomp/algebra/matrix.v
+++ b/mathcomp/algebra/matrix.v
@@ -2395,7 +2395,7 @@ rewrite (reindex (lift_perm i0 j0)); last first.
   by rewrite lift_perm_lift -si0 permE ulsfK.
 rewrite /cofactor big_distrr /=.
 apply: eq_big => [s | s _]; first by rewrite lift_perm_id eqxx.
-rewrite -signr_odd mulrA -signr_addb odd_add -odd_lift_perm; congr (_ * _).
+rewrite -signr_odd mulrA -signr_addb oddD -odd_lift_perm; congr (_ * _).
 case: (pickP 'I_n) => [k0 _ | n0]; last first.
   by rewrite !big1 // => [j /unlift_some[i] | i _]; have:= n0 i.
 rewrite (reindex (lift i0)).
diff --git a/mathcomp/algebra/mxpoly.v b/mathcomp/algebra/mxpoly.v
index b39f600..b66b96e 100644
--- a/mathcomp/algebra/mxpoly.v
+++ b/mathcomp/algebra/mxpoly.v
@@ -469,7 +469,7 @@ rewrite big_ord_recr big_ord_recl/= big1 ?add0r //=; last first.
 rewrite !mxE ?subnn -horner_coef0 /= hornerMXaddC.
 rewrite !(eqxx, mulr0, add0r, addr0, subr0, rmorphN, opprK)/=.
 rewrite mulrC /cofactor; congr (_ * 'X + _).
-  rewrite /cofactor -signr_odd odd_add addbb mul1r; congr (\det _).
+  rewrite /cofactor -signr_odd oddD addbb mul1r; congr (\det _).
   apply/matrixP => i j; rewrite !mxE -val_eqE coefD coefMX coefC.
   by rewrite /= /bump /= !add1n !eqSS addr0.
 rewrite /cofactor [X in \det X](_ : _ = D _).
-- 
cgit v1.2.3