diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/safe_typing.mli | 7 | ||||
| -rw-r--r-- | kernel/term_typing.mli | 5 |
2 files changed, 12 insertions, 0 deletions
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index 8bc47d6ce0..efeb98bd25 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 diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli index 5330fb32ba..075389ea53 100644 --- a/kernel/term_typing.mli +++ b/kernel/term_typing.mli @@ -34,7 +34,12 @@ val inline_entry_side_effects : val empty_seff : side_effects val add_seff : side_effect -> side_effects -> side_effects val concat_seff : side_effects -> side_effects -> side_effects +(** [concat_seff e1 e2] adds the side-effects of [e1] to [e2], i.e. effects in + [e1] must be more recent than those of [e2]. *) val uniq_seff : side_effects -> side_effect list +(** Return the list of individual side-effects in the order of their + creation. *) + val equal_eff : side_effect -> side_effect -> bool val translate_constant : |