From fb4948fabff8143e1a47e3943cd1fecb75867689 Mon Sep 17 00:00:00 2001
From: Cyril Cohen
Date: Wed, 24 Oct 2018 16:57:13 +0200
Subject: fix TFAE

---
 mathcomp/ssreflect/seq.v | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

(limited to 'mathcomp')

diff --git a/mathcomp/ssreflect/seq.v b/mathcomp/ssreflect/seq.v
index ba1f969..e625807 100644
--- a/mathcomp/ssreflect/seq.v
+++ b/mathcomp/ssreflect/seq.v
@@ -2800,11 +2800,6 @@ Definition all_iff (P0 : Prop) (Ps : seq Prop) : Prop :=
       if Qs is Q :: Qs then all_iff_and (P -> Q) (aux Q Qs)
       else P -> P0 : Prop) P0 Ps.
 
-(* This means "the following are all equivalent: P0, ... Pn" *)
-Notation "[ '<->' P0 ; P1 ; .. ; Pn ]" := (all_iff P0 (P1 :: .. [:: Pn] ..))
-  (at level 0, format "[ '<->' '['  P0 ;  '/' P1 ;  '/'  .. ;  '/'  Pn ']' ]")
-  : form_scope.
-
 Lemma all_iffLR P0 Ps : all_iff P0 Ps ->
    forall m n, nth P0 (P0 :: Ps) m -> nth P0 (P0 :: Ps) n.
 Proof.
@@ -2838,6 +2833,11 @@ Arguments all_iffLR {P0 Ps}.
 Arguments all_iffP {P0 Ps}.
 Coercion all_iffP : all_iff >-> Funclass.
 
+(* This means "the following are all equivalent: P0, ... Pn" *)
+Notation "[ '<->' P0 ; P1 ; .. ; Pn ]" := (all_iff P0 (P1 :: .. [:: Pn] ..))
+  (at level 0, format "[ '<->' '['  P0 ;  '/' P1 ;  '/'  .. ;  '/'  Pn ']' ]")
+  : form_scope.
+
 Section All2.
 Context {T U : Type} (p : T -> U -> bool).
 
-- 
cgit v1.2.3