From 6be8fd5c67949a59bde7083e81401263986e7a4e Mon Sep 17 00:00:00 2001
From: Georges Gonthier
Date: Sun, 28 Apr 2019 20:37:17 +0200
Subject: 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`).
---
 mathcomp/character/classfun.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'mathcomp/character/classfun.v')

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} ->
-- 
cgit v1.2.3