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.

1 files changed, 4 insertions, 1 deletions

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