From c4e6aa42306a4eed85fc09f3164a911e75e177f0 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Mon, 22 Feb 2016 17:30:32 +0100
Subject: PF5: more predictable rewrite line (needed by rewrite using 8.5
 refiner)

---
 mathcomp/odd_order/PFsection5.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'mathcomp')

diff --git a/mathcomp/odd_order/PFsection5.v b/mathcomp/odd_order/PFsection5.v
index b1a5a32..d318f5f 100644
--- a/mathcomp/odd_order/PFsection5.v
+++ b/mathcomp/odd_order/PFsection5.v
@@ -1286,7 +1286,7 @@ have haveX xi: xi \in S2 chi1 -> exists2 X, Xspec X & Xi_spec X xi.
   - apply: sub_iso_to IZtau; last exact: zcharW.
     by apply: zchar_trans_on; apply/allP; rewrite /= !Zd.
   have [||minX1 _]:= subcoherent_norm _ _ (erefl _) defX1Y2.
-  - rewrite char_vchar ?N_S /orthogonal //= !oSS ?eqxx ?inv_eq //.
+  - rewrite char_vchar ?N_S /orthogonal //= !oSS ?eqxx // inv_eq //.
     exact: cfConjCK.
   - apply: sub_iso_to IZtau; last exact: zcharW.
     by apply: zchar_trans_on; apply/allP; rewrite /= !Zd.
-- 
cgit v1.2.3