Merge pull request #337 from math-comp/coq-ssrbool-refactor-compat

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

25 files changed, 283 insertions, 229 deletions

diff --git a/mathcomp/algebra/interval.v b/mathcomp/algebra/interval.v
index 7c1ab8f..eb0785f 100644
--- a/mathcomp/algebra/interval.v
+++ b/mathcomp/algebra/interval.v
@@ -331,7 +331,7 @@ Definition pred_of_itv (i : interval R) : pred R :=
         | BOpen_if b ub => x <= ub ?< if b
         | BInfty => true
       end].
-Canonical Structure itvPredType := Eval hnf in mkPredType pred_of_itv.
+Canonical Structure itvPredType := PredType pred_of_itv.
 
 (* we compute a set of rewrite rules associated to an interval *)
 Definition itv_rewrite (i : interval R) x : Type :=
diff --git a/mathcomp/algebra/poly.v b/mathcomp/algebra/poly.v
index e0a8e5d..d898774 100644
--- a/mathcomp/algebra/poly.v
+++ b/mathcomp/algebra/poly.v
@@ -1298,13 +1298,14 @@ Qed.
 
 (* Lifting a ring predicate to polynomials. *)
 
-Definition polyOver (S : pred_class) :=
-  [qualify a p : {poly R} | all (mem S) p].
+Implicit Type S : {pred R}.
+
+Definition polyOver S := [qualify a p : {poly R} | all (mem S) p].
 
 Fact polyOver_key S : pred_key (polyOver S). Proof. by []. Qed.
 Canonical polyOver_keyed S := KeyedQualifier (polyOver_key S).
 
-Lemma polyOverS (S1 S2 : pred_class) :
+Lemma polyOverS (S1 S2 : {pred R}) :
   {subset S1 <= S2} -> {subset polyOver S1 <= polyOver S2}.
 Proof.
 by move=> sS12 p /(all_nthP 0)S1p; apply/(all_nthP 0)=> i /S1p; apply: sS12.
@@ -1313,7 +1314,7 @@ Qed.
 Lemma polyOver0 S : 0 \is a polyOver S.
 Proof. by rewrite qualifE polyseq0. Qed.
 
-Lemma polyOver_poly (S : pred_class) n E :
+Lemma polyOver_poly S n E :
   (forall i, i < n -> E i \in S) -> \poly_(i < n) E i \is a polyOver S.
 Proof.
 move=> S_E; apply/(all_nthP 0)=> i lt_i_p /=; rewrite coef_poly.
@@ -1322,7 +1323,7 @@ Qed.
 
 Section PolyOverAdd.
 
-Variables (S : predPredType R) (addS : addrPred S) (kS : keyed_pred addS).
+Variables (S : {pred R}) (addS : addrPred S) (kS : keyed_pred addS).
 
 Lemma polyOverP {p} : reflect (forall i, p`_i \in kS) (p \in polyOver kS).
 Proof.
@@ -1354,7 +1355,7 @@ Canonical polyOver_zmodPred S addS kS := ZmodPred (@polyOverNr S addS kS).
 
 Section PolyOverSemiring.
 
-Context (S : pred_class) (ringS : @semiringPred R S) (kS : keyed_pred ringS).
+Variables (S : {pred R}) (ringS : semiringPred S) (kS : keyed_pred ringS).
 
 Fact polyOver_mulr_closed : mulr_closed (polyOver kS).
 Proof.
@@ -1382,7 +1383,7 @@ End PolyOverSemiring.
 
 Section PolyOverRing.
 
-Context (S : pred_class) (ringS : @subringPred R S) (kS : keyed_pred ringS).
+Variables (S : {pred R}) (ringS : subringPred S) (kS : keyed_pred ringS).
 Canonical polyOver_smulrPred := SmulrPred (polyOver_mulr_closed kS).
 Canonical polyOver_subringPred := SubringPred (polyOver_mulr_closed kS).
 
diff --git a/mathcomp/algebra/rat.v b/mathcomp/algebra/rat.v
index 8654fd1..228a824 100644
--- a/mathcomp/algebra/rat.v
+++ b/mathcomp/algebra/rat.v
@@ -689,7 +689,8 @@ Proof. by rewrite /ratr numq_int denq_int divr1. Qed.
 Lemma ratr_nat n : ratr n%:R = n%:R.
 Proof. exact: (ratr_int n). Qed.
 
-Lemma rpred_rat S (ringS : @divringPred R S) (kS : keyed_pred ringS) a :
+Lemma rpred_rat (S : {pred R}) (ringS : divringPred S) (kS : keyed_pred ringS)
+                a :
   ratr a \in kS.
 Proof. by rewrite rpred_div ?rpred_int. Qed.
 
diff --git a/mathcomp/algebra/ring_quotient.v b/mathcomp/algebra/ring_quotient.v
index 7e6bbf3..22aa279 100644
--- a/mathcomp/algebra/ring_quotient.v
+++ b/mathcomp/algebra/ring_quotient.v
@@ -38,9 +38,9 @@ From mathcomp Require Import ssrfun seq ssralg generic_quotient.
 (*   unitRingQuotType ... u i == As in the previous cases, instance of unit   *)
 (*                               ring whose unit predicate  is obtained from  *)
 (*                               u and the inverse from i.                    *)
-(*                 idealr R S == (S : pred R) is a non-trivial, decidable,    *)
+(*                 idealr R S == S : {pred R} is a non-trivial, decidable,    *)
 (*                               right ideal of the ring R.                   *)
-(*           prime_idealr R S == (S : pred R) is a non-trivial, decidable,    *)
+(*           prime_idealr R S == S : {pred R} is a non-trivial, decidable,    *)
 (*                               right, prime ideal of the ring R.            *)
 (*                                                                            *)
 (* The formalization of ideals features the following constructions:          *)
@@ -52,22 +52,21 @@ From mathcomp Require Import ssrfun seq ssralg generic_quotient.
 (*                             ring  R  represents  a  (right) ideal.  This   *)
 (*                             implies its being a proper_ideal.              *)
 (*                                                                            *)
-(*           MkIdeal idealS == packs   idealS : proper_ideal S   into  an     *)
-(*                             idealr S  interface structure  associating the *)
+(*           MkIdeal idealS == packs idealS : proper_ideal S into an idealr S *)
+(*                             interface structure associating the            *)
 (*                             idealr_closed   property   to  the   canonical *)
 (*                             pred_key S  (see ssrbool), which  must already *)
-(*                             be an zmodPred (see ssralg).                   *)
+(*                             be a zmodPred (see ssralg).                    *)
 (*     MkPrimeIdeal pidealS == packs  pidealS : prime_idealr_closed S  into a *)
 (*                             prime_idealr S interface structure associating *)
 (*                             the  prime_idealr_closed   property   to   the *)
 (*                             canonical pred_key S (see ssrbool), which must *)
 (*                             already be an idealr (see above).              *)
 (*          {ideal_quot kI} == quotient by the keyed (right) ideal predicate  *)
-(*                             kI of a commutative ring R. Note that we indeed*)
-(*                             only provide canonical structures of ring      *)
-(*                             quotients for the case of commutative rings,   *)
-(*                             for which a right ideal is obviously a         *)
-(*                             two-sided ideal.                               *)
+(*                             kI of a commutative ring R. Note that we only  *)
+(*                             provide canonical structures of ring quotients *)
+(*                             for commutative rings, in which a right ideal  *)
+(*                             is obviously a two-sided ideal.                *)
 (*                                                                            *)
 (* Note :                                                                     *)
 (* if (I : pred R) is a predicate over a ring R and (ideal : idealr I) is an  *)
@@ -425,13 +424,13 @@ Notation UnitRingQuotMixin Q mU mV :=
 
 Section IdealDef.
 
-Definition proper_ideal (R : ringType) (S : predPredType R) : Prop :=
+Definition proper_ideal (R : ringType) (S : {pred R}) : Prop :=
   1 \notin S /\ forall a, {in S, forall u, a * u \in S}.
 
-Definition prime_idealr_closed (R : ringType) (S : predPredType R) : Prop :=
+Definition prime_idealr_closed (R : ringType) (S : {pred R}) : Prop :=
   forall u v, u * v \in S -> (u \in S) || (v \in S).
 
-Definition idealr_closed (R : ringType) (S : predPredType R) :=
+Definition idealr_closed (R : ringType) (S : {pred R}) :=
   [/\ 0 \in S, 1 \notin S & forall a, {in S &, forall u v, a * u + v \in S}].
 
 Lemma idealr_closed_nontrivial R S : @idealr_closed R S -> proper_ideal S.
@@ -443,22 +442,22 @@ Proof. by case=> S0 _ hS; split=> // x y xS yS; rewrite -mulN1r addrC hS. Qed.
 Coercion idealr_closedB : idealr_closed >-> zmod_closed.
 Coercion idealr_closed_nontrivial : idealr_closed >-> proper_ideal.
 
-Structure idealr (R : ringType) (S : predPredType R) := MkIdeal {
+Structure idealr (R : ringType) (S : {pred R}) := MkIdeal {
   idealr_zmod :> zmodPred S;
   _ : proper_ideal S
 }.
 
-Structure prime_idealr (R : ringType) (S : predPredType R) := MkPrimeIdeal {
+Structure prime_idealr (R : ringType) (S : {pred R}) := MkPrimeIdeal {
   prime_idealr_zmod :> idealr S;
   _ : prime_idealr_closed S
 }.
 
-Definition Idealr (R : ringType) (I : predPredType R) (zmodI : zmodPred I)
+Definition Idealr (R : ringType) (I : {pred R}) (zmodI : zmodPred I)
             (kI : keyed_pred zmodI) : proper_ideal I -> idealr I.
 Proof. by move=> kI1; split => //. Qed.
 
 Section IdealTheory.
-Variables (R : ringType) (I : predPredType R)
+Variables (R : ringType) (I : {pred R})
           (idealrI : idealr I) (kI : keyed_pred idealrI).
 
 Lemma idealr1 : 1 \in kI = false.
@@ -475,7 +474,7 @@ End IdealTheory.
 
 Section PrimeIdealTheory.
 
-Variables (R : comRingType) (I : predPredType R)
+Variables (R : comRingType) (I : {pred R})
           (pidealrI : prime_idealr I) (kI : keyed_pred pidealrI).
 
 Lemma prime_idealrM u v : (u * v \in kI) = (u \in kI) || (v \in kI).
@@ -490,7 +489,7 @@ End IdealDef.
 
 Module Quotient.
 Section ZmodQuotient.
-Variables (R : zmodType) (I : predPredType R)
+Variables (R : zmodType) (I : {pred R})
           (zmodI : zmodPred I) (kI : keyed_pred zmodI).
 
 Definition equiv (x y : R) := (x - y) \in kI.
@@ -567,7 +566,7 @@ Notation "{quot I }" := (@type_of _ _ _ I (Phant _)).
 
 Section RingQuotient.
 
-Variables (R : comRingType) (I : predPredType R)
+Variables (R : comRingType) (I : {pred R})
           (idealI : idealr I) (kI : keyed_pred idealI).
 
 Local Notation type := {quot kI}.
@@ -618,7 +617,7 @@ End RingQuotient.
 
 Section IDomainQuotient.
 
-Variables (R : comRingType) (I : predPredType R)
+Variables (R : comRingType) (I : {pred R})
           (pidealI : prime_idealr I) (kI : keyed_pred pidealI).
 
 Lemma rquot_IdomainAxiom (x y : {quot kI}): x * y = 0 -> (x == 0) || (y == 0).
diff --git a/mathcomp/algebra/ssralg.v b/mathcomp/algebra/ssralg.v
index 7c74468..d35253c 100644
--- a/mathcomp/algebra/ssralg.v
+++ b/mathcomp/algebra/ssralg.v
@@ -851,7 +851,7 @@ Qed.
 
 Section ClosedPredicates.
 
-Variable S : predPredType V.
+Variable S : {pred V}.
 
 Definition addr_closed := 0 \in S /\ {in S &, forall u v, u + v \in S}.
 Definition oppr_closed := {in S, forall u, - u \in S}.
@@ -1418,7 +1418,7 @@ Canonical converse_ringType := RingType R^c converse_ringMixin.
 
 Section ClosedPredicates.
 
-Variable S : predPredType R.
+Variable S : {pred R}.
 
 Definition mulr_2closed := {in S &, forall u v, u * v \in S}.
 Definition mulr_closed := 1 \in S /\ mulr_2closed.
@@ -1626,7 +1626,7 @@ Proof. exact: big_endo (scalerDr a) (scaler0 a) I r P F. Qed.
 
 Section ClosedPredicates.
 
-Variable S : predPredType V.
+Variable S : {pred V}.
 
 Definition scaler_closed := forall a, {in S, forall v, a *: v \in S}.
 Definition linear_closed := forall a, {in S &, forall u v, a *: u + v \in S}.
@@ -1746,7 +1746,7 @@ Canonical regular_lalgType := LalgType R R^o (@mulrA regular_ringType).
 
 Section ClosedPredicates.
 
-Variable S : predPredType A.
+Variable S : {pred A}.
 
 Definition subalg_closed := [/\ 1 \in S, linear_closed S & mulr_2closed S].
 
@@ -2985,14 +2985,13 @@ Lemma rev_unitrP (x y : R^c) : y * x = 1 /\ x * y = 1 -> x \is a unit.
 Proof. by case=> [yx1 xy1]; apply/unitrP; exists y. Qed.
 
 Definition converse_unitRingMixin :=
-  @UnitRing.Mixin _ ((unit : pred_class) : pred R^c) _
-     mulrV mulVr rev_unitrP invr_out.
+  @UnitRing.Mixin _ (unit : {pred R^c}) _ mulrV mulVr rev_unitrP invr_out.
 Canonical converse_unitRingType := UnitRingType R^c converse_unitRingMixin.
 Canonical regular_unitRingType := [unitRingType of R^o].
 
 Section ClosedPredicates.
 
-Variables S : predPredType R.
+Variables S : {pred R}.
 
 Definition invr_closed := {in S, forall x, x^-1 \in S}.
 Definition divr_2closed := {in S &, forall x y, x / y \in S}.
@@ -3266,7 +3265,7 @@ Qed.
 
 Section ClosedPredicates.
 
-Variables S : predPredType A.
+Variables S : {pred A}.
 
 Definition divalg_closed := [/\ 1 \in S, linear_closed S & divr_2closed S].
 
@@ -3511,7 +3510,7 @@ End DefaultPred.
 
 Section ZmodulePred.
 
-Variables (V : zmodType) (S : predPredType V).
+Variables (V : zmodType) (S : {pred V}).
 
 Section Add.
 
@@ -3580,7 +3579,7 @@ End ZmodulePred.
 
 Section RingPred.
 
-Variables (R : ringType) (S : predPredType R).
+Variables (R : ringType) (S : {pred R}).
 
 Lemma rpredMsign (oppS : opprPred S) (kS : keyed_pred oppS) n x :
   ((-1) ^+ n * x \in kS) = (x \in kS).
@@ -3624,7 +3623,7 @@ End RingPred.
 
 Section LmodPred.
 
-Variables (R : ringType) (V : lmodType R) (S : predPredType V).
+Variables (R : ringType) (V : lmodType R) (S : {pred V}).
 
 Lemma rpredZsign (oppS : opprPred S) (kS : keyed_pred oppS) n u :
   ((-1) ^+ n *: u \in kS) = (u \in kS).
@@ -3645,7 +3644,7 @@ Variable R : unitRingType.
 
 Section Div.
 
-Variables (S : predPredType R) (divS : divrPred S) (kS : keyed_pred divS).
+Variables (S : {pred R}) (divS : divrPred S) (kS : keyed_pred divS).
 
 Lemma rpredVr x : x \in kS -> x^-1 \in kS.
 Proof. by rewrite !keyed_predE; case: divS x. Qed.
@@ -4792,7 +4791,7 @@ Proof. by move=> p; rewrite inE -scaler_nat scaler_eq0 oner_eq0 orbF. Qed.
 
 Section Predicates.
 
-Context (S : pred_class) (divS : @divrPred F S) (kS : keyed_pred divS).
+Context (S : {pred F}) (divS : @divrPred F S) (kS : keyed_pred divS).
 
 Lemma fpredMl x y : x \in kS -> x != 0 -> (x * y \in kS) = (y \in kS).
 Proof. by rewrite -!unitfE; apply: rpredMl. Qed.
@@ -5150,7 +5149,7 @@ Module SubType.
 
 Section Zmodule.
 
-Variables (V : zmodType) (S : predPredType V).
+Variables (V : zmodType) (S : {pred V}).
 Variables (subS : zmodPred S) (kS : keyed_pred subS).
 Variable U : subType (mem kS).
 
@@ -5175,7 +5174,7 @@ End Zmodule.
 
 Section Ring.
 
-Variables (R : ringType) (S : predPredType R).
+Variables (R : ringType) (S : {pred R}).
 Variables (ringS : subringPred S) (kS : keyed_pred ringS).
 
 Definition cast_zmodType (V : zmodType) T (VeqT : V = T :> Type) :=
@@ -5219,7 +5218,7 @@ End Ring.
 
 Section Lmodule.
 
-Variables (R : ringType) (V : lmodType R) (S : predPredType V).
+Variables (R : ringType) (V : lmodType R) (S : {pred V}).
 Variables (linS : submodPred S) (kS : keyed_pred linS).
 Variables (W : subType (mem kS)) (Z : zmodType) (ZeqW : Z = W :> Type).
 
@@ -5265,7 +5264,7 @@ Definition cast_ringType (Q : ringType) T (QeqT : Q = T :> Type) :=
   let cast rQ := let: erefl in _ = T := QeqT return Ring.class_of T in rQ in
   Ring.Pack (cast (Ring.class Q)).
 
-Variables (R : unitRingType) (S : predPredType R).
+Variables (R : unitRingType) (S : {pred R}).
 Variables (ringS : divringPred S) (kS : keyed_pred ringS).
 
 Variables (T : subType (mem kS)) (Q : ringType) (QeqT : Q = T :> Type).
@@ -5279,7 +5278,7 @@ Hypothesis val1 : val (1 : T') = 1.
 Hypothesis valM : {morph (val : T' -> R) : x y / x * y}.
 
 Fact mulVr :
-  {in (unitT : predPredType T'), left_inverse (1 : T') invT (@mul T')}.
+  {in (unitT : {pred T'}), left_inverse (1 : T') invT (@mul T')}.
 Proof. by move=> u Uu; apply: val_inj; rewrite val1 valM SubK mulVr. Qed.
 
 Fact mulrV : {in unitT, right_inverse (1 : T') invT (@mul T')}.
@@ -6249,7 +6248,7 @@ Canonical pair_unitAlgType (R : comUnitRingType) (A1 A2 : unitAlgType R) :=
 (* Testing subtype hierarchy
 Section Test0.
 
-Variables (T : choiceType) (S : predPredType T).
+Variables (T : choiceType) (S : {pred T}).
 
 Inductive B := mkB x & x \in S.
 Definition vB u := let: mkB x _ := u in x.
@@ -6264,7 +6263,7 @@ End Test0.
 
 Section Test1.
 
-Variables (R : unitRingType) (S : pred R).
+Variables (R : unitRingType) (S : {pred R}).
 Variables (ringS : divringPred S) (kS : keyed_pred ringS).
 
 Definition B_zmodMixin := [zmodMixin of B kS by <:].
@@ -6278,7 +6277,7 @@ End Test1.
 
 Section Test2.
 
-Variables (R : comUnitRingType) (A : unitAlgType R) (S : pred A).
+Variables (R : comUnitRingType) (A : unitAlgType R) (S : {pred A}).
 Variables (algS : divalgPred S) (kS : keyed_pred algS).
 
 Definition B_lmodMixin := [lmodMixin of B kS by <:].
@@ -6293,7 +6292,7 @@ End Test2.
 
 Section Test3.
 
-Variables (F : fieldType) (S : pred F).
+Variables (F : fieldType) (S : {pred F}).
 Variables (ringS : divringPred S) (kS : keyed_pred ringS).
 
 Definition B_comRingMixin := [comRingMixin of B kS by <:].
diff --git a/mathcomp/algebra/ssrnum.v b/mathcomp/algebra/ssrnum.v
index 6b2a40a..97afdfb 100644
--- a/mathcomp/algebra/ssrnum.v
+++ b/mathcomp/algebra/ssrnum.v
@@ -1314,8 +1314,7 @@ Proof. by move=> m n; apply: leq_total. Qed.
 
 Section AcrossTypes.
 
-Variable D D' : pred R.
-Variable (f : R -> R').
+Variables (D D' : {pred R}) (f : R -> R').
 
 Lemma ltrW_homo : {homo f : x y / x < y} -> {homo f : x y / x <= y}.
 Proof. exact: homoW. Qed.
@@ -1382,8 +1381,7 @@ End AcrossTypes.
 
 Section NatToR.
 
-Variable D D' : pred nat.
-Variable (f : nat -> R).
+Variables (D D' : {pred nat}) (f : nat -> R).
 
 Lemma ltnrW_homo : {homo f : m n / (m < n)%N >-> m < n} ->
   {homo f : m n / (m <= n)%N >-> m <= n}.
@@ -1471,8 +1469,7 @@ End NatToR.
 
 Section RToNat.
 
-Variable D D' : pred R.
-Variable (f : R -> nat).
+Variables (D D' : {pred R}) (f : R -> nat).
 
 Lemma ltrnW_homo : {homo f : m n / m < n >-> (m < n)%N} ->
   {homo f : m n / m <= n >-> (m <= n)%N}.
@@ -3070,7 +3067,7 @@ Proof. by move=> le_xy; rewrite ltr_neqAle !le_xy andbT. Qed.
 Lemma lerif_nat m n C : (m%:R <= n%:R ?= iff C :> R) = (m <= n ?= iff C)%N.
 Proof. by rewrite /lerif !ler_nat eqr_nat. Qed.
 
-Lemma mono_in_lerif (A : pred R) (f : R -> R) C :
+Lemma mono_in_lerif (A : {pred R}) (f : R -> R) C :
    {in A &, {mono f : x y / x <= y}} ->
   {in A &, forall x y, (f x <= f y ?= iff C) = (x <= y ?= iff C)}.
 Proof.
@@ -3082,7 +3079,7 @@ Lemma mono_lerif (f : R -> R) C :
   forall x y, (f x <= f y ?= iff C) = (x <= y ?= iff C).
 Proof. by move=> mf x y; rewrite /lerif mf (inj_eq (incr_inj _)). Qed.
 
-Lemma nmono_in_lerif (A : pred R) (f : R -> R) C :
+Lemma nmono_in_lerif (A : {pred R}) (f : R -> R) C :
     {in A &, {mono f : x y /~ x <= y}} ->
   {in A &, forall x y, (f x <= f y ?= iff C) = (y <= x ?= iff C)}.
 Proof.
@@ -3183,7 +3180,7 @@ move=> Rx Ry; rewrite sqrrD addrAC (mulrnDr _ 2) -lerif_subLR addrK.
 exact: real_lerif_mean_square_scaled.
 Qed.
 
-Lemma lerif_AGM_scaled (I : finType) (A : pred I) (E : I -> R) (n := #|A|) :
+Lemma lerif_AGM_scaled (I : finType) (A : {pred I}) (E : I -> R) (n := #|A|) :
     {in A, forall i, 0 <= E i *+ n} ->
   \prod_(i in A) (E i *+ n) <= (\sum_(i in A) E i) ^+ n
                             ?= iff [forall i in A, forall j in A, E i == E j].
@@ -3515,7 +3512,7 @@ rewrite mulr_natr (natrX F 2 2) -exprMn divfK ?pnatr_eq0 //.
 exact: real_lerif_AGM2_scaled.
 Qed.
 
-Lemma lerif_AGM (I : finType) (A : pred I) (E : I -> F) :
+Lemma lerif_AGM (I : finType) (A : {pred I}) (E : I -> F) :
     let n := #|A| in let mu := (\sum_(i in A) E i) / n%:R in
     {in A, forall i, 0 <= E i} ->
   \prod_(i in A) E i <= mu ^+ n
@@ -4855,7 +4852,7 @@ Qed.
 
 (* The proper form of the Arithmetic - Geometric Mean inequality. *)
 
-Lemma lerif_rootC_AGM (I : finType) (A : pred I) (n := #|A|) E :
+Lemma lerif_rootC_AGM (I : finType) (A : {pred I}) (n := #|A|) E :
     {in A, forall i, 0 <= E i} ->
   n.-root (\prod_(i in A) E i) <= (\sum_(i in A) E i) / n%:R
                              ?= iff [forall i in A, forall j in A, E i == E j].
diff --git a/mathcomp/algebra/vector.v b/mathcomp/algebra/vector.v
index 48d7d3e..e73ca33 100644
--- a/mathcomp/algebra/vector.v
+++ b/mathcomp/algebra/vector.v
@@ -267,10 +267,10 @@ Definition subsetv U V := (vs2mx U <= vs2mx V)%MS.
 Definition vline u := mx2vs (v2r u).
 
 (* Vspace membership is defined as line inclusion. *)
-Definition pred_of_vspace phV (U : Vector.space phV) : pred_class :=
+Definition pred_of_vspace phV (U : Vector.space phV) : {pred vT} :=
   fun v => (vs2mx (vline v) <= vs2mx U)%MS.
 Canonical vspace_predType :=
-  @mkPredType _ (unkeyed {vspace vT}) (@pred_of_vspace _).
+  @PredType _ (unkeyed {vspace vT}) (@pred_of_vspace _).
 
 Definition fullv : {vspace vT} := mx2vs 1%:M.
 Definition addv U V := mx2vs (vs2mx U + vs2mx V).
@@ -294,7 +294,7 @@ Definition basis_of U X := (span X == U) && free X.
 
 End VspaceDefs.
 
-Coercion pred_of_vspace : Vector.space >-> pred_class.
+Coercion pred_of_vspace : Vector.space >-> pred_sort.
 Notation "\dim U" := (dimv U) : nat_scope.
 Notation "U <= V" := (subsetv U V) : vspace_scope.
 Notation "U <= V <= W" := (subsetv U V && subsetv V W) : vspace_scope.
diff --git a/mathcomp/character/character.v b/mathcomp/character/character.v
index 862e1ba..c2a7ef4 100644
--- a/mathcomp/character/character.v
+++ b/mathcomp/character/character.v
@@ -572,10 +572,10 @@ Lemma irr_of_socleK : cancel irr_of_socle W.
 Proof. by move=> Wi; rewrite /W subrK cast_ordKV enum_rankK. Qed.
 Hint Resolve socle_of_IirrK irr_of_socleK : core.
 
-Lemma irr_of_socle_bij (A : pred (Iirr G)) : {on A, bijective irr_of_socle}.
+Lemma irr_of_socle_bij (A : {pred (Iirr G)}) : {on A, bijective irr_of_socle}.
 Proof. by apply: onW_bij; exists W. Qed.
 
-Lemma socle_of_Iirr_bij (A : pred sG) : {on A, bijective W}.
+Lemma socle_of_Iirr_bij (A : {pred sG}) : {on A, bijective W}.
 Proof. by apply: onW_bij; exists irr_of_socle. Qed.
 
 End IrrClassDef.
diff --git a/mathcomp/character/classfun.v b/mathcomp/character/classfun.v
index 2cf17aa..468aa66 100644
--- a/mathcomp/character/classfun.v
+++ b/mathcomp/character/classfun.v
@@ -1066,7 +1066,7 @@ have [-> | nzV] := eqVneq V 0; first by rewrite cfdot0r !mul0r subrr.
 by rewrite divfK ?cfnorm_eq0 ?subrr.
 Qed.
 
-Lemma map_orthogonal M (nu : 'CF(G) -> 'CF(M)) S R (A : pred 'CF(G)) :
+Lemma map_orthogonal M (nu : 'CF(G) -> 'CF(M)) S R (A : {pred 'CF(G)}) :
   {in A &, isometry nu} -> {subset S <= A} -> {subset R <= A} ->
  orthogonal (map nu S) (map nu R) = orthogonal S R.
 Proof.
@@ -1290,7 +1290,7 @@ Section BuildIsometries.
 
 Variable (gT : finGroupType) (L G : {group gT}).
 Implicit Types (phi psi xi : 'CF(L)) (R S : seq 'CF(L)).
-Implicit Types (U : pred 'CF(L)) (W : pred 'CF(G)).
+Implicit Types (U : {pred 'CF(L)}) (W : {pred 'CF(G)}).
 
 Lemma sub_iso_to U1 U2 W1 W2 tau :
     {subset U2 <= U1} -> {subset W1 <= W2} ->
diff --git a/mathcomp/character/vcharacter.v b/mathcomp/character/vcharacter.v
index 8d7d7e9..4212fbe 100644
--- a/mathcomp/character/vcharacter.v
+++ b/mathcomp/character/vcharacter.v
@@ -47,7 +47,7 @@ Section Basics.
 
 Variables (gT : finGroupType) (B : {set gT}) (S : seq 'CF(B)) (A : {set gT}).
 
-Definition Zchar : pred_class :=
+Definition Zchar : {pred 'CF(B)} :=
   [pred phi in 'CF(B, A) | dec_Cint_span (in_tuple S) phi].
 Fact Zchar_key : pred_key Zchar. Proof. by []. Qed.
 Canonical Zchar_keyed := KeyedPred Zchar_key.
@@ -701,8 +701,8 @@ Qed.
 
 End MoreVchar.
 
-Definition dirr (gT : finGroupType) (B : {set gT}) : pred_class :=  
-  [pred f : 'CF(B) | (f \in irr B) || (- f \in irr B)].
+Definition dirr (gT : finGroupType) (B : {set gT}) : {pred 'CF(B)} :=  
+  [pred f | (f \in irr B) || (- f \in irr B)].
 Arguments dirr {gT}.
 
 Section Norm1vchar.
diff --git a/mathcomp/field/algC.v b/mathcomp/field/algC.v
index 86e9e30..e1fd4d1 100644
--- a/mathcomp/field/algC.v
+++ b/mathcomp/field/algC.v
@@ -554,13 +554,13 @@ Notation algCnumClosedField := numClosedFieldType.
 Notation Creal := (@Num.Def.Rreal numDomainType).
 
 Definition getCrat := let: GetCrat_spec CtoQ _ := getCrat_subproof in CtoQ.
-Definition Crat : pred_class := fun x : algC => ratr (getCrat x) == x.
+Definition Crat : {pred algC} := fun x => ratr (getCrat x) == x.
 
 Definition floorC x := sval (floorC_subproof x).
-Definition Cint : pred_class := fun x : algC => (floorC x)%:~R == x.
+Definition Cint : {pred algC} := fun x => (floorC x)%:~R == x.
 
 Definition truncC x := if x >= 0 then `|floorC x|%N else 0%N.
-Definition Cnat : pred_class := fun x : algC => (truncC x)%:R == x.
+Definition Cnat : {pred algC} := fun x => (truncC x)%:R == x.
 
 Definition minCpoly x : {poly algC} :=
   let: exist2 p _ _ := minCpoly_subproof x in map_poly ratr p.
@@ -573,8 +573,8 @@ Lemma nCdivE (p : nat) : p = p%:R :> divisor. Proof. by []. Qed.
 Lemma zCdivE (p : int) : p = p%:~R :> divisor. Proof. by []. Qed.
 Definition CdivE := (nCdivE, zCdivE).
 
-Definition dvdC (x : divisor) : pred_class :=
-   fun y : algC => if x == 0 then y == 0 else y / x \in Cint.
+Definition dvdC (x : divisor) : {pred algC} :=
+   fun y => if x == 0 then y == 0 else y / x \in Cint.
 Notation "x %| y" := (y \in dvdC x) : C_expanded_scope.
 Notation "x %| y" := (@in_mem divisor y (mem (dvdC x))) : C_scope.
 
@@ -715,7 +715,8 @@ Proof. by move=> _ _ /CintP[m1 ->] /CintP[m2 ->]; rewrite -rmorphM !intCK. Qed.
 Lemma floorCX n : {in Cint, {morph floorC : x / x ^+ n}}.
 Proof. by move=> _ /CintP[m ->]; rewrite -rmorphX !intCK. Qed.
 
-Lemma rpred_Cint S (ringS : subringPred S) (kS : keyed_pred ringS) x :
+Lemma rpred_Cint
+        (S : {pred algC}) (ringS : subringPred S) (kS : keyed_pred ringS) x :
   x \in Cint -> x \in kS.
 Proof. by case/CintP=> m ->; apply: rpred_int. Qed.
 
@@ -805,7 +806,8 @@ Proof. by move=> _ _ /CnatP[n1 ->] /CnatP[n2 ->]; rewrite -natrM !natCK. Qed.
 Lemma truncCX n : {in Cnat, {morph truncC : x / x ^+ n >-> (x ^ n)%N}}.
 Proof. by move=> _ /CnatP[n1 ->]; rewrite -natrX !natCK. Qed.
 
-Lemma rpred_Cnat S (ringS : semiringPred S) (kS : keyed_pred ringS) x :
+Lemma rpred_Cnat
+        (S : {pred algC}) (ringS : semiringPred S) (kS : keyed_pred ringS) x :
   x \in Cnat -> x \in kS.
 Proof. by case/CnatP=> n ->; apply: rpred_nat. Qed.
 
@@ -1110,7 +1112,8 @@ Canonical Crat_subringPred := SubringPred Crat_divring_closed.
 Canonical Crat_sdivrPred := SdivrPred Crat_divring_closed.
 Canonical Crat_divringPred := DivringPred Crat_divring_closed.
 
-Lemma rpred_Crat S (ringS : divringPred S) (kS : keyed_pred ringS) :
+Lemma rpred_Crat
+        (S : {pred algC}) (ringS : divringPred S) (kS : keyed_pred ringS) :
   {subset Crat <= kS}.
 Proof. by move=> _ /CratP[a ->]; apply: rpred_rat. Qed.
 
diff --git a/mathcomp/field/algnum.v b/mathcomp/field/algnum.v
index 144a82e..3f25ae6 100644
--- a/mathcomp/field/algnum.v
+++ b/mathcomp/field/algnum.v
@@ -505,8 +505,7 @@ Qed.
 
 (* Algebraic integers. *)
 
-Definition Aint : pred_class :=
-  fun x : algC => minCpoly x \is a polyOver Cint.
+Definition Aint : {pred algC} := fun x => minCpoly x \is a polyOver Cint.
 Fact Aint_key : pred_key Aint. Proof. by []. Qed.
 Canonical Aint_keyed := KeyedPred Aint_key.
 
@@ -673,8 +672,8 @@ Lemma Aint_aut (nu : {rmorphism algC -> algC}) x :
   (nu x \in Aint) = (x \in Aint).
 Proof. by rewrite !unfold_in minCpoly_aut. Qed.
 
-Definition dvdA (e : Algebraics.divisor) : pred_class :=
-  fun z : algC => if e == 0 then z == 0 else z / e \in Aint.
+Definition dvdA (e : Algebraics.divisor) : {pred algC} :=
+  fun z => if e == 0 then z == 0 else z / e \in Aint.
 Fact dvdA_key e : pred_key (dvdA e). Proof. by []. Qed.
 Canonical dvdA_keyed e := KeyedPred (dvdA_key e).
 Delimit Scope algC_scope with A.
diff --git a/mathcomp/fingroup/fingroup.v b/mathcomp/fingroup/fingroup.v
index 65af825..9399035 100644
--- a/mathcomp/fingroup/fingroup.v
+++ b/mathcomp/fingroup/fingroup.v
@@ -1357,17 +1357,6 @@ Lemma valG : val G = G. Proof. by []. Qed.
 Lemma group1 : 1 \in G. Proof. by case/group_setP: (valP G). Qed.
 Hint Resolve group1 : core.
 
-(* Loads of silly variants to placate the incompleteness of trivial. *)
-(* An alternative would be to upgrade done, pending better support   *)
-(* in the ssreflect ML code.                                         *)
-Notation gTr := (FinGroup.sort gT).
-Notation Gcl := (pred_of_set G : pred gTr).
-Lemma group1_class1 : (1 : gTr) \in G. Proof. by []. Qed.
-Lemma group1_class2 : 1 \in Gcl. Proof. by []. Qed.
-Lemma group1_class12 : (1 : gTr) \in Gcl. Proof. by []. Qed.
-Lemma group1_eqType : (1 : gT : eqType) \in G. Proof. by []. Qed.
-Lemma group1_finType : (1 : gT : finType) \in G. Proof. by []. Qed.
-
 Lemma group1_contra x : x \notin G -> x != 1.
 Proof. by apply: contraNneq => ->. Qed.
 
@@ -1385,14 +1374,6 @@ Lemma repr_group : repr G = 1. Proof. by rewrite /repr group1. Qed.
 
 Lemma cardG_gt0 : 0 < #|G|.
 Proof. by rewrite lt0n; apply/existsP; exists (1 : gT). Qed.
-(* Workaround for the fact that the simple matching used by Trivial does not  *)
-(* always allow conversion. In particular cardG_gt0 always fails to apply to  *)
-(* subgoals that have been simplified (by /=) because type inference in the   *)
-(* notation #|G| introduces redexes of the form                               *)
-(*    Finite.sort (arg_finGroupType (FinGroup.base gT))                       *)
-(* which get collapsed to Fingroup.arg_sort (FinGroup.base gT).               *)
-Definition cardG_gt0_reduced : 0 < card (@mem gT (predPredType gT) G)
-  := cardG_gt0.
 
 Lemma indexg_gt0 A : 0 < #|G : A|.
 Proof.
@@ -1839,9 +1820,9 @@ Qed.
 
 End GroupProp.
 
-Hint Resolve group1 group1_class1 group1_class12 group1_class12 : core.
-Hint Resolve group1_eqType group1_finType : core.
-Hint Resolve cardG_gt0 cardG_gt0_reduced indexg_gt0 : core.
+Hint Extern 0 (is_true (1%g \in _)) => apply: group1 : core.
+Hint Extern 0 (is_true (0 < #|_|)) => apply: cardG_gt0 : core.
+Hint Extern 0 (is_true (0 < #|_ : _|)) => apply: indexg_gt0 : core.
 
 Notation "G :^ x" := (conjG_group G x) : Group_scope.
 
@@ -3005,7 +2986,8 @@ Notation "''C_' G [ x ]" := (setI_group G 'C[x]) : Group_scope.
 Notation "''C_' ( G ) [ x ]" := (setI_group G 'C[x])
   (only parsing) : Group_scope.
 
-Hint Resolve normG normal_refl : core.
+Hint Extern 0 (is_true (_ \subset _)) => apply: normG : core.
+Hint Extern 0 (is_true (_ <| _)) => apply: normal_refl : core.
 
 Section MinMaxGroup.
 
diff --git a/mathcomp/solvable/gfunctor.v b/mathcomp/solvable/gfunctor.v
index 31ffded..3417d84 100644
--- a/mathcomp/solvable/gfunctor.v
+++ b/mathcomp/solvable/gfunctor.v
@@ -266,7 +266,7 @@ Variable F : GFunctor.iso_map.
 Lemma gFsub gT (G : {group gT}) : F gT G \subset G.
 Proof. by case: F gT G. Qed.
 
-Lemma gFsub_trans gT (G : {group gT}) (A : pred_class) :
+Lemma gFsub_trans gT (G : {group gT}) (A : {pred gT}) :
   G \subset A -> F gT G \subset A.
 Proof. exact/subset_trans/gFsub. Qed.
 
@@ -297,7 +297,7 @@ Proof. exact/char_trans/gFchar. Qed.
 Lemma gFnormal_trans gT (G H : {group gT}) : H <| G -> F gT H <| G.
 Proof. exact/char_normal_trans/gFchar. Qed.
 
-Lemma gFnorm_trans gT (A : pred_class) (G : {group gT}) :
+Lemma gFnorm_trans gT (A : {pred gT}) (G : {group gT}) :
   A \subset 'N(G) -> A \subset 'N(F gT G).
 Proof. by move/subset_trans/(_ (gFnorms G)). Qed.
 
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..bcb163c 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,18 +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|)
+Notation "\p 'i' ( A )" := \pi(#|A|) 
   (at level 2, format "\p 'i' ( A )") : 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].