diff options
Diffstat (limited to 'kernel/term_typing.ml')
| -rw-r--r-- | kernel/term_typing.ml | 27 |
1 files changed, 16 insertions, 11 deletions
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 35fa871b4e..f9fdbdd68e 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -88,6 +88,7 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = Cooking.cook_body = Undef nl; cook_type = t; cook_universes = univs; + cook_private_univs = None; cook_inline = false; cook_context = ctx; } @@ -130,6 +131,7 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = Cooking.cook_body = def; cook_type = typ; cook_universes = Monomorphic_const univs; + cook_private_univs = None; cook_inline = c.const_entry_inline_code; cook_context = c.const_entry_secctx; } @@ -145,24 +147,25 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = 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 + let env, usubst, univs, private_univs = match c.const_entry_universes with | Monomorphic_const_entry univs -> let ctx = Univ.ContextSet.union univs ctx in let env = push_context_set ~strict:true ctx env in - env, Univ.empty_level_subst, Monomorphic_const ctx + env, Univ.empty_level_subst, Monomorphic_const ctx, None | Polymorphic_const_entry (nas, uctx) -> - (** Ensure not to generate internal constraints in polymorphic mode. - The only way for this to happen would be that either the body - contained deferred universes, or that it contains monomorphic - side-effects. The first property is ruled out by upper layers, - and the second one is ensured by the fact we currently - unconditionally export side-effects from polymorphic definitions, - i.e. [trust] is always [Pure]. *) - let () = assert (Univ.ContextSet.is_empty ctx) in + (** [ctx] must contain local universes, such that it has no impact + on the rest of the graph (up to transitivity). *) let env = push_context ~strict:false uctx env in let sbst, auctx = Univ.abstract_universes nas uctx in let sbst = Univ.make_instance_subst sbst in - env, sbst, Polymorphic_const auctx + let env, local = + if opaque then + push_subgraph ctx env, Some (on_snd (Univ.subst_univs_level_constraints sbst) ctx) + else + if Univ.ContextSet.is_empty ctx then env, None + else CErrors.anomaly Pp.(str "Local universes in non-opaque polymorphic definition.") + in + env, sbst, Polymorphic_const auctx, local in let j = infer env body in let typ = match typ with @@ -183,6 +186,7 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = Cooking.cook_body = def; cook_type = typ; cook_universes = univs; + cook_private_univs = private_univs; cook_inline = c.const_entry_inline_code; cook_context = c.const_entry_secctx; } @@ -277,6 +281,7 @@ let build_constant_declaration _kn env result = const_type = typ; const_body_code = tps; const_universes = univs; + const_private_poly_univs = result.cook_private_univs; const_inline_code = result.cook_inline; const_typing_flags = Environ.typing_flags env } |