diff options
| author | Cyril Cohen | 2020-08-11 03:57:16 +0200 |
|---|---|---|
| committer | GitHub | 2020-08-11 03:57:16 +0200 |
| commit | 60bd08e5b3575a34d8e969c2e4ade40926630143 (patch) | |
| tree | c9940ac14c9424f2adeb32a868ed833d0fe547da /mathcomp | |
| parent | d7c08d664a58f8ee99ae9a0de805c8af89889ba5 (diff) | |
| parent | 8a4ae574ed75857b9762e06c11589409874ca1a4 (diff) | |
Merge pull request #542 from chdoc/nothing-to-inject
fix "Nothing to inject" warnings
Diffstat (limited to 'mathcomp')
| -rw-r--r-- | mathcomp/ssreflect/fingraph.v | 4 |
1 files changed, 2 insertions, 2 deletions
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 _ _)). |