From ee02c17a2e8a10c4f6f6b47e8875f2f9b1a3d42f Mon Sep 17 00:00:00 2001
From: Vincent Laporte
Date: Fri, 25 Jan 2019 13:01:21 +0000
Subject: [stdlib] Do not put INR_eq in the “real” hint database

---
 theories/Reals/RIneq.v | 1 -
 1 file changed, 1 deletion(-)

(limited to 'theories')

diff --git a/theories/Reals/RIneq.v b/theories/Reals/RIneq.v
index 75298855b2..3b108b485a 100644
--- a/theories/Reals/RIneq.v
+++ b/theories/Reals/RIneq.v
@@ -1692,7 +1692,6 @@ Proof.
   exact H.
   now apply not_INR in H.
 Qed.
-Hint Resolve INR_eq: real.
 
 Lemma INR_le : forall n m:nat, INR n <= INR m -> (n <= m)%nat.
 Proof.
-- 
cgit v1.2.3