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/solvable/gfunctor.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'mathcomp/solvable')

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