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/term_typing.mli | |
| parent | ee1546dc6686e888cc8da5f9442bcf788544dd0e (diff) | |
Documenting the API of side-effects.
Diffstat (limited to 'kernel/term_typing.mli')
| -rw-r--r-- | kernel/term_typing.mli | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli index 5330fb32b..075389ea5 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 : |