From c2a42557d0cc7c4c776a4572dcfeef011bfc73b8 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Mon, 6 Nov 2017 17:15:35 +0100
Subject: Fix the only remaining spurious injection in the entire codebase.

We may want to make it an error, now that the transition period has been
long enough.
---
 mathcomp/odd_order/PFsection14.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'mathcomp')

diff --git a/mathcomp/odd_order/PFsection14.v b/mathcomp/odd_order/PFsection14.v
index c634ec1..bed35bc 100644
--- a/mathcomp/odd_order/PFsection14.v
+++ b/mathcomp/odd_order/PFsection14.v
@@ -349,7 +349,7 @@ have o1M: orthonormal (map tau1M calM).
 have Lgt1: (1 < size calL)%N by apply: seqInd_nontrivial (mFT_odd _ ) _ Lphi.
 have [[_ _]] := Dade_Ind1_sub_lin cohL Lgt1 irr_phi Lphi phi1.
 rewrite -/tauL -/betaL -/calL => ZbetaL [Gamma [_ _ [b _ Dbeta]]]. 
-rewrite odd_Frobenius_index_ler ?mFT_odd // -/u => -[]// [_ ub_Ga] _ nz_a.
+rewrite odd_Frobenius_index_ler ?mFT_odd // -/u => -[]// _ ub_Ga _ nz_a.
 have Za: a \in Cint by rewrite Cint_cfdot_vchar // ?Ztau1 ?mem_zchar.
 have [X M_X [Del [defGa oXD oDM]]] := orthogonal_split (map tau1M calM) Gamma.
 apply: ler_trans ub_Ga; rewrite defGa cfnormDd // ler_paddr ?cfnorm_ge0 //.
-- 
cgit v1.2.3