Merge PR#475: Opaque side effects

1 files changed, 11 insertions, 1 deletions

diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli
index 89b5fc40e3..075389ea53 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 :