diff options
| author | Pierre-Marie Pédrot | 2018-09-21 13:22:01 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-10-19 13:54:47 +0200 |
| commit | d24125537710202cc15a8d6a7352072bd6c77cba (patch) | |
| tree | 7f61942976af89fc074c673f8593784f10331fef /kernel/term_typing.ml | |
| parent | eba0e54f6ecef38b451ef84a978b9ab55699ccf8 (diff) | |
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.
Diffstat (limited to 'kernel/term_typing.ml')
| -rw-r--r-- | kernel/term_typing.ml | 9 |
1 files changed, 5 insertions, 4 deletions
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 -> |