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.

---
 proofs/proof_global.ml        | 3 ++-
 test-suite/bugs/closed/4363.v | 7 +++++++
 2 files changed, 9 insertions(+), 1 deletion(-)
 create mode 100644 test-suite/bugs/closed/4363.v

diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 3d60ff217a..3edd34e5f6 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -333,7 +333,8 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now fpl =
           (* For vi2vo compilation proofs are computed now but we need to
            * complement the univ constraints of the typ with the ones of
            * the body.  So we keep the two sets distinct. *)
-          let ctx_body = restrict_universe_context ctx used_univs_body in
+	  let used_univs = Univ.LSet.union used_univs_body used_univs_typ in
+          let ctx_body = restrict_universe_context ctx used_univs in
           (initunivs, typ), ((body, ctx_body), eff)
         else
           let initunivs = Univ.UContext.empty in
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