diff options
Diffstat (limited to 'kernel/term_typing.mli')
| -rw-r--r-- | kernel/term_typing.mli | 12 |
1 files changed, 11 insertions, 1 deletions
diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli index 89b5fc40e..075389ea5 100644 --- a/kernel/term_typing.mli +++ b/kernel/term_typing.mli @@ -12,6 +12,8 @@ open Environ open Declarations open Entries +type side_effects + val translate_local_def : structure_body -> env -> Id.t -> side_effects definition_entry -> constant_def * types * constant_universes @@ -29,7 +31,15 @@ val inline_entry_side_effects : {!Entries.const_entry_body} field. It is meant to get a term out of a not yet type checked proof. *) -val uniq_seff : side_effects -> 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 : |