diff options
| author | Kazuhiko Sakaguchi | 2019-04-18 15:06:18 +0200 |
|---|---|---|
| committer | Kazuhiko Sakaguchi | 2019-04-18 16:22:48 +0200 |
| commit | 10e688f72239e75fbe8d8ea0c84c468569f49a96 (patch) | |
| tree | 02949d8d9f505274784b834ecb1f89844b035598 /mathcomp/algebra | |
| parent | 4e33a068c5451a37d36d94714c966232bc130626 (diff) | |
Remove unused `Require`s and a hint directive from interval.v
Diffstat (limited to 'mathcomp/algebra')
| -rw-r--r-- | mathcomp/algebra/interval.v | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/mathcomp/algebra/interval.v b/mathcomp/algebra/interval.v index 3ef444c..41767e1 100644 --- a/mathcomp/algebra/interval.v +++ b/mathcomp/algebra/interval.v @@ -4,7 +4,7 @@ Require Import mathcomp.ssreflect.ssreflect. From mathcomp Require Import ssrfun ssrbool eqtype ssrnat seq div choice fintype. From mathcomp -Require Import bigop ssralg finset fingroup zmodp ssrint ssrnum. +Require Import bigop ssralg finset fingroup ssrnum. (*****************************************************************************) (* This file provide support for intervals in numerical and real domains. *) @@ -471,7 +471,6 @@ move=> x [[[] a|] [[] b|]] /itv_dec // [? ?]; | rewrite (@ler_lt_trans _ x) // 1?ltrW ]. Qed. -Hint Rewrite intP : core. Arguments itvP [x i]. Definition itv_intersection (x y : interval R) : interval R := |