From 78edfe09f34db4a28fb41a1f6fd3bb4922d09ec8 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 29 Oct 2015 15:09:14 -0400
Subject: Collect subproof universes in handle_side_effects.

---
 kernel/safe_typing.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'kernel')

diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 97b74cadb9..e0a07dcc3a 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -254,7 +254,9 @@ let universes_of_private eff =
           if cb.const_polymorphic then acc
           else (Univ.ContextSet.of_context cb.const_universes) :: acc)
         acc l
-     | Entries.SEsubproof _ -> acc)
+     | Entries.SEsubproof (c, cb, e) ->
+	if cb.const_polymorphic then acc
+	else Univ.ContextSet.of_context cb.const_universes :: acc)
    [] eff
 
 let env_of_safe_env senv = senv.env
-- 
cgit v1.2.3