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`).

7 files changed, 63 insertions, 66 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.