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

3 files changed, 7 insertions, 7 deletions

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.