From 10e688f72239e75fbe8d8ea0c84c468569f49a96 Mon Sep 17 00:00:00 2001
From: Kazuhiko Sakaguchi
Date: Thu, 18 Apr 2019 15:06:18 +0200
Subject: Remove unused `Require`s and a hint directive from interval.v

---
 mathcomp/algebra/interval.v | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'mathcomp')

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