Generalise use of `{pred T}` from coq/coq#9995

Use `{pred T}` systematically for generic _collective_ boolean
predicate.
Use `PredType` to construct `predType` instances.
Instrument core `ssreflect` files to replicate these and other new
features introduces by coq/coq#9555 (`nonPropType` interface,
`simpl_rel` that simplifies with `inE`).

11 files changed, 192 insertions, 120 deletions

diff --git a/mathcomp/ssreflect/finfun.v b/mathcomp/ssreflect/finfun.v
index 127bd48..075ebfa 100644
--- a/mathcomp/ssreflect/finfun.v
+++ b/mathcomp/ssreflect/finfun.v
@@ -348,7 +348,7 @@ Section EqTheory.
 
 Variables (aT : finType) (rT : eqType).
 Notation fT := {ffun aT -> rT}.
-Implicit Types (y : rT) (D : pred aT) (R : pred rT) (f : fT).
+Implicit Types (y : rT) (D : {pred aT}) (R : {pred rT}) (f : fT).
 
 Lemma supportP y D g :
   reflect (forall x, x \notin D -> g x = y) (y.-support g \subset D).
@@ -440,7 +440,7 @@ Section FinFunTheory.
 
 Variables aT rT : finType.
 Notation fT := {ffun aT -> rT}.
-Implicit Types (D : pred aT) (R : pred rT) (F : aT -> pred rT).
+Implicit Types (D : {pred aT}) (R : {pred rT}) (F : aT -> pred rT).
 
 Lemma card_pfamily y0 D F :
   #|pfamily y0 D F| = foldr muln 1 [seq #|F x| | x in D].
diff --git a/mathcomp/ssreflect/fingraph.v b/mathcomp/ssreflect/fingraph.v
index 42346e2..70536dc 100644
--- a/mathcomp/ssreflect/fingraph.v
+++ b/mathcomp/ssreflect/fingraph.v
@@ -238,7 +238,7 @@ Notation fclosure f a := (closure (coerced_frel f) a).
 Section EqConnect.
 
 Variable T : finType.
-Implicit Types (e : rel T) (a : pred T).
+Implicit Types (e : rel T) (a : {pred T}).
 
 Lemma connect_sub e e' :
   subrel e (connect e') -> subrel (connect e) (connect e').
@@ -289,7 +289,7 @@ Section Closure.
 
 Variables (T : finType) (e : rel T).
 Hypothesis sym_e : connect_sym e.
-Implicit Type a : pred T.
+Implicit Type a : {pred T}.
 
 Lemma same_connect_rev : connect e =2 connect (fun x y => e y x).
 Proof.
@@ -465,7 +465,7 @@ End Loop.
 
 Section orbit_in.
 
-Variable S : pred_sort (predPredType T).
+Variable S : {pred T}.
 
 Hypothesis f_in : {in S, forall x, f x \in S}.
 Hypothesis injf : {in S &, injective f}.
@@ -579,7 +579,7 @@ Proof. exact: eq_n_comp same_fconnect_finv. Qed.
 
 Definition order_set n : pred T := [pred x | order x == n].
 
-Lemma fcard_order_set n (a : pred T) :
+Lemma fcard_order_set n (a : {pred T}) :
   a \subset order_set n -> fclosed f a -> fcard f a * n = #|a|.
 Proof.
 move=> a_n cl_a; rewrite /n_comp_mem; set b := [predI froots f & a].
@@ -598,7 +598,8 @@ rewrite -(cardID (fconnect f x)); congr (_ + _); apply: eq_card => y.
 by congr (~~ _ && _); rewrite /= /in_mem /= symf -(root_connect symf) r_x.
 Qed.
 
-Lemma fclosed1 (a : pred T) : fclosed f a -> forall x, (x \in a) = (f x \in a).
+Lemma fclosed1 (a : {pred T}) :
+  fclosed f a -> forall x, (x \in a) = (f x \in a).
 Proof. by move=> cl_a x; apply: cl_a (eqxx _). Qed.
 
 Lemma same_fconnect1 x : fconnect f x =1 fconnect f (f x).
@@ -630,7 +631,7 @@ Proof. by rewrite /roots -fconnect_id connect_root. Qed.
 Lemma froot_id (x : T) : froot id x = x.
 Proof. by apply/eqP; apply: froots_id. Qed.
 
-Lemma fcard_id (a : pred T) : fcard id a = #|a|.
+Lemma fcard_id (a : {pred T}) : fcard id a = #|a|.
 Proof. by apply: eq_card => x; rewrite inE froots_id. Qed.
 
 End FconnectId.
@@ -694,7 +695,7 @@ Record rel_adjunction_mem m_a := RelAdjunction {
     in_mem (h x') m_a -> connect e' x' y' = connect e (h x') (h y')
 }.
 
-Variable a : pred T.
+Variable a : {pred T}.
 Hypothesis cl_a : closed e a.
 
 Local Notation rel_adjunction := (rel_adjunction_mem (mem a)).
diff --git a/mathcomp/ssreflect/finset.v b/mathcomp/ssreflect/finset.v
index 98abdf2..204843a 100644
--- a/mathcomp/ssreflect/finset.v
+++ b/mathcomp/ssreflect/finset.v
@@ -203,8 +203,7 @@ Coercion pred_of_set: set_type >-> fin_pred_sort.
 
 (* Declare pred_of_set as a canonical instance of topred, but use the         *)
 (* coercion to resolve mem A to @mem (predPredType T) (pred_of_set A).        *)
-Canonical set_predType T :=
-  Eval hnf in @mkPredType _ (unkeyed (set_type T)) (@pred_of_set T).
+Canonical set_predType T := @PredType _ (unkeyed (set_type T)) (@pred_of_set T).
 
 Section BasicSetTheory.
 
@@ -1085,7 +1084,7 @@ Notation "[ 'set' E | x : T 'in' A , y : U 'in' B & P ]" :=
   (at level 0, E, x, y at level 99, only parsing) : set_scope.
 
 (* Comprehensions over a type. *)
-Local Notation predOfType T := (sort_of_simpl_pred (@pred_of_argType T)).
+Local Notation predOfType T := (pred_of_simpl (@pred_of_argType T)).
 Notation "[ 'set' E | x : T ]" := [set E | x : T in predOfType T]
   (at level 0, E, x at level 99,
    format "[ '[hv' 'set'  E '/ '  |  x  :  T ] ']'") : set_scope.
@@ -1205,7 +1204,7 @@ apply: (iffP imageP) => [[[x1 x2] Dx12] | [x1 x2 Dx1 Dx2]] -> {y}.
 by exists (x1, x2); rewrite //= !inE Dx1.
 Qed.
 
-Lemma mem_imset (D : pred aT) x : x \in D -> f x \in f @: D.
+Lemma mem_imset (D : {pred aT}) x : x \in D -> f x \in f @: D.
 Proof. by move=> Dx; apply/imsetP; exists x. Qed.
 
 Lemma imset0 : f @: set0 = set0.
@@ -1223,12 +1222,12 @@ apply/setP => y.
 by apply/imsetP/set1P=> [[x' /set1P-> //]| ->]; exists x; rewrite ?set11.
 Qed.
 
-Lemma mem_imset2 (D : pred aT) (D2 : aT -> pred aT2) x x2 :
+Lemma mem_imset2 (D : {pred aT}) (D2 : aT -> {pred aT2}) x x2 :
     x \in D -> x2 \in D2 x ->
   f2 x x2 \in imset2 f2 (mem D) (fun x1 => mem (D2 x1)).
 Proof. by move=> Dx Dx2; apply/imset2P; exists x x2. Qed.
 
-Lemma sub_imset_pre (A : pred aT) (B : pred rT) :
+Lemma sub_imset_pre (A : {pred aT}) (B : {pred rT}) :
   (f @: A \subset B) = (A \subset f @^-1: B).
 Proof.
 apply/subsetP/subsetP=> [sfAB x Ax | sAf'B fx].
@@ -1236,7 +1235,7 @@ apply/subsetP/subsetP=> [sfAB x Ax | sAf'B fx].
 by case/imsetP=> x Ax ->; move/sAf'B: Ax; rewrite inE.
 Qed.
 
-Lemma preimsetS (A B : pred rT) :
+Lemma preimsetS (A B : {pred rT}) :
   A \subset B -> (f @^-1: A) \subset (f @^-1: B).
 Proof. by move=> sAB; apply/subsetP=> y; rewrite !inE; apply: subsetP. Qed.
 
@@ -1261,7 +1260,7 @@ Proof. by apply/setP=> y; rewrite !inE. Qed.
 Lemma preimsetC (A : {set rT}) : f @^-1: (~: A) = ~: f @^-1: A.
 Proof. by apply/setP=> y; rewrite !inE. Qed.
 
-Lemma imsetS (A B : pred aT) : A \subset B -> f @: A \subset f @: B.
+Lemma imsetS (A B : {pred aT}) : A \subset B -> f @: A \subset f @: B.
 Proof.
 move=> sAB; apply/subsetP=> _ /imsetP[x Ax ->].
 by apply/imsetP; exists x; rewrite ?(subsetP sAB).
@@ -1303,27 +1302,27 @@ apply/subsetP=> _ /setIP[/imsetP[x Ax ->] /imsetP[z Bz /injf eqxz]].
 by rewrite mem_imset // inE Ax eqxz.
 Qed.
 
-Lemma imset2Sl (A B : pred aT) (C : pred aT2) :
+Lemma imset2Sl (A B : {pred aT}) (C : {pred aT2}) :
   A \subset B -> f2 @2: (A, C) \subset f2 @2: (B, C).
 Proof.
 move=> sAB; apply/subsetP=> _ /imset2P[x y Ax Cy ->].
 by apply/imset2P; exists x y; rewrite ?(subsetP sAB).
 Qed.
 
-Lemma imset2Sr (A B : pred aT2) (C : pred aT) :
+Lemma imset2Sr (A B : {pred aT2}) (C : {pred aT}) :
   A \subset B -> f2 @2: (C, A) \subset f2 @2: (C, B).
 Proof.
 move=> sAB; apply/subsetP=> _ /imset2P[x y Ax Cy ->].
 by apply/imset2P; exists x y; rewrite ?(subsetP sAB).
 Qed.
 
-Lemma imset2S (A B : pred aT) (A2 B2 : pred aT2) :
+Lemma imset2S (A B : {pred aT}) (A2 B2 : {pred aT2}) :
   A \subset B ->  A2 \subset B2 -> f2 @2: (A, A2) \subset f2 @2: (B, B2).
 Proof.  by move=> /(imset2Sl B2) sBA /(imset2Sr A)/subset_trans->. Qed.
 
 End ImsetProp.
 
-Implicit Types (f g : aT -> rT) (D : {set aT}) (R : pred rT).
+Implicit Types (f g : aT -> rT) (D : {set aT}) (R : {pred rT}).
 
 Lemma eq_preimset f g R : f =1 g -> f @^-1: R = g @^-1: R.
 Proof. by move=> eqfg; apply/setP => y; rewrite !inE eqfg. Qed.
@@ -1340,7 +1339,7 @@ move=> eqfg; apply/setP => y.
 by apply/imsetP/imsetP=> [] [x Dx ->]; exists x; rewrite ?eqfg.
 Qed.
 
-Lemma eq_in_imset2 (f g : aT -> aT2 -> rT) (D : pred aT) (D2 : pred aT2) :
+Lemma eq_in_imset2 (f g : aT -> aT2 -> rT) (D : {pred aT}) (D2 : {pred aT2}) :
   {in D & D2, f =2 g} -> f @2: (D, D2) = g @2: (D, D2).
 Proof.
 move=> eqfg; apply/setP => y.
@@ -1407,7 +1406,7 @@ Lemma big_setU1 a A F : a \notin A ->
   \big[aop/idx]_(i in a |: A) F i = aop (F a) (\big[aop/idx]_(i in A) F i).
 Proof. by move=> notAa; rewrite (@big_setD1 a) ?setU11 //= setU1K. Qed.
 
-Lemma big_imset h (A : pred I) G : {in A &, injective h} ->
+Lemma big_imset h (A : {pred I}) G : {in A &, injective h} ->
   \big[aop/idx]_(j in h @: A) G j = \big[aop/idx]_(i in A) G (h i).
 Proof.
 move=> injh; pose hA := mem (image h A).
@@ -1424,12 +1423,12 @@ symmetry; rewrite (negbTE nhAhi); apply/idP=> Ai.
 by case/imageP: nhAhi; exists i.
 Qed.
 
-Lemma big_imset_cond h (A : pred I) (P : pred J) G : {in A &, injective h} ->
+Lemma big_imset_cond h (A : {pred I}) (P : pred J) G : {in A &, injective h} ->
   \big[aop/idx]_(j in h @: A | P j) G j =
     \big[aop/idx]_(i in A | P (h i)) G (h i).
 Proof. by move=> h_inj; rewrite 2!big_mkcondr big_imset. Qed.
 
-Lemma partition_big_imset h (A : pred I) F :
+Lemma partition_big_imset h (A : {pred I}) F :
   \big[aop/idx]_(i in A) F i =
      \big[aop/idx]_(j in h @: A) \big[aop/idx]_(i in A | h i == j) F i.
 Proof. by apply: partition_big => i Ai; apply/imsetP; exists i. Qed.
@@ -1447,14 +1446,14 @@ Section Fun2Set1.
 Variables aT1 aT2 rT : finType.
 Variables (f : aT1 -> aT2 -> rT).
 
-Lemma imset2_set1l x1 (D2 : pred aT2) : f @2: ([set x1], D2) = f x1 @: D2.
+Lemma imset2_set1l x1 (D2 : {pred aT2}) : f @2: ([set x1], D2) = f x1 @: D2.
 Proof.
 apply/setP=> y; apply/imset2P/imsetP=> [[x x2 /set1P->]| [x2 Dx2 ->]].
   by exists x2.
 by exists x1 x2; rewrite ?set11.
 Qed.
 
-Lemma imset2_set1r x2 (D1 : pred aT1) : f @2: (D1, [set x2]) = f^~ x2 @: D1.
+Lemma imset2_set1r x2 (D1 : {pred aT1}) : f @2: (D1, [set x2]) = f^~ x2 @: D1.
 Proof.
 apply/setP=> y; apply/imset2P/imsetP=> [[x1 x Dx1 /set1P->]| [x1 Dx1 ->]].
   by exists x1.
@@ -1467,7 +1466,7 @@ Section CardFunImage.
 
 Variables aT aT2 rT : finType.
 Variables (f : aT -> rT) (g : rT -> aT) (f2 : aT -> aT2 -> rT).
-Variables (D : pred aT) (D2 : pred aT).
+Variables (D : {pred aT}) (D2 : {pred aT}).
 
 Lemma imset_card : #|f @: D| = #|image f D|.
 Proof. by rewrite [@imset]unlock cardsE. Qed.
@@ -1498,7 +1497,7 @@ End CardFunImage.
 
 Arguments imset_injP {aT rT f D}.
 
-Lemma on_card_preimset (aT rT : finType) (f : aT -> rT) (R : pred rT) :
+Lemma on_card_preimset (aT rT : finType) (f : aT -> rT) (R : {pred rT}) :
   {on R, bijective f} -> #|f @^-1: R| = #|R|.
 Proof.
 case=> g fK gK; rewrite -(can2_in_imset_pre gK) // card_in_imset //.
@@ -1539,7 +1538,7 @@ Section FunImageComp.
 
 Variables T T' U : finType.
 
-Lemma imset_comp (f : T' -> U) (g : T -> T') (H : pred T) :
+Lemma imset_comp (f : T' -> U) (g : T -> T') (H : {pred T}) :
   (f \o g) @: H = f @: (g @: H).
 Proof.
 apply/setP/subset_eqP/andP.
@@ -1603,7 +1602,7 @@ Notation "\bigcap_ ( i 'in' A ) F" :=
 Section BigSetOps.
 
 Variables T I : finType.
-Implicit Types (U : pred T) (P : pred I) (A B : {set I}) (F :  I -> {set T}).
+Implicit Types (U : {pred T}) (P : pred I) (A B : {set I}) (F :  I -> {set T}).
 
 (* It is very hard to use this lemma, because the unification fails to *)
 (* defer the F j pattern (even though it's a Miller pattern!).         *)
@@ -1714,7 +1713,7 @@ Variables (aT1 aT2 rT : finType) (f : aT1 -> aT2 -> rT).
 Section Curry.
 
 Variables (A1 : {set aT1}) (A2 : {set aT2}).
-Variables (D1 : pred aT1) (D2 : pred aT2).
+Variables (D1 : {pred aT1}) (D2 : {pred aT2}).
 
 Lemma curry_imset2X : f @2: (A1, A2) = prod_curry f @: (setX A1 A2).
 Proof.
diff --git a/mathcomp/ssreflect/fintype.v b/mathcomp/ssreflect/fintype.v
index 04c1732..e58ae61 100644
--- a/mathcomp/ssreflect/fintype.v
+++ b/mathcomp/ssreflect/fintype.v
@@ -461,9 +461,7 @@ Section OpsTheory.
 
 Variable T : finType.
 
-Implicit Types A B C P Q : pred T.
-Implicit Types x y : T.
-Implicit Type s : seq T.
+Implicit Types (A B C : {pred T}) (P Q : pred T) (x y : T) (s : seq T).
 
 Lemma enumP : Finite.axiom (Finite.enum T).
 Proof. by rewrite unlock; case T => ? [? []]. Qed.
@@ -478,7 +476,7 @@ Proof. exact: filter_predT. Qed.
 Lemma mem_enum A : enum A =i A.
 Proof. by move=> x; rewrite mem_filter andbC -has_pred1 has_count enumP. Qed.
 
-Lemma enum_uniq : uniq (enum P).
+Lemma enum_uniq A : uniq (enum A).
 Proof.
 by apply/filter_uniq/count_mem_uniq => x; rewrite enumP -enumT mem_enum.
 Qed.
@@ -504,8 +502,8 @@ Qed.
 
 End EnumPick.
 
-Lemma eq_enum P Q : P =i Q -> enum P = enum Q.
-Proof. by move=> eqPQ; apply: eq_filter. Qed.
+Lemma eq_enum A B : A =i B -> enum A = enum B.
+Proof. by move=> eqAB; apply: eq_filter. Qed.
 
 Lemma eq_pick P Q : P =1 Q -> pick P = pick Q.
 Proof. by move=> eqPQ; rewrite /pick (eq_enum eqPQ). Qed.
@@ -640,17 +638,17 @@ Hint Resolve subxx_hint : core.
 Lemma subxx (pT : predType T) (pA : pT) : pA \subset pA.
 Proof. by []. Qed.
 
-Lemma eq_subset A1 A2 : A1 =i A2 -> subset (mem A1) =1 subset (mem A2).
+Lemma eq_subset A B : A =i B -> subset (mem A) =1 subset (mem B).
 Proof.
-move=> eqA12 [B]; rewrite !unlock; congr (_ == 0).
-by apply: eq_card => x; rewrite inE /= eqA12.
+move=> eqAB [C]; rewrite !unlock; congr (_ == 0).
+by apply: eq_card => x; rewrite inE /= eqAB.
 Qed.
 
-Lemma eq_subset_r B1 B2 : B1 =i B2 ->
-  (@subset T)^~ (mem B1) =1 (@subset T)^~ (mem B2).
+Lemma eq_subset_r A B :
+   A =i B -> (@subset T)^~ (mem A) =1 (@subset T)^~ (mem B).
 Proof.
-move=> eqB12 [A]; rewrite !unlock; congr (_ == 0).
-by apply: eq_card => x; rewrite !inE /= eqB12.
+move=> eqAB [C]; rewrite !unlock; congr (_ == 0).
+by apply: eq_card => x; rewrite !inE /= eqAB.
 Qed.
 
 Lemma eq_subxx A B : A =i B -> A \subset B.
@@ -746,8 +744,8 @@ move=> eAB [C]; congr (_ && _); first exact: (eq_subset eAB).
 by rewrite (eq_subset_r eAB).
 Qed.
 
-Lemma eq_proper_r A B : A =i B ->
-  (@proper T)^~ (mem A) =1 (@proper T)^~ (mem B).
+Lemma eq_proper_r A B :
+  A =i B -> (@proper T)^~ (mem A) =1 (@proper T)^~ (mem B).
 Proof.
 move=> eAB [C]; congr (_ && _); first exact: (eq_subset_r eAB).
 by rewrite (eq_subset eAB).
@@ -756,15 +754,15 @@ Qed.
 Lemma disjoint_sym A B : [disjoint A & B] = [disjoint B & A].
 Proof. by congr (_ == 0); apply: eq_card => x; apply: andbC. Qed.
 
-Lemma eq_disjoint A1 A2 : A1 =i A2 -> disjoint (mem A1) =1 disjoint (mem A2).
+Lemma eq_disjoint A B : A =i B -> disjoint (mem A) =1 disjoint (mem B).
 Proof.
-by move=> eqA12 [B]; congr (_ == 0); apply: eq_card => x; rewrite !inE eqA12.
+by move=> eqAB [C]; congr (_ == 0); apply: eq_card => x; rewrite !inE eqAB.
 Qed.
 
-Lemma eq_disjoint_r B1 B2 : B1 =i B2 ->
-  (@disjoint T)^~ (mem B1) =1 (@disjoint T)^~ (mem B2).
+Lemma eq_disjoint_r A B : A =i B ->
+  (@disjoint T)^~ (mem A) =1 (@disjoint T)^~ (mem B).
 Proof.
-by move=> eqB12 [A]; congr (_ == 0); apply: eq_card => x; rewrite !inE eqB12.
+by move=> eqAB [C]; congr (_ == 0); apply: eq_card => x; rewrite !inE eqAB.
 Qed.
 
 Lemma subset_disjoint A B : (A \subset B) = [disjoint A & [predC B]].
@@ -787,9 +785,9 @@ Proof. by move/eq_disjoint->; apply: disjoint0. Qed.
 
 Lemma disjoint1 x A : [disjoint pred1 x & A] = (x \notin A).
 Proof.
-apply/negbRL/(sameP (pred0Pn _)).
+apply/negbRL/(sameP (pred0Pn _))=> /=.
 apply: introP => [Ax | notAx [_ /andP[/eqP->]]]; last exact: negP.
-by exists x; rewrite !inE eqxx.
+by exists x; rewrite inE eqxx.
 Qed.
 
 Lemma eq_disjoint1 x A B :
@@ -863,7 +861,7 @@ Notation "'forall_ view" := (forallPP (fun _ => view))
 Section Quantifiers.
 
 Variables (T : finType) (rT : T -> eqType).
-Implicit Type (D P : pred T) (f : forall x, rT x).
+Implicit Types (D P : pred T) (f : forall x, rT x).
 
 Lemma forallP P : reflect (forall x, P x) [forall x, P x].
 Proof. exact: 'forall_idP. Qed.
@@ -1059,7 +1057,7 @@ Notation "[ 'arg' 'max_' ( i > i0 ) F ]" := [arg max_(i > i0 | true) F]
 Section Injectiveb.
 
 Variables (aT : finType) (rT : eqType) (f : aT -> rT).
-Implicit Type D : pred aT.
+Implicit Type D : {pred aT}.
 
 Definition dinjectiveb D := uniq (map f (enum D)).
 
@@ -1113,7 +1111,7 @@ Notation "[ 'seq' F | x 'in' A ]" := (image (fun x => F) A)
 Notation "[ 'seq' F | x : T 'in' A ]" := (image (fun x : T => F) A)
   (at level 0, F at level 99, x ident, only parsing) : seq_scope.
 Notation "[ 'seq' F | x : T ]" :=
-  [seq F | x : T in sort_of_simpl_pred (@pred_of_argType T)]
+  [seq F | x : T in pred_of_simpl (@pred_of_argType T)]
   (at level 0, F at level 99, x ident,
    format "'[hv' [ 'seq'  F '/ '  |  x  :  T ] ']'") : seq_scope.
 Notation "[ 'seq' F , x ]" := [seq F | x : _ ]
@@ -1124,7 +1122,7 @@ Definition codom T T' f := @image_mem T T' f (mem T).
 Section Image.
 
 Variable T : finType.
-Implicit Type A : pred T.
+Implicit Type A : {pred T}.
 
 Section SizeImage.
 
@@ -1236,7 +1234,8 @@ Prenex Implicits codom iinv.
 Arguments imageP {T T' f A y}.
 Arguments codomP {T T' f y}.
 
-Lemma flatten_imageP (aT : finType) (rT : eqType) A (P : pred aT) (y : rT) :
+Lemma flatten_imageP (aT : finType) (rT : eqType)
+                     (A : aT -> seq rT) (P : {pred aT}) (y : rT) :
   reflect (exists2 x, x \in P & y \in A x) (y \in flatten [seq A x | x in P]).
 Proof.
 by apply: (iffP flatten_mapP) => [][x Px]; exists x; rewrite ?mem_enum in Px *.
@@ -1246,7 +1245,7 @@ Arguments flatten_imageP {aT rT A P y}.
 Section CardFunImage.
 
 Variables (T T' : finType) (f : T -> T').
-Implicit Type A : pred T.
+Implicit Type A : {pred T}.
 
 Lemma leq_image_card A : #|image f A| <= #|A|.
 Proof. by rewrite (cardE A) -(size_map f) card_size. Qed.
@@ -1271,7 +1270,7 @@ Proof. by apply: card_in_image; apply: in2W. Qed.
 Lemma card_codom : #|codom f| = #|T|.
 Proof. exact: card_image. Qed.
 
-Lemma card_preim (B : pred T') : #|[preim f of B]| = #|[predI codom f & B]|.
+Lemma card_preim (B : {pred T'}) : #|[preim f of B]| = #|[predI codom f & B]|.
 Proof.
 rewrite -card_image /=; apply: eq_card => y.
 by rewrite [y \in _]image_pre !inE andbC.
@@ -1330,7 +1329,7 @@ Section EqImage.
 
 Variables (T : finType) (T' : Type).
 
-Lemma eq_image (A B : pred T) (f g : T -> T') :
+Lemma eq_image (A B : {pred T}) (f g : T -> T') :
   A =i B -> f =1 g -> image f A = image g B.
 Proof.
 by move=> eqAB eqfg; rewrite /image_mem (eq_enum eqAB) (eq_map eqfg).
@@ -1461,7 +1460,7 @@ Variable sfT : subFinType P.
 Lemma card_sub : #|sfT| = #|[pred x | P x]|.
 Proof. by rewrite -(eq_card (codom_val sfT)) (card_image val_inj). Qed.
 
-Lemma eq_card_sub (A : pred sfT) : A =i predT -> #|A| = #|[pred x | P x]|.
+Lemma eq_card_sub (A : {pred sfT}) : A =i predT -> #|A| = #|[pred x | P x]|.
 Proof. exact: eq_card_trans card_sub. Qed.
 
 End FinTypeForSub.
@@ -1695,7 +1694,7 @@ Proof. exact: inv_inj rev_ordK. Qed.
 Section EnumRank.
 
 Variable T : finType.
-Implicit Type A : pred T.
+Implicit Type A : {pred T}.
 
 Lemma enum_rank_subproof x0 A : x0 \in A -> 0 < #|A|.
 Proof. by move=> Ax0; rewrite (cardD1 x0) Ax0. Qed.
@@ -2026,7 +2025,7 @@ Variable T1 T2 : finType.
 
 Definition prod_enum := [seq (x1, x2) | x1 <- enum T1, x2 <- enum T2].
 
-Lemma predX_prod_enum (A1 : pred T1) (A2 : pred T2) :
+Lemma predX_prod_enum (A1 : {pred T1}) (A2 : {pred T2}) :
   count [predX A1 & A2] prod_enum = #|A1| * #|A2|.
 Proof.
 rewrite !cardE !size_filter -!enumT /prod_enum.
@@ -2042,13 +2041,14 @@ Qed.
 Definition prod_finMixin := Eval hnf in FinMixin prod_enumP.
 Canonical prod_finType := Eval hnf in FinType (T1 * T2) prod_finMixin.
 
-Lemma cardX (A1 : pred T1) (A2 : pred T2) : #|[predX A1 & A2]| = #|A1| * #|A2|.
+Lemma cardX (A1 : {pred T1}) (A2 : {pred T2}) :
+  #|[predX A1 & A2]| = #|A1| * #|A2|.
 Proof. by rewrite -predX_prod_enum unlock size_filter unlock. Qed.
 
 Lemma card_prod : #|{: T1 * T2}| = #|T1| * #|T2|.
 Proof. by rewrite -cardX; apply: eq_card; case. Qed.
 
-Lemma eq_card_prod (A : pred (T1 * T2)) : A =i predT -> #|A| = #|T1| * #|T2|.
+Lemma eq_card_prod (A : {pred (T1 * T2)}) : A =i predT -> #|A| = #|T1| * #|T2|.
 Proof. exact: eq_card_trans card_prod. Qed.
 
 End ProdFinType.
diff --git a/mathcomp/ssreflect/prime.v b/mathcomp/ssreflect/prime.v
index 9a01ed1..bfecfa9 100644
--- a/mathcomp/ssreflect/prime.v
+++ b/mathcomp/ssreflect/prime.v
@@ -7,7 +7,9 @@ From mathcomp Require Import fintype div bigop.
 (* This file contains the definitions of:                                     *)
 (*        prime p <=> p is a prime.                                           *)
 (*       primes m == the sorted list of prime divisors of m > 1, else [::].   *)
-(*        pfactor == the type of prime factors, syntax (p ^ e)%pfactor.       *)
+(*    pfactor p e == the value p ^ e of a prime factor (p, e).                *)
+(*    NumFactor f == print version of a prime factor, converting the prime    *)
+(*                   component to a Num (which can print large values).       *)
 (* prime_decomp m == the list of prime factors of m > 1, sorted by primes.    *)
 (*       logn p m == the e such that (p ^ e) \in prime_decomp n, else 0.      *)
 (*  trunc_log p m == the largest e such that p ^ e <= m, or 0 if p or m is 0. *)
@@ -26,16 +28,15 @@ From mathcomp Require Import fintype div bigop.
 (*                   that (p \in \pi(n)) = (p \in primes n).                  *)
 (*         \pi(A) == the set of primes of #|A|, with A a collective predicate *)
 (*                   over a finite Type.                                      *)
-(*     -> The notation \pi(A) is implemented with a collapsible Coercion, so  *)
-(*        the type of A must coerce to finpred_class (e.g., by coercing to    *)
-(*        {set T}), not merely implement the predType interface (as seq T     *)
-(*        does).                                                              *)
-(*     -> The expression #|A| will only appear in \pi(A) after simplification *)
-(*        collapses the coercion stack, so it is advisable to do so early on. *)
+(*    -> The notation \pi(A) is implemented with a collapsible Coercion. The  *)
+(*       type of A must coerce to finpred_sort (e.g., by coercing to {set T}) *)
+(*       and not merely implement the predType interface (as seq T does).     *)
+(*    -> The expression #|A| will only appear in \pi(A) after simplification  *)
+(*       collapses the coercion, so it is advisable to do so early on.        *)
 (*     pi.-nat n <=> n > 0 and all prime divisors of n are in pi.             *)
 (*          n`_pi == the pi-part of n -- the largest pi.-nat divisor of n.    *)
 (*               := \prod_(0 <= p < n.+1 | p \in pi) p ^ logn p n.            *)
-(*     -> The nat >-> nat_pred coercion lets us write p.-nat n and n`_p.      *)
+(*    -> The nat >-> nat_pred coercion lets us write p.-nat n and n`_p.       *)
 (* In addition to the lemmas relevant to these definitions, this file also    *)
 (* contains the dvdn_sum lemma, so that bigop.v doesn't depend on div.v.      *)
 (******************************************************************************)
@@ -56,7 +57,9 @@ Unset Printing Implicit Defensive.
 (* which can then be used casually in proofs with moderately-sized numeric  *)
 (* values (indeed, the code here performs well for up to 6-digit numbers).  *)
 
-(* We start with faster mod-2 functions. *)
+Module Import PrimeDecompAux.
+
+(* We start with faster mod-2 and 2-valuation functions. *)
 
 Fixpoint edivn2 q r := if r is r'.+2 then edivn2 q.+1 r' else (q, r).
 
@@ -95,21 +98,35 @@ Variant ifnz_spec T n (x y : T) : T -> Type :=
 Lemma ifnzP T n (x y : T) : ifnz_spec n x y (ifnz n x y).
 Proof. by case: n => [|n]; [right | left]. Qed.
 
-(* For pretty-printing. *)
-Definition NumFactor (f : nat * nat) := ([Num of f.1], f.2).
+(* The list of divisors and the Euler function are computed directly from    *)
+(* the decomposition, using a merge_sort variant sort of the divisor list.   *)
 
-Definition pfactor p e := p ^ e.
+Definition add_divisors f divs :=
+  let: (p, e) := f in
+  let add1 divs' := merge leq (map (NatTrec.mul p) divs') divs in
+  iter e add1 divs.
+
+Import NatTrec.
+
+Definition add_totient_factor f m := let: (p, e) := f in p.-1 * p ^ e.-1 * m.
 
 Definition cons_pfactor (p e : nat) pd := ifnz e ((p, e) :: pd) pd.
 
-Local Notation "p ^? e :: pd" := (cons_pfactor p e pd)
+Notation "p ^? e :: pd" := (cons_pfactor p e pd)
   (at level 30, e at level 30, pd at level 60) : nat_scope.
 
+End PrimeDecompAux.
+
+(* For pretty-printing. *)
+Definition NumFactor (f : nat * nat) := ([Num of f.1], f.2).
+
+Definition pfactor p e := p ^ e.
+
 Section prime_decomp.
 
 Import NatTrec.
 
-Fixpoint prime_decomp_rec m k a b c e :=
+Local Fixpoint prime_decomp_rec m k a b c e :=
   let p := k.*2.+1 in
   if a is a'.+1 then
     if b - (ifnz e 1 k - c) is b'.+1 then
@@ -128,16 +145,6 @@ Definition prime_decomp n :=
   let: (b, c) := edivn (2 - bc) 2 in
   2 ^? e2 :: [rec m2.*2.+1, 1, a, b, c, 0].
 
-(* The list of divisors and the Euler function are computed directly from *)
-(* the decomposition, using a merge_sort variant sort the divisor list.   *)
-
-Definition add_divisors f divs :=
-  let: (p, e) := f in
-  let add1 divs' := merge leq (map (NatTrec.mul p) divs') divs in
-  iter e add1 divs.
-
-Definition add_totient_factor f m := let: (p, e) := f in p.-1 * p ^ e.-1 * m.
-
 End prime_decomp.
 
 Definition primes n := unzip1 (prime_decomp n).
@@ -146,19 +153,16 @@ Definition prime p := if prime_decomp p is [:: (_ , 1)] then true else false.
 
 Definition nat_pred := simpl_pred nat.
 
-Definition pi_unwrapped_arg := nat.
-Definition pi_wrapped_arg := wrapped nat.
-Coercion unwrap_pi_arg (wa : pi_wrapped_arg) : pi_unwrapped_arg := unwrap wa.
-Coercion pi_arg_of_nat (n : nat) := Wrap n : pi_wrapped_arg.
-Coercion pi_arg_of_fin_pred T pT (A : @fin_pred_sort T pT) : pi_wrapped_arg :=
-  Wrap #|A|.
-
-Definition pi_of (n : pi_unwrapped_arg) : nat_pred := [pred p in primes n].
+Definition pi_arg := nat.
+Coercion pi_arg_of_nat (n : nat) : pi_arg := n.
+Coercion pi_arg_of_fin_pred T pT (A : @fin_pred_sort T pT) : pi_arg := #|A|.
+Arguments pi_arg_of_nat n /.
+Arguments pi_arg_of_fin_pred {T pT} A /.
+Definition pi_of (n : pi_arg) : nat_pred := [pred p in primes n].
 
 Notation "\pi ( n )" := (pi_of n)
   (at level 2, format "\pi ( n )") : nat_scope.
-Notation "\p 'i' ( A )" := \pi(#|A|)
-  (at level 2, format "\p 'i' ( A )") : nat_scope.
+Notation "\pi ( A )" := \pi(#|A|) (only printing) : nat_scope.
 
 Definition pdiv n := head 1 (primes n).
 
diff --git a/mathcomp/ssreflect/seq.v b/mathcomp/ssreflect/seq.v
index 1c8e150..5576355 100644
--- a/mathcomp/ssreflect/seq.v
+++ b/mathcomp/ssreflect/seq.v
@@ -928,14 +928,13 @@ Proof. by rewrite -size_eq0 size_filter has_count lt0n. Qed.
 Fixpoint mem_seq (s : seq T) :=
   if s is y :: s' then xpredU1 y (mem_seq s') else xpred0.
 
-Definition eqseq_class := seq T.
-Identity Coercion seq_of_eqseq : eqseq_class >-> seq.
+Definition seq_eqclass := seq T. 
+Identity Coercion seq_of_eqclass : seq_eqclass >-> seq.
+Coercion pred_of_seq (s : seq_eqclass) : {pred T} := mem_seq s.
 
-Coercion pred_of_eq_seq (s : eqseq_class) : pred_class := [eta mem_seq s].
-
-Canonical seq_predType := @mkPredType T (seq T) pred_of_eq_seq.
+Canonical seq_predType := PredType (pred_of_seq : seq T -> pred T).
 (* The line below makes mem_seq a canonical instance of topred. *)
-Canonical mem_seq_predType := mkPredType mem_seq.
+Canonical mem_seq_predType := PredType mem_seq.
 
 Lemma in_cons y s x : (x \in y :: s) = (x == y) || (x \in s).
 Proof. by []. Qed.
@@ -949,14 +948,13 @@ Proof. by rewrite in_cons orbF. Qed.
  (* to be repeated after the Section discharge. *)
 Let inE := (mem_seq1, in_cons, inE).
 
-Lemma mem_seq2 x y1 y2 : (x \in [:: y1; y2]) = xpred2 y1 y2 x.
+Lemma mem_seq2 x y z : (x \in [:: y; z]) = xpred2 y z x.
 Proof. by rewrite !inE. Qed.
 
-Lemma mem_seq3  x y1 y2 y3 : (x \in [:: y1; y2; y3]) = xpred3 y1 y2 y3 x.
+Lemma mem_seq3 x y z t : (x \in [:: y; z; t]) = xpred3 y z t x.
 Proof. by rewrite !inE. Qed.
 
-Lemma mem_seq4  x y1 y2 y3 y4 :
-  (x \in [:: y1; y2; y3; y4]) = xpred4 y1 y2 y3 y4 x.
+Lemma mem_seq4 x y z t u : (x \in [:: y; z; t; u]) = xpred4 y z t u x.
 Proof. by rewrite !inE. Qed.
 
 Lemma mem_cat x s1 s2 : (x \in s1 ++ s2) = (x \in s1) || (x \in s2).
@@ -1285,6 +1283,7 @@ Definition inE := (mem_seq1, in_cons, inE).
 Prenex Implicits mem_seq1 constant uniq undup index.
 
 Arguments eqseq {T} !_ !_.
+Arguments pred_of_seq {T} s x /.
 Arguments eqseqP {T x y}.
 Arguments hasP {T a s}.
 Arguments hasPn {T a s}.
@@ -2253,7 +2252,7 @@ Qed.
 
 Lemma perm_pmap s t : perm_eq s t -> perm_eq (pmap f s) (pmap f t).
 Proof.
-move=> eq_st; apply/(perm_map_inj (@Some_inj _)); rewrite !pmapS_filter.
+move=> eq_st; apply/(perm_map_inj Some_inj); rewrite !pmapS_filter.
 exact/perm_map/perm_filter.
 Qed.
 
diff --git a/mathcomp/ssreflect/ssrbool.v b/mathcomp/ssreflect/ssrbool.v
index c96ca6a..7eb7fd9 100644
--- a/mathcomp/ssreflect/ssrbool.v
+++ b/mathcomp/ssreflect/ssrbool.v
@@ -1 +1,40 @@
-From Coq Require Export ssrbool.
\ No newline at end of file
+From mathcomp Require Import ssreflect ssrfun.
+From Coq Require Export ssrbool.
+
+Notation "{ 'pred' T }" := (pred_sort (predPredType T)) (at level 0,
+  format "{ 'pred'  T }") : type_scope.
+
+Lemma simpl_pred_sortE T (p : pred T) : (SimplPred p : {pred T}) =1 p.
+Proof. by []. Qed.
+Definition inE := (inE, simpl_pred_sortE).
+
+Definition PredType : forall T pT, (pT -> pred T) -> predType T.
+exact PredType || exact mkPredType.
+Defined.
+Arguments PredType [T pT] toP.
+
+Definition simpl_rel T := T -> simpl_pred T.
+Definition SimplRel {T} (r : rel T) : simpl_rel T := fun x => SimplPred (r x).
+Coercion rel_of_simpl_rel T (sr : simpl_rel T) : rel T := sr.
+Arguments rel_of_simpl_rel {T} sr x / y : rename.
+
+Notation "[ 'rel' x y | E ]" := (SimplRel (fun x y => E%B)) (at level 0,
+  x ident, y ident, format "'[hv' [ 'rel'  x  y  | '/ '  E ] ']'") : fun_scope.
+Notation "[ 'rel' x y : T | E ]" := (SimplRel (fun x y : T => E%B)) (at level 0,
+  x ident, y ident, only parsing) : fun_scope.
+Notation "[ 'rel' x y 'in' A & B | E ]" :=
+  [rel x y | (x \in A) && (y \in B) && E] (at level 0, x ident, y ident,
+  format "'[hv' [ 'rel'  x  y  'in'  A  &  B  | '/ '  E ] ']'") : fun_scope.
+Notation "[ 'rel' x y 'in' A & B ]" := [rel x y | (x \in A) && (y \in B)]
+  (at level 0, x ident, y ident,
+  format "'[hv' [ 'rel'  x  y  'in'  A  &  B ] ']'") : fun_scope.
+Notation "[ 'rel' x y 'in' A | E ]" := [rel x y in A & A | E]
+  (at level 0, x ident, y ident,
+  format "'[hv' [ 'rel'  x  y  'in'  A  | '/ '  E ] ']'") : fun_scope.
+Notation "[ 'rel' x y 'in' A ]" := [rel x y in A & A] (at level 0,
+  x ident, y ident, format "'[hv' [ 'rel'  x  y  'in'  A ] ']'") : fun_scope.
+
+Notation xrelpre := (fun f (r : rel _) x y => r (f x) (f y)).
+Definition relpre {T rT} (f : T -> rT)  (r : rel rT) :=
+  [rel x y | r (f x) (f y)].
+
diff --git a/mathcomp/ssreflect/ssreflect.v b/mathcomp/ssreflect/ssreflect.v
index a7b5ef8..fe06c0d 100644
--- a/mathcomp/ssreflect/ssreflect.v
+++ b/mathcomp/ssreflect/ssreflect.v
@@ -5,3 +5,31 @@ Global Set SsrOldRewriteGoalsOrder.
 Global Set Asymmetric Patterns.
 Global Set Bullet Behavior "None".
 
+Module NonPropType.
+
+Structure call_of (condition : unit) (result : bool) := Call {callee : Type}.
+Definition maybeProp (T : Type) := tt.
+Definition call T := Call (maybeProp T) false T.
+
+Structure test_of (result : bool) := Test {condition :> unit}.
+Definition test_Prop (P : Prop) := Test true (maybeProp P).
+Definition test_negative := Test false tt.
+
+Structure type :=
+  Check {result : bool; test : test_of result; frame : call_of test result}.
+Definition check result test frame := @Check result test frame.
+
+Module Exports.
+Canonical call.
+Canonical test_Prop.
+Canonical test_negative.
+Canonical check.
+Notation nonPropType := type.
+Coercion callee : call_of >-> Sortclass.
+Coercion frame : type >-> call_of.
+Notation notProp T := (@check false test_negative (call T)).
+End Exports.
+
+End NonPropType.
+Export NonPropType.Exports.
+
diff --git a/mathcomp/ssreflect/ssrfun.v b/mathcomp/ssreflect/ssrfun.v
index 2dd7103..ed18941 100644
--- a/mathcomp/ssreflect/ssrfun.v
+++ b/mathcomp/ssreflect/ssrfun.v
@@ -1,2 +1,5 @@
+From mathcomp Require Import ssreflect.
 From Coq Require Export ssrfun.
 From mathcomp Require Export ssrnotations.
+
+Definition Some_inj {T : nonPropType} := @Some_inj T.
diff --git a/mathcomp/ssreflect/ssrnat.v b/mathcomp/ssreflect/ssrnat.v
index 9222124..86f8fb2 100644
--- a/mathcomp/ssreflect/ssrnat.v
+++ b/mathcomp/ssreflect/ssrnat.v
@@ -1382,7 +1382,7 @@ Qed.
 Section Monotonicity.
 Variable T : Type.
 
-Lemma homo_ltn_in (D : pred nat) (f : nat -> T) (r : T -> T -> Prop) :
+Lemma homo_ltn_in (D : {pred nat}) (f : nat -> T) (r : T -> T -> Prop) :
   (forall y x z, r x y -> r y z -> r x z) ->
   {in D &, forall i j k, i < k < j -> k \in D} ->
   {in D, forall i, i.+1 \in D -> r (f i) (f i.+1)} ->
@@ -1400,7 +1400,7 @@ Lemma homo_ltn (f : nat -> T) (r : T -> T -> Prop) :
   (forall i, r (f i) (f i.+1)) -> {homo f : i j / i < j >-> r i j}.
 Proof. by move=> /(@homo_ltn_in predT f) fr fS i j; apply: fr. Qed.
 
-Lemma homo_leq_in (D : pred nat) (f : nat -> T) (r : T -> T -> Prop) :
+Lemma homo_leq_in (D : {pred nat}) (f : nat -> T) (r : T -> T -> Prop) :
   (forall x, r x x) -> (forall y x z, r x y -> r y z -> r x z) ->
   {in D &, forall i j k, i < k < j -> k \in D} ->
   {in D, forall i, i.+1 \in D -> r (f i) (f i.+1)} ->
@@ -1464,7 +1464,7 @@ Proof. exact: total_homo_mono. Qed.
 Lemma leq_nmono : {homo f : m n /~ m < n} -> {mono f : m n /~ m <= n}.
 Proof. exact: total_homo_mono. Qed.
 
-Variable (D D' : pred nat).
+Variables (D D' : {pred nat}).
 
 Lemma ltnW_homo_in : {in D & D', {homo f : m n / m < n}} ->
   {in D & D', {homo f : m n / m <= n}}.
diff --git a/mathcomp/ssreflect/tuple.v b/mathcomp/ssreflect/tuple.v
index 77e9dc0..dd73664 100644
--- a/mathcomp/ssreflect/tuple.v
+++ b/mathcomp/ssreflect/tuple.v
@@ -275,8 +275,7 @@ Variables (n : nat) (T : eqType).
 Definition tuple_eqMixin := Eval hnf in [eqMixin of n.-tuple T by <:].
 Canonical tuple_eqType := Eval hnf in EqType (n.-tuple T) tuple_eqMixin.
 
-Canonical tuple_predType :=
-  Eval hnf in mkPredType (fun t : n.-tuple T => mem_seq t).
+Canonical tuple_predType := PredType (pred_of_seq : n.-tuple T -> pred T).
 
 Lemma memtE (t : n.-tuple T) : mem t = mem (tval t).
 Proof. by []. Qed.
@@ -371,7 +370,7 @@ Canonical tuple_subFinType := Eval hnf in [subFinType of n.-tuple T].
 Lemma card_tuple : #|{:n.-tuple T}| = #|T| ^ n.
 Proof. by rewrite [#|_|]cardT enumT unlock FinTuple.size_enum. Qed.
 
-Lemma enum_tupleP (A : pred T) : size (enum A) == #|A|.
+Lemma enum_tupleP (A : {pred T}) : size (enum A) == #|A|.
 Proof. by rewrite -cardE. Qed.
 Canonical enum_tuple A := Tuple (enum_tupleP A).
 
@@ -389,7 +388,7 @@ Qed.
 
 Section ImageTuple.
 
-Variables (T' : Type) (f : T -> T') (A : pred T).
+Variables (T' : Type) (f : T -> T') (A : {pred T}).
 
 Canonical image_tuple : #|A|.-tuple T' := [tuple of image f A].
 Canonical codom_tuple : #|T|.-tuple T' := [tuple of codom f].