diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-03-20 08:48:22 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-03-23 16:33:26 +0100 |
| commit | 91dbe4af7b2a435142dcf40902082f90f07cc8be (patch) | |
| tree | aaae79d684fa71882f9dd4ad1c7a592b29c0cbff /kernel/safe_typing.mli | |
| parent | ee1546dc6686e888cc8da5f9442bcf788544dd0e (diff) | |
Documenting the API of side-effects.
Diffstat (limited to 'kernel/safe_typing.mli')
| -rw-r--r-- | kernel/safe_typing.mli | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index 8bc47d6ce..efeb98bd2 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -48,10 +48,17 @@ type private_constant_role = val side_effects_of_private_constants : private_constants -> Entries.side_effect list +(** Return the list of individual side-effects in the order of their + creation. *) val empty_private_constants : private_constants val add_private : private_constant -> private_constants -> private_constants +(** Add a constant to a list of private constants. The former must be more + recent than all constants appearing in the latter, i.e. one should not + create a dependency cycle. *) val concat_private : private_constants -> private_constants -> private_constants +(** [concat_private e1 e2] adds the constants of [e1] to [e2], i.e. constants in + [e1] must be more recent than those of [e2]. *) val private_con_of_con : safe_environment -> constant -> private_constant val private_con_of_scheme : kind:string -> safe_environment -> (inductive * constant) list -> private_constant |