From 94f1cb115b791a36ee660e94bf086e1638acbb88 Mon Sep 17 00:00:00 2001
From: Vincent Laporte
Date: Thu, 14 Mar 2019 10:34:46 +0000
Subject: [Stdlib] OrderedType: do not pollute the “core” hint database

---
 test-suite/bugs/opened/bug_1596.v | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

(limited to 'test-suite/bugs/opened')

diff --git a/test-suite/bugs/opened/bug_1596.v b/test-suite/bugs/opened/bug_1596.v
index 820022d995..27cb731151 100644
--- a/test-suite/bugs/opened/bug_1596.v
+++ b/test-suite/bugs/opened/bug_1596.v
@@ -69,9 +69,8 @@ Definition t := (X.t * Y.t)%type.
     elim (X.lt_not_eq H2 H3).
     elim H0;clear H0;intros.
     right.
-    split.
-    eauto.
-    eauto.
+    split;
+    eauto with ordered_type.
   Qed.
 
   Lemma lt_not_eq : forall (x y:t),(lt x y)->~(eq x y).
@@ -97,7 +96,7 @@ Definition t := (X.t * Y.t)%type.
     apply EQ.
     split;trivial.
     apply GT.
-    right;auto.
+    right;auto with ordered_type.
     apply GT.
     left;trivial.
   Defined.
-- 
cgit v1.2.3