diff options
Diffstat (limited to 'mathcomp/algebra/interval.v')
| -rw-r--r-- | mathcomp/algebra/interval.v | 2 |
1 files changed, 1 insertions, 1 deletions
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 := |