Merge branch 'trunk' into pr379

11 files changed, 164 insertions, 95 deletions

diff --git a/kernel/cbytecodes.ml b/kernel/cbytecodes.ml
index 810c346990..94ca4c72dd 100644
--- a/kernel/cbytecodes.ml
+++ b/kernel/cbytecodes.ml
@@ -299,7 +299,7 @@ and pp_bytecodes c =
   | Ksequence (l1, l2) :: c ->
       pp_bytecodes l1 ++ pp_bytecodes l2 ++  pp_bytecodes c
   | i :: c ->
-      tab () ++ pp_instr i ++ fnl () ++ pp_bytecodes c
+      pp_instr i ++ fnl () ++ pp_bytecodes c
 
 (*spiwack: moved this type in this file  because I needed it for
   retroknowledge which can't depend from cbytegen *)
diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml
index ad7a41a347..40c1e027d4 100644
--- a/kernel/cemitcodes.ml
+++ b/kernel/cemitcodes.ml
@@ -24,33 +24,45 @@ type reloc_info =
 type patch = reloc_info * int
 
 let patch_char4 buff pos c1 c2 c3 c4 = 
-  String.unsafe_set buff pos       c1;
-  String.unsafe_set buff (pos + 1) c2;
-  String.unsafe_set buff (pos + 2) c3;
-  String.unsafe_set buff (pos + 3) c4 
+  Bytes.unsafe_set buff pos       c1;
+  Bytes.unsafe_set buff (pos + 1) c2;
+  Bytes.unsafe_set buff (pos + 2) c3;
+  Bytes.unsafe_set buff (pos + 3) c4 
   
 let patch buff (pos, n) =
   patch_char4 buff pos 
     (Char.unsafe_chr n) (Char.unsafe_chr (n asr 8))  (Char.unsafe_chr (n asr 16))
     (Char.unsafe_chr (n asr 24))
 
+(* val patch_int : emitcodes -> ((\*pos*\)int * int) list -> emitcodes *)
 let patch_int buff patches =
   (* copy code *before* patching because of nested evaluations:
      the code we are patching might be called (and thus "concurrently" patched)
      and results in wrong results. Side-effects... *)
-  let buff = String.copy buff in
+  let buff = Bytes.of_string buff in
   let () = List.iter (fun p -> patch buff p) patches in
-  buff
+  (* Note: we follow the apporach suggested by Gabriel Scherer in
+     PR#136 here, and use unsafe as we own buff.
+
+     The crux of the question that avoids defining emitcodes just as a
+     Byte.t is the call to hcons in to_memory below. Even if disabling
+     this optimization has no visible time impact, test data shows
+     that the optimization is indeed triggered quite often so we
+     choose ugliness over altering the semantics.
+
+     Handle with care.
+  *)
+  Bytes.unsafe_to_string buff
 
 (* Buffering of bytecode *)
 
-let out_buffer = ref(String.create 1024)
+let out_buffer = ref(Bytes.create 1024)
 and out_position = ref 0
 
 let out_word b1 b2 b3 b4 =
   let p = !out_position in
-  if p >= String.length !out_buffer then begin
-    let len = String.length !out_buffer in
+  if p >= Bytes.length !out_buffer then begin
+    let len = Bytes.length !out_buffer in
     let new_len =
       if len <= Sys.max_string_length / 2
       then 2 * len
@@ -58,8 +70,8 @@ let out_word b1 b2 b3 b4 =
 	if len = Sys.max_string_length
 	then invalid_arg "String.create"  (* Pas la bonne exception .... *)
 	else Sys.max_string_length in
-    let new_buffer = String.create new_len in
-    String.blit !out_buffer 0 new_buffer 0 len;
+    let new_buffer = Bytes.create new_len in
+    Bytes.blit !out_buffer 0 new_buffer 0 len;
     out_buffer := new_buffer
   end;
   patch_char4 !out_buffer p (Char.unsafe_chr b1)
@@ -94,10 +106,10 @@ let extend_label_table needed =
 
 let backpatch (pos, orig) =
   let displ = (!out_position - orig) asr 2 in
-  !out_buffer.[pos]   <- Char.unsafe_chr displ;
-  !out_buffer.[pos+1] <- Char.unsafe_chr (displ asr 8);
-  !out_buffer.[pos+2] <- Char.unsafe_chr (displ asr 16);
-  !out_buffer.[pos+3] <- Char.unsafe_chr (displ asr 24)
+  Bytes.set !out_buffer  pos    @@ Char.unsafe_chr displ;
+  Bytes.set !out_buffer (pos+1) @@ Char.unsafe_chr (displ asr 8);
+  Bytes.set !out_buffer (pos+2) @@ Char.unsafe_chr (displ asr 16);
+  Bytes.set !out_buffer (pos+3) @@ Char.unsafe_chr (displ asr 24)
 
 let define_label lbl =
   if lbl >= Array.length !label_table then extend_label_table lbl;
@@ -262,41 +274,44 @@ let emit_instr = function
   | Kstop ->
       out opSTOP
 
-(* Emission of a list of instructions. Include some peephole optimization. *)
+(* Emission of a current list and remaining lists of instructions. Include some peephole optimization. *)
 
-let rec emit = function
-  | [] -> ()
+let rec emit insns remaining = match insns with
+  | [] -> 
+     (match remaining with 
+       [] -> () 
+     | (first::rest) -> emit first rest)
   (* Peephole optimizations *)
   | Kpush :: Kacc n :: c ->
       if n < 8 then out(opPUSHACC0 + n) else (out opPUSHACC; out_int n);
-      emit c
+      emit c remaining
   | Kpush :: Kenvacc n :: c ->
       if n >= 1 && n <= 4
       then out(opPUSHENVACC1 + n - 1)
       else (out opPUSHENVACC; out_int n);
-      emit c
+      emit c remaining
   | Kpush :: Koffsetclosure ofs :: c ->
       if Int.equal ofs (-2) || Int.equal ofs 0 || Int.equal ofs 2
       then out(opPUSHOFFSETCLOSURE0 + ofs / 2)
       else (out opPUSHOFFSETCLOSURE; out_int ofs);
-      emit c
+      emit c remaining
   | Kpush :: Kgetglobal id :: c ->
-      out opPUSHGETGLOBAL; slot_for_getglobal id; emit c
+      out opPUSHGETGLOBAL; slot_for_getglobal id; emit c remaining
   | Kpush :: Kconst (Const_b0 i) :: c ->
       if i >= 0 && i <= 3
       then out (opPUSHCONST0 + i)
       else (out opPUSHCONSTINT; out_int i);
-      emit c
+      emit c remaining
   | Kpush :: Kconst const :: c ->
       out opPUSHGETGLOBAL; slot_for_const const;
-      emit c
+      emit c remaining
   | Kpop n :: Kjump :: c ->
-      out opRETURN; out_int n; emit c
+      out opRETURN; out_int n; emit c remaining
   | Ksequence(c1,c2)::c ->
-      emit c1; emit c2;emit c
+      emit c1 (c2::c::remaining)
   (* Default case *)
   | instr :: c ->
-      emit_instr instr; emit c
+      emit_instr instr; emit c remaining
 
 (* Initialization *)
 
@@ -305,7 +320,7 @@ let init () =
   label_table := Array.make 16 (Label_undefined []);
   reloc_info := []
 
-type emitcodes = string
+type emitcodes = String.t
 
 let length = String.length
 
@@ -367,11 +382,10 @@ let repr_body_code = function
 
 let to_memory (init_code, fun_code, fv) =
   init();
-  emit init_code;
-  emit fun_code;
-  let code = String.create !out_position in
-  String.unsafe_blit !out_buffer 0 code 0 !out_position;
+  emit init_code [];
+  emit fun_code [];
   (** Later uses of this string are all purely functional *)
+  let code = Bytes.sub_string !out_buffer 0 !out_position in
   let code = CString.hcons code in
   let reloc = List.rev !reloc_info in
   Array.iter (fun lbl ->
diff --git a/kernel/entries.mli b/kernel/entries.mli
index 77081947ec..1e07c96909 100644
--- a/kernel/entries.mli
+++ b/kernel/entries.mli
@@ -113,5 +113,3 @@ type side_effect = {
   from_env : Declarations.structure_body CEphemeron.key;
   eff      : side_eff;
 }
-
-type side_effects = side_effect list
diff --git a/kernel/names.ml b/kernel/names.ml
index 1f138581cc..ee8d838da1 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -50,17 +50,20 @@ struct
   | None -> true
   | Some _ -> false
 
+  let of_bytes s =
+    let s = Bytes.to_string s in
+    check_soft s;
+    String.hcons s
+
   let of_string s =
     let () = check_soft s in
-    let s = String.copy s in
     String.hcons s
 
   let of_string_soft s =
     let () = check_soft ~warn:false s in
-    let s = String.copy s in
     String.hcons s
 
-  let to_string id = String.copy id
+  let to_string id = id
 
   let print id = str id
 
diff --git a/kernel/names.mli b/kernel/names.mli
index 6b0a80625b..be9b9422b7 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -43,6 +43,7 @@ sig
   (** Check that a string may be converted to an identifier.
   @raise Unicode.Unsupported if the provided string contains unsupported UTF-8 characters. *)
 
+  val of_bytes : bytes -> t
   val of_string : string -> t
   (** Converts a string into an identifier.
       @raise UserError if the string is not valid, or echo a warning if it contains invalid identifier characters.
diff --git a/kernel/nativevalues.ml b/kernel/nativevalues.ml
index 8093df3044..965ed67b07 100644
--- a/kernel/nativevalues.ml
+++ b/kernel/nativevalues.ml
@@ -491,12 +491,12 @@ let str_encode expr =
 let str_decode s =
   let mshl_expr_len = String.length s / 2 in
   let mshl_expr = Buffer.create mshl_expr_len in
-  let buf = String.create 2 in
+  let buf = Bytes.create 2 in
   for i = 0 to mshl_expr_len - 1 do
-    String.blit s (2*i) buf 0 2;
-    Buffer.add_char mshl_expr (bin_of_hex buf)
+    Bytes.blit_string s (2*i) buf 0 2;
+    Buffer.add_char mshl_expr (bin_of_hex (Bytes.to_string buf))
   done;
-  Marshal.from_string (Buffer.contents mshl_expr) 0
+  Marshal.from_bytes (Buffer.to_bytes mshl_expr) 0
 
 (** Retroknowledge, to be removed when we switch to primitive integers *)
 
diff --git a/kernel/opaqueproof.ml b/kernel/opaqueproof.ml
index 130f1eb039..f147ea3433 100644
--- a/kernel/opaqueproof.ml
+++ b/kernel/opaqueproof.ml
@@ -136,7 +136,7 @@ let dump (otab,_) =
   let disch_table = Array.make n a_discharge in
   let f2t_map = ref FMap.empty in
   Int.Map.iter (fun n (d,cu) ->
-    let c, u = Future.split2 ~greedy:true cu in
+    let c, u = Future.split2 cu in
     Future.sink u;
     Future.sink c;
     opaque_table.(n) <- c;
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index e4b3fcbf1a..caaaff1b89 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -71,7 +71,7 @@ module NamedDecl = Context.Named.Declaration
   - [env] : the underlying environment (cf Environ)
   - [modpath] : the current module name
   - [modvariant] :
-    * NONE before coqtop initialization (or when -notop is used)
+    * NONE before coqtop initialization
     * LIBRARY at toplevel of a compilation or a regular coqtop session
     * STRUCT (params,oldsenv) : inside a local module, with
       module parameters [params] and earlier environment [oldsenv]
@@ -208,19 +208,19 @@ let get_opaque_body env cbo =
          Opaqueproof.force_constraints (Environ.opaque_tables env) opaque)
 
 type private_constant = Entries.side_effect
-type private_constants = private_constant list
+type private_constants = Term_typing.side_effects
 
 type private_constant_role = Term_typing.side_effect_role =
   | Subproof
   | Schema of inductive * string
 
-let empty_private_constants = []
-let add_private x xs = if List.mem_f Term_typing.equal_eff x xs then xs else x :: xs
-let concat_private xs ys = List.fold_right add_private xs ys
+let empty_private_constants = Term_typing.empty_seff
+let add_private = Term_typing.add_seff
+let concat_private = Term_typing.concat_seff
 let mk_pure_proof = Term_typing.mk_pure_proof
 let inline_private_constants_in_constr = Term_typing.inline_side_effects
 let inline_private_constants_in_definition_entry = Term_typing.inline_entry_side_effects
-let side_effects_of_private_constants x = Term_typing.uniq_seff (List.rev x)
+let side_effects_of_private_constants = Term_typing.uniq_seff
 
 let private_con_of_con env c =
   let cbo = Environ.lookup_constant c env.env in
@@ -250,7 +250,7 @@ let universes_of_private eff =
      | Entries.SEsubproof (c, cb, e) ->
 	if cb.const_polymorphic then acc
 	else Univ.ContextSet.of_context cb.const_universes :: acc)
-   [] eff
+   [] (Term_typing.uniq_seff eff)
 
 let env_of_safe_env senv = senv.env
 let env_of_senv = env_of_safe_env
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 15ebc7d880..efeb98bd25 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -47,11 +47,18 @@ type private_constant_role =
   | Schema of inductive * string
 
 val side_effects_of_private_constants :
-  private_constants -> Entries.side_effects
+  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.ml b/kernel/term_typing.ml
index 3a0d1a2a5e..2eb2c040e1 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -24,28 +24,8 @@ open Typeops
 module RelDecl = Context.Rel.Declaration
 module NamedDecl = Context.Named.Declaration
 
-let constrain_type env j poly subst = function
-  | `None -> 
-    if not poly then (* Old-style polymorphism *)
-      make_polymorphic_if_constant_for_ind env j
-    else RegularArity (Vars.subst_univs_level_constr subst j.uj_type)
-  | `Some t ->
-      let tj = infer_type env t in
-      let _ = judge_of_cast env j DEFAULTcast tj in
-	assert (eq_constr t tj.utj_val);
-	RegularArity (Vars.subst_univs_level_constr subst t)
-  | `SomeWJ (t, tj) ->
-      let tj = infer_type env t in
-      let _ = judge_of_cast env j DEFAULTcast tj in
-	assert (eq_constr t tj.utj_val);
-	RegularArity (Vars.subst_univs_level_constr subst t)
-
-let map_option_typ = function None -> `None | Some x -> `Some x
-
 (* Insertion of constants and parameters in environment. *)
 
-let mk_pure_proof c = (c, Univ.ContextSet.empty), []
-
 let equal_eff e1 e2 =
   let open Entries in
   match e1, e2 with
@@ -57,13 +37,54 @@ let equal_eff e1 e2 =
           cl1 cl2
   | _ -> false
 
-let rec uniq_seff = function
-  | [] -> []
-  | x :: xs -> x :: uniq_seff (List.filter (fun y -> not (equal_eff x y)) xs)
-(* The list of side effects is in reverse order (most recent first).
- * To keep the "topological" order between effects we have to uniq-ize from
- * the tail *)
-let uniq_seff l = List.rev (uniq_seff (List.rev l))
+module SideEffects :
+sig
+  type t
+  val repr : t -> side_effect list
+  val empty : t
+  val add : side_effect -> t -> t
+  val concat : t -> t -> t
+end =
+struct
+
+let compare_seff e1 e2 = match e1, e2 with
+| SEsubproof (c1, _, _), SEsubproof (c2, _, _) -> Constant.CanOrd.compare c1 c2
+| SEscheme (cl1, _), SEscheme (cl2, _) ->
+  let cmp (_, c1, _, _) (_, c2, _, _) = Constant.CanOrd.compare c1 c2 in
+  CList.compare cmp cl1 cl2
+| SEsubproof _, SEscheme _ -> -1
+| SEscheme _, SEsubproof _ -> 1
+
+module SeffOrd = struct
+type t = side_effect
+let compare e1 e2 = compare_seff e1.eff e2.eff
+end
+
+module SeffSet = Set.Make(SeffOrd)
+
+type t = { seff : side_effect list; elts : SeffSet.t }
+(** Invariant: [seff] is a permutation of the elements of [elts] *)
+
+let repr eff = eff.seff
+let empty = { seff = []; elts = SeffSet.empty }
+let add x es =
+  if SeffSet.mem x es.elts then es
+  else { seff = x :: es.seff; elts = SeffSet.add x es.elts }
+let concat xes yes =
+  List.fold_right add xes.seff yes
+
+end
+
+type side_effects = SideEffects.t
+
+let uniq_seff_rev = SideEffects.repr
+let uniq_seff l = List.rev (SideEffects.repr l)
+
+let empty_seff = SideEffects.empty
+let add_seff = SideEffects.add
+let concat_seff = SideEffects.concat
+
+let mk_pure_proof c = (c, Univ.ContextSet.empty), empty_seff
 
 let inline_side_effects env body ctx side_eff =
   let handle_sideff (t,ctx,sl) { eff = se; from_env = mb } =
@@ -76,8 +97,7 @@ let inline_side_effects env body ctx side_eff =
     let cbl = List.filter not_exists cbl in
     let cname c = 
       let name = string_of_con c in
-      for i = 0 to String.length name - 1 do
-        if name.[i] == '.' || name.[i] == '#' then name.[i] <- '_' done;
+      let name = String.map (fun c -> if c == '.' || c == '#' then '_' else c) name in
       Name (id_of_string name) in
     let rec sub c i x = match kind_of_term x with
       | Const (c', _) when eq_constant c c' -> mkRel i
@@ -117,7 +137,7 @@ let inline_side_effects env body ctx side_eff =
     t, ctx, (mb,List.length cbl) :: sl
   in
   (* CAVEAT: we assure a proper order *)
-  List.fold_left handle_sideff (body,ctx,[]) (uniq_seff side_eff)
+  List.fold_left handle_sideff (body,ctx,[]) (uniq_seff_rev side_eff)
 
 (* Given the list of signatures of side effects, checks if they match.
  * I.e. if they are ordered descendants of the current revstruct *)
@@ -184,6 +204,10 @@ let infer_declaration ~trust env kn dcl =
       let t = hcons_constr (Vars.subst_univs_level_constr usubst c) in
 	Undef nl, RegularArity t, None, poly, univs, false, ctx
 
+  (** Definition [c] is opaque (Qed), non polymorphic and with a specified type,
+      so we delay the typing and hash consing of its body.
+      Remark: when the universe quantification is given explicitly, we could
+      delay even in the polymorphic case.  *)
   | DefinitionEntry ({ const_entry_type = Some typ;
                        const_entry_opaque = true;
 		       const_entry_polymorphic = false} as c) ->
@@ -191,19 +215,20 @@ let infer_declaration ~trust env kn dcl =
       let { const_entry_body = body; const_entry_feedback = feedback_id } = c in
       let tyj = infer_type env typ in
       let proofterm =
-        Future.chain ~greedy:true ~pure:true body (fun ((body,uctx),side_eff) ->
+        Future.chain ~pure:true body (fun ((body,uctx),side_eff) ->
           let body, uctx, signatures =
             inline_side_effects env body uctx side_eff in
           let valid_signatures = check_signatures trust signatures in
-	  let env' = push_context_set uctx env in
+	  let env = push_context_set uctx env in
           let j =
-            let body,env',ectx = skip_trusted_seff valid_signatures body env' in
-            let j = infer env' body in
+            let body,env,ectx = skip_trusted_seff valid_signatures body env in
+            let j = infer env body in
             unzip ectx j in
           let j = hcons_j j in
 	  let subst = Univ.LMap.empty in
-          let _typ = constrain_type env' j c.const_entry_polymorphic subst
-	    (`SomeWJ (typ,tyj)) in
+          let _ = judge_of_cast env j DEFAULTcast tyj in
+          assert (eq_constr typ tyj.utj_val);
+          let _typ = RegularArity (Vars.subst_univs_level_constr subst typ) in
           feedback_completion_typecheck feedback_id;
           j.uj_val, uctx) in
       let def = OpaqueDef (Opaqueproof.create proofterm) in
@@ -211,6 +236,7 @@ let infer_declaration ~trust env kn dcl =
 	c.const_entry_universes,
 	c.const_entry_inline_code, c.const_entry_secctx
 
+  (** Other definitions have to be processed immediately. *)
   | DefinitionEntry c ->
       let { const_entry_type = typ; const_entry_opaque = opaque } = c in
       let { const_entry_body = body; const_entry_feedback = feedback_id } = c in
@@ -223,7 +249,17 @@ let infer_declaration ~trust env kn dcl =
       let usubst, univs =
 	Univ.abstract_universes abstract (Univ.ContextSet.to_context ctx) in      
       let j = infer env body in
-      let typ = constrain_type env j c.const_entry_polymorphic usubst (map_option_typ typ) in
+      let typ = match typ with
+        | None ->
+           if not c.const_entry_polymorphic then (* Old-style polymorphism *)
+             make_polymorphic_if_constant_for_ind env j
+           else RegularArity (Vars.subst_univs_level_constr usubst j.uj_type)
+        | Some t ->
+           let tj = infer_type env t in
+           let _ = judge_of_cast env j DEFAULTcast tj in
+           assert (eq_constr t tj.utj_val);
+           RegularArity (Vars.subst_univs_level_constr usubst t)
+      in
       let def = hcons_constr (Vars.subst_univs_level_constr usubst j.uj_val) in
       let def = 
 	if opaque then OpaqueDef (Opaqueproof.create (Future.from_val (def, Univ.ContextSet.empty)))
@@ -383,7 +419,7 @@ let constant_entry_of_side_effect cb u =
     | Def b, `Nothing -> Mod_subst.force_constr b, Univ.ContextSet.empty
     | _ -> assert false in
   DefinitionEntry {
-    const_entry_body = Future.from_val (pt, []);
+    const_entry_body = Future.from_val (pt, empty_seff);
     const_entry_secctx = None;
     const_entry_feedback = None;
     const_entry_type =
@@ -416,8 +452,8 @@ let export_side_effects mb env ce =
       let { const_entry_body = body } = c in
       let _, eff = Future.force body in
       let ce = DefinitionEntry { c with
-        const_entry_body = Future.chain ~greedy:true ~pure:true body
-          (fun (b_ctx, _) -> b_ctx, []) } in
+        const_entry_body = Future.chain ~pure:true body
+          (fun (b_ctx, _) -> b_ctx, empty_seff) } in
       let not_exists (c,_,_,_) =
         try ignore(Environ.lookup_constant c env); false
         with Not_found -> true in 
@@ -429,7 +465,7 @@ let export_side_effects mb env ce =
         let cbl = List.filter not_exists cbl in
         if cbl = [] then acc, sl
         else cbl :: acc, (mb,List.length cbl) :: sl in
-      let seff, signatures = List.fold_left aux ([],[]) (uniq_seff eff) in
+      let seff, signatures = List.fold_left aux ([],[]) (uniq_seff_rev eff) in
       let trusted = check_signatures mb signatures in
       let push_seff env = function
         | kn, cb, `Nothing, _ ->
@@ -498,10 +534,10 @@ let translate_local_def mb env id centry =
 let translate_mind env kn mie = Indtypes.check_inductive env kn mie
 
 let inline_entry_side_effects env ce = { ce with
-  const_entry_body = Future.chain ~greedy:true ~pure:true
+  const_entry_body = Future.chain ~pure:true
     ce.const_entry_body (fun ((body, ctx), side_eff) ->
       let body, ctx',_ = inline_side_effects env body ctx side_eff in
-      (body, ctx'), []);
+      (body, ctx'), empty_seff);
 }
 
 let inline_side_effects env body side_eff =
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 :