From 8860362de4a26286b0cb20cf4e02edc5209bdbd1 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Thu, 1 Oct 2015 23:35:51 +0200 Subject: Univs: Change intf of push_named_def to return the computed universe context Let-bound definitions can be opaque but the whole universe context was not gathered to be discharged at section closing time. --- kernel/safe_typing.ml | 17 +++++++++-------- kernel/safe_typing.mli | 5 ++++- library/declare.ml | 6 +++--- library/global.ml | 2 +- library/global.mli | 2 +- 5 files changed, 18 insertions(+), 14 deletions(-) diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 4299f729d..9329b1686 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -338,17 +338,18 @@ let safe_push_named (id,_,_ as d) env = let push_named_def (id,de) senv = let c,typ,univs = Term_typing.translate_local_def senv.env id de in - let senv' = push_context de.Entries.const_entry_polymorphic univs senv in - let c, senv' = match c with - | Def c -> Mod_subst.force_constr c, senv' + let poly = de.Entries.const_entry_polymorphic in + let univs = Univ.ContextSet.of_context univs in + let c, univs = match c with + | Def c -> Mod_subst.force_constr c, univs | OpaqueDef o -> - Opaqueproof.force_proof (Environ.opaque_tables senv'.env) o, - push_context_set de.Entries.const_entry_polymorphic - (Opaqueproof.force_constraints (Environ.opaque_tables senv'.env) o) - senv' + Opaqueproof.force_proof (Environ.opaque_tables senv.env) o, + Univ.ContextSet.union univs + (Opaqueproof.force_constraints (Environ.opaque_tables senv.env) o) | _ -> assert false in + let senv' = push_context_set poly univs senv in let env'' = safe_push_named (id,Some c,typ) senv'.env in - {senv' with env=env''} + univs, {senv' with env=env''} let push_named_assum ((id,t,poly),ctx) senv = let senv' = push_context_set poly ctx senv in diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index b971a1bd4..eac08eb83 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -59,8 +59,11 @@ val is_joined_environment : safe_environment -> bool val push_named_assum : (Id.t * Term.types * bool (* polymorphic *)) Univ.in_universe_context_set -> safe_transformer0 + +(** Returns the full universe context necessary to typecheck the definition + (futures are forced) *) val push_named_def : - Id.t * Entries.definition_entry -> safe_transformer0 + Id.t * Entries.definition_entry -> Univ.universe_context_set safe_transformer (** Insertion of global axioms or definitions *) diff --git a/library/declare.ml b/library/declare.ml index ec0e1047e..16803b3bf 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -54,9 +54,9 @@ let cache_variable ((sp,_),o) = let impl = if impl then Implicit else Explicit in impl, true, poly, ctx | SectionLocalDef (de) -> - let () = Global.push_named_def (id,de) in - Explicit, de.const_entry_opaque, de.const_entry_polymorphic, - (Univ.ContextSet.of_context de.const_entry_universes) in + let univs = Global.push_named_def (id,de) in + Explicit, de.const_entry_opaque, + de.const_entry_polymorphic, univs in Nametab.push (Nametab.Until 1) (restrict_path 0 sp) (VarRef id); add_section_variable id impl poly ctx; Dischargedhypsmap.set_discharged_hyps sp []; diff --git a/library/global.ml b/library/global.ml index 382abb846..6002382c1 100644 --- a/library/global.ml +++ b/library/global.ml @@ -78,7 +78,7 @@ let globalize_with_summary fs f = let i2l = Label.of_id let push_named_assum a = globalize0 (Safe_typing.push_named_assum a) -let push_named_def d = globalize0 (Safe_typing.push_named_def d) +let push_named_def d = globalize (Safe_typing.push_named_def d) let add_constraints c = globalize0 (Safe_typing.add_constraints c) let push_context_set b c = globalize0 (Safe_typing.push_context_set b c) let push_context b c = globalize0 (Safe_typing.push_context b c) diff --git a/library/global.mli b/library/global.mli index e6b5c1cba..ac231f7fd 100644 --- a/library/global.mli +++ b/library/global.mli @@ -31,7 +31,7 @@ val set_engagement : Declarations.engagement -> unit (** Variables, Local definitions, constants, inductive types *) val push_named_assum : (Id.t * Constr.types * bool) Univ.in_universe_context_set -> unit -val push_named_def : (Id.t * Entries.definition_entry) -> unit +val push_named_def : (Id.t * Entries.definition_entry) -> Univ.universe_context_set val add_constant : DirPath.t -> Id.t -> Safe_typing.global_declaration -> constant -- cgit v1.2.3