From a1d6232019dd903419b0ac10819dfde6759c45d1 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 31 Dec 2015 19:32:31 +0100
Subject: Fix bug #4456, anomaly in handle-side effects

The side-effects can contain universe declarations needed to typecheck
later proofs, which weren't added to the env used to typecheck them.
---
 kernel/term_typing.ml | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

(limited to 'kernel')

diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index a566028d40..74c2e7da37 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -424,7 +424,10 @@ let export_side_effects mb env ce =
       let trusted = check_signatures mb signatures in
       let push_seff env = function
         | kn, cb, `Nothing, _ ->
-            Environ.add_constant kn cb env
+           let env = Environ.add_constant kn cb env in
+	   if not cb.const_polymorphic then
+	     Environ.push_context ~strict:true cb.const_universes env
+	   else env
         | kn, cb, `Opaque(_, ctx), _ -> 
             let env = Environ.add_constant kn cb env in
             Environ.push_context_set
-- 
cgit v1.2.3


From bb9acba7cfe83ba3a5116b0e7aa78ac7f1219f60 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Mon, 4 Jan 2016 16:55:44 +0100
Subject: Fix handling of side-effects in case of `Opaque side-effects as well.

---
 kernel/term_typing.ml | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

(limited to 'kernel')

diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 74c2e7da37..aa60432a7e 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -429,9 +429,11 @@ let export_side_effects mb env ce =
 	     Environ.push_context ~strict:true cb.const_universes env
 	   else env
         | kn, cb, `Opaque(_, ctx), _ -> 
-            let env = Environ.add_constant kn cb env in
-            Environ.push_context_set
-              ~strict:(not cb.const_polymorphic) ctx env in
+           let env = Environ.add_constant kn cb env in
+	   if not cb.const_polymorphic then
+	     let env = Environ.push_context ~strict:true cb.const_universes env in
+             Environ.push_context_set ~strict:true ctx env
+	   else env in
       let rec translate_seff sl seff acc env =
         match sl, seff with
         | _, [] -> List.rev acc, ce
-- 
cgit v1.2.3