From 91dbe4af7b2a435142dcf40902082f90f07cc8be Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 20 Mar 2017 08:48:22 +0100 Subject: Documenting the API of side-effects. --- kernel/safe_typing.mli | 7 +++++++ 1 file changed, 7 insertions(+) (limited to 'kernel/safe_typing.mli') 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 -- cgit v1.2.3