From be428c80f7be97b80e7e1e58d195a26465407915 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Tue, 8 Apr 2014 16:58:52 +0200
Subject: Refresh some universes in cases.ml as they might appear in the term.

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

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/2615.v b/test-suite/bugs/closed/2615.v
index 54e1a07cc8..dde6a6a5ed 100644
--- a/test-suite/bugs/closed/2615.v
+++ b/test-suite/bugs/closed/2615.v
@@ -12,3 +12,5 @@ Fail induction 1.
 refine (fun p => match p with _ => _ end).
 Undo.
 refine (fun p => match p with foo_intro _ _ => _ end).
+admit.
+Qed.
\ No newline at end of file
-- 
cgit v1.2.3