diff options
| author | Pierre-Marie Pédrot | 2019-05-13 00:03:36 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-05-14 20:19:37 +0200 |
| commit | e74fce3090323b4d3734f84ee8cf6dc1f5e85953 (patch) | |
| tree | 4c738543dd88e68759fe9c198f0c48d12e73c4e4 /kernel/safe_typing.mli | |
| parent | 106a7c4a86e4c164a73cbc5a4c14f3c4ff527f30 (diff) | |
Abstract away the implementation of side-effects in Safe_typing.
Diffstat (limited to 'kernel/safe_typing.mli')
| -rw-r--r-- | kernel/safe_typing.mli | 8 |
1 files changed, 3 insertions, 5 deletions
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index 46c97c1fb8..6fcdef9a10 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -43,11 +43,6 @@ type 'a safe_transformer = safe_environment -> 'a * safe_environment type private_constants -val side_effects_of_private_constants : - private_constants -> Entries.side_eff list -(** Return the list of individual side-effects in the order of their - creation. *) - val empty_private_constants : private_constants val concat_private : private_constants -> private_constants -> private_constants (** [concat_private e1 e2] adds the constants of [e1] to [e2], i.e. constants in @@ -62,6 +57,9 @@ val inline_private_constants_in_constr : val inline_private_constants_in_definition_entry : Environ.env -> private_constants Entries.definition_entry -> unit Entries.definition_entry +val push_private_constants : Environ.env -> private_constants -> Environ.env +(** Push the constants in the environment if not already there. *) + val universes_of_private : private_constants -> Univ.ContextSet.t list val is_curmod_library : safe_environment -> bool |