diff options
| author | Pierre-Marie Pédrot | 2019-09-26 11:14:48 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-09-26 15:29:41 +0200 |
| commit | 92006b6cc6b49ed6f892a7e5475f32ca852a9769 (patch) | |
| tree | 7884eb1bbb64981b7545fffcb8cb3f604f8a8561 /library | |
| parent | 884b413e91d293a6b2009da11f2996db0654e40f (diff) | |
Implement section discharging inside kernel.
This patch is minimalistic, insofar as it is only untying the dependency
loop between Declare and Safe_typing. Nonetheless, it is already quite
big, thus we will polish it afterwards.
Diffstat (limited to 'library')
| -rw-r--r-- | library/global.ml | 12 | ||||
| -rw-r--r-- | library/global.mli | 1 |
2 files changed, 6 insertions, 7 deletions
diff --git a/library/global.ml b/library/global.ml index 3d28178d7b..315a147d2c 100644 --- a/library/global.ml +++ b/library/global.ml @@ -71,6 +71,11 @@ let globalize0 f = GlobalSafeEnv.set_safe_env (f (safe_env ())) let globalize f = let res,env = f (safe_env ()) in GlobalSafeEnv.set_safe_env env; res +let globalize0_with_summary fs f = + let env = f (safe_env ()) in + Summary.unfreeze_summaries fs; + GlobalSafeEnv.set_safe_env env + let globalize_with_summary fs f = let res,env = f (safe_env ()) in Summary.unfreeze_summaries fs; @@ -99,18 +104,13 @@ let set_allow_sprop b = globalize0 (Safe_typing.set_allow_sprop b) let sprop_allowed () = Environ.sprop_allowed (env()) let export_private_constants ~in_section cd = globalize (Safe_typing.export_private_constants ~in_section cd) let add_constant ~side_effect ~in_section id d = globalize (Safe_typing.add_constant ~side_effect ~in_section (i2l id) d) -let add_recipe ~in_section id d = globalize (Safe_typing.add_recipe ~in_section (i2l id) d) let add_mind id mie = globalize (Safe_typing.add_mind (i2l id) mie) let add_modtype id me inl = globalize (Safe_typing.add_modtype (i2l id) me inl) let add_module id me inl = globalize (Safe_typing.add_module (i2l id) me inl) let add_include me ismod inl = globalize (Safe_typing.add_include me ismod inl) let open_section ~poly = globalize0 (Safe_typing.open_section ~poly) -let close_section fs = - (* TODO: use globalize0_with_summary *) - Summary.unfreeze_summaries fs; - let env = Safe_typing.close_section (safe_env ()) in - GlobalSafeEnv.set_safe_env env +let close_section fs = globalize0_with_summary fs Safe_typing.close_section let start_module id = globalize (Safe_typing.start_module (i2l id)) let start_modtype id = globalize (Safe_typing.start_modtype (i2l id)) diff --git a/library/global.mli b/library/global.mli index b809e9b241..26ccb90271 100644 --- a/library/global.mli +++ b/library/global.mli @@ -52,7 +52,6 @@ val export_private_constants : in_section:bool -> val add_constant : side_effect:'a Safe_typing.effect_entry -> in_section:bool -> Id.t -> Safe_typing.global_declaration -> Constant.t * 'a -val add_recipe : in_section:bool -> Id.t -> Cooking.recipe -> Constant.t val add_mind : Id.t -> Entries.mutual_inductive_entry -> MutInd.t |