From 2bcae5b7a22019718973f65cafd271f735d3d85b Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau <mattam@mattam.org>
Date: Tue, 11 Oct 2016 16:33:26 +0200
Subject: Fix test-suite file 5123 to fail in case of regression

---
 test-suite/bugs/closed/5123.v | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/test-suite/bugs/closed/5123.v b/test-suite/bugs/closed/5123.v
index c171a10d1..bcde510ee 100644
--- a/test-suite/bugs/closed/5123.v
+++ b/test-suite/bugs/closed/5123.v
@@ -21,6 +21,7 @@ Goal True.
   unshelve opose (@vect_sigT_eqdec _ _ _ _) as H.
   all:cycle 2.
   eapply existT. (*BUG: Why does this do typeclass resolution in the evar?*)
+  Focus 5.
 Abort.
 
 Goal True.
@@ -28,4 +29,5 @@ Goal True.
   Unshelve.
   all:cycle 3.
   eapply existT. (*This does no typeclass resultion, which is correct.*)
+  Focus 5.
 Abort.
\ No newline at end of file
-- 
cgit v1.2.3