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/interval.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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

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