From 3c81c6c3b595ef06e0c01e51775aa0118f44e421 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Fri, 11 Dec 2015 17:59:42 +0100
Subject: Univs: Fix bug #4363, nested abstract.

---
 test-suite/bugs/closed/4363.v | 7 +++++++
 1 file changed, 7 insertions(+)
 create mode 100644 test-suite/bugs/closed/4363.v

(limited to 'test-suite/bugs')

diff --git a/test-suite/bugs/closed/4363.v b/test-suite/bugs/closed/4363.v
new file mode 100644
index 0000000000..75a9c9a041
--- /dev/null
+++ b/test-suite/bugs/closed/4363.v
@@ -0,0 +1,7 @@
+Set Printing Universes.
+Definition foo : Type.
+Proof.
+  assert (H : Set) by abstract (assert Type by abstract exact Type using bar; exact nat).
+  exact bar.
+Defined. (* Toplevel input, characters 0-8:
+Error:
\ No newline at end of file
-- 
cgit v1.2.3


From 9329cb508f336b48a2bf2e699886546158b6b4d8 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Mon, 14 Dec 2015 11:14:45 +0100
Subject: Test file for #4363 was not complete.

---
 test-suite/bugs/closed/4363.v | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'test-suite/bugs')

diff --git a/test-suite/bugs/closed/4363.v b/test-suite/bugs/closed/4363.v
index 75a9c9a041..9895548c1d 100644
--- a/test-suite/bugs/closed/4363.v
+++ b/test-suite/bugs/closed/4363.v
@@ -4,4 +4,6 @@ Proof.
   assert (H : Set) by abstract (assert Type by abstract exact Type using bar; exact nat).
   exact bar.
 Defined. (* Toplevel input, characters 0-8:
-Error:
\ No newline at end of file
+Error:
+The term "(fun _ : Set => bar) foo_subproof" has type
+"Type@{Top.2}" while it is expected to have type "Type@{Top.1}". *)
-- 
cgit v1.2.3