From d24125537710202cc15a8d6a7352072bd6c77cba Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 21 Sep 2018 13:22:01 +0200
Subject: Explicitly merge contexts in side-effect universe handling.

Instead of threading the universe state and making it grow, we make clear
in the signature that the differed side-effects generate constraints to be
added.
---
 kernel/term_typing.ml | 9 +++++----
 1 file changed, 5 insertions(+), 4 deletions(-)

(limited to 'kernel/term_typing.ml')

diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 644f07adfa..fb1b3e236c 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -28,7 +28,7 @@ module NamedDecl = Context.Named.Declaration
 (* Insertion of constants and parameters in environment. *)
 
 type 'a effect_handler =
-  env -> Constr.t -> Univ.ContextSet.t -> 'a -> (Constr.t * Univ.ContextSet.t * int)
+  env -> Constr.t -> 'a -> (Constr.t * Univ.ContextSet.t * int)
 
 type _ trust =
 | Pure : unit trust
@@ -113,7 +113,8 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
             let _ = judge_of_cast env j DEFAULTcast tyj in
             j, uctx
           | SideEffects handle ->
-            let (body, uctx, valid_signatures) = handle env body uctx side_eff in
+            let (body, uctx', valid_signatures) = handle env body side_eff in
+            let uctx = Univ.ContextSet.union uctx uctx' in
             let env = push_context_set uctx env in
             let body,env,ectx = skip_trusted_seff valid_signatures body env in
             let j = infer env body in
@@ -141,8 +142,8 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
       let body, ctx = match trust with
       | Pure -> body, ctx
       | SideEffects handle ->
-        let body, ctx, _ = handle env body ctx side_eff in
-        body, ctx
+        let body, ctx', _ = handle env body side_eff in
+        body, Univ.ContextSet.union ctx ctx'
       in
       let env, usubst, univs = match c.const_entry_universes with
       | Monomorphic_const_entry univs ->
-- 
cgit v1.2.3