From 8a4ae574ed75857b9762e06c11589409874ca1a4 Mon Sep 17 00:00:00 2001
From: Christian Doczkal
Date: Fri, 26 Jun 2020 12:47:52 +0200
Subject: fix "Nothing to inject" warnings

---
 mathcomp/ssreflect/fingraph.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'mathcomp')

diff --git a/mathcomp/ssreflect/fingraph.v b/mathcomp/ssreflect/fingraph.v
index d1376d0..6495ef6 100644
--- a/mathcomp/ssreflect/fingraph.v
+++ b/mathcomp/ssreflect/fingraph.v
@@ -621,8 +621,8 @@ Lemma fcard_gt1P (A : {pred T}) :
   reflect (exists2 x, x \in A & exists2 y, y \in A & ~~ fconnect f x y)
           (1 < fcard f A).
 Proof.
-move=> clAf; apply: (iffP card_gt1P) => [|[x] [xA [y yA not_xfy]]]. 
-  move=> [x] [y] [/andP [/= rfx xA]] [/andP[/= rfy yA] xDy].
+move=> clAf; apply: (iffP card_gt1P) => [|[x xA [y yA not_xfy]]].
+  move=> [x [y [/andP [/= rfx xA] /andP[/= rfy yA] xDy]]].
   by exists x; try exists y; rewrite // -root_connect // (eqP rfx) (eqP rfy).
 exists (froot f x), (froot f y); rewrite !inE !roots_root ?root_connect //=.
 by split => //; rewrite -(closed_connect clAf (connect_root _ _)).
-- 
cgit v1.2.3