diff options
| author | Cyril Cohen | 2019-04-23 08:43:09 +0200 |
|---|---|---|
| committer | GitHub | 2019-04-23 08:43:09 +0200 |
| commit | 5118bc30e1748dd58ddf30889c69502e9366f2d9 (patch) | |
| tree | 02949d8d9f505274784b834ecb1f89844b035598 | |
| parent | 05c18a013e26d29473d70ec4aa978fc8f58d1002 (diff) | |
| parent | 10e688f72239e75fbe8d8ea0c84c468569f49a96 (diff) | |
Merge pull request #332 from pi8027/zmodp-interval
Remove unused `Require`s and a hint directive from interval.v
| -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 := |