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/algebra/vector.v | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'mathcomp/algebra/vector.v')

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