Avoid type checking private_constants (side_eff) again during Qed (#4357).

Side effects are now an opaque data type, called private_constant, you can
only obtain from safe_typing.  When add_constant is called on a
definition_entry that contains private constants, they are either
- inlined in the main proof term but not re-checked
- declared globally without re-checking them
As a safety measure, the opaque data type contains a pointer to the
revstruct (an internal field of safe_env that changes every time a new
constant is added), and such pointer is compared with the current value
store in safe_env when the private_constant is inlined.  Only when the
comparison is successful the private_constant is not re-checked.  Otherwise
else it is.  In short, we accept into the kernel private constant only
when they arrive in the very same order and on top of the very same env
they arrived when we fist checked them.

Note: private_constants produced by workers never pass the safety
measure (the revstruct pointer is an Ephemeron).  Sending back the
entire revstruct is possible but: 1. we lack a way to quickly compare
two revstructs, 2. it can be large.

43 files changed, 547 insertions, 312 deletions

diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index 7def963e7..dc5c17a75 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -79,12 +79,6 @@ type constant_body = {
     const_proj : projection_body option;
     const_inline_code : bool }
 
-type seff_env = [ `Nothing | `Opaque of Constr.t * Univ.universe_context_set ]
-
-type side_effect =
-  | SEsubproof of constant * constant_body * seff_env
-  | SEscheme of (inductive * constant * constant_body * seff_env) list * string
-    
 (** {6 Representation of mutual inductive types in the kernel } *)
 
 type recarg =
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index a7051d5c1..248504c1b 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -304,17 +304,7 @@ let hcons_mind mib =
 
 (** {6 Stm machinery } *)
 
-let string_of_side_effect = function
-  | SEsubproof (c,_,_) -> Names.string_of_con c
-  | SEscheme (cl,_) ->
-      String.concat ", " (List.map (fun (_,c,_,_) -> Names.string_of_con c) cl)
-type side_effects = side_effect list
-let no_seff = ([] : side_effects)
-let iter_side_effects f l = List.iter f (List.rev l)
-let fold_side_effects f a l = List.fold_left f a l
-let uniquize_side_effects l = List.rev (CList.uniquize (List.rev l))
-let union_side_effects l1 l2 = l1 @ l2
-let flatten_side_effects l = List.flatten l
-let side_effects_of_list l = l
-let cons_side_effects x l = x :: l
-let side_effects_is_empty = List.is_empty
+let string_of_side_effect { Entries.eff } = match eff with
+  | Entries.SEsubproof (c,_,_) -> "P(" ^ Names.string_of_con c ^ ")"
+  | Entries.SEscheme (cl,_) ->
+      "S(" ^ String.concat ", " (List.map (fun (_,c,_,_) -> Names.string_of_con c) cl) ^ ")"
diff --git a/kernel/declareops.mli b/kernel/declareops.mli
index ce65af975..1b8700958 100644
--- a/kernel/declareops.mli
+++ b/kernel/declareops.mli
@@ -9,6 +9,7 @@
 open Declarations
 open Mod_subst
 open Univ
+open Entries
 
 (** Operations concerning types in [Declarations] :
     [constant_body], [mutual_inductive_body], [module_body] ... *)
@@ -49,17 +50,6 @@ val is_opaque : constant_body -> bool
 
 val string_of_side_effect : side_effect -> string
 
-type side_effects
-val no_seff : side_effects
-val iter_side_effects : (side_effect -> unit) -> side_effects -> unit
-val fold_side_effects : ('a -> side_effect -> 'a) -> 'a -> side_effects -> 'a
-val uniquize_side_effects : side_effects -> side_effects
-val union_side_effects : side_effects -> side_effects -> side_effects
-val flatten_side_effects : side_effects list -> side_effects
-val side_effects_of_list : side_effect list -> side_effects
-val cons_side_effects : side_effect -> side_effects -> side_effects
-val side_effects_is_empty : side_effects -> bool
-
 (** {6 Inductive types} *)
 
 val eq_recarg : recarg -> recarg -> bool
diff --git a/kernel/entries.mli b/kernel/entries.mli
index 303d27d35..e058519e9 100644
--- a/kernel/entries.mli
+++ b/kernel/entries.mli
@@ -54,11 +54,11 @@ type mutual_inductive_entry = {
   mind_entry_private : bool option }
 
 (** {6 Constants (Definition/Axiom) } *)
-type proof_output = constr Univ.in_universe_context_set * Declareops.side_effects
-type const_entry_body = proof_output Future.computation
+type 'a proof_output = constr Univ.in_universe_context_set * 'a
+type 'a const_entry_body = 'a proof_output Future.computation
 
-type definition_entry = {
-  const_entry_body   : const_entry_body;
+type 'a definition_entry = {
+  const_entry_body   : 'a const_entry_body;
   (* List of section variables *)
   const_entry_secctx : Context.section_context option;
   (* State id on which the completion of type checking is reported *)
@@ -78,8 +78,8 @@ type projection_entry = {
   proj_entry_ind : mutual_inductive;
   proj_entry_arg : int }
 
-type constant_entry =
-  | DefinitionEntry of definition_entry
+type 'a constant_entry =
+  | DefinitionEntry of 'a definition_entry
   | ParameterEntry of parameter_entry
   | ProjectionEntry of projection_entry
 
@@ -96,3 +96,16 @@ type module_entry =
   | MType of module_params_entry * module_struct_entry
   | MExpr of
       module_params_entry * module_struct_entry * module_struct_entry option
+
+type seff_env = [ `Nothing | `Opaque of Constr.t * Univ.universe_context_set ]
+
+type side_eff =
+  | SEsubproof of constant * Declarations.constant_body * seff_env
+  | SEscheme of (inductive * constant * Declarations.constant_body * seff_env) list * string
+
+type side_effect = {
+  from_env : Declarations.structure_body Ephemeron.key;
+  eff      : side_eff;
+}
+
+type side_effects = side_effect list
diff --git a/kernel/opaqueproof.ml b/kernel/opaqueproof.ml
index 9f4361f40..badb15b56 100644
--- a/kernel/opaqueproof.ml
+++ b/kernel/opaqueproof.ml
@@ -43,7 +43,10 @@ let set_indirect_univ_accessor f = (get_univ := f)
 let create cu = Direct ([],cu)
 
 let turn_indirect dp o (prfs,odp) = match o with
-  | Indirect _ -> Errors.anomaly (Pp.str "Already an indirect opaque")
+  | Indirect (_,_,i) ->
+      if not (Int.Map.mem i prfs)
+      then Errors.anomaly (Pp.str "Indirect in a different table")
+      else Errors.anomaly (Pp.str "Already an indirect opaque")
   | Direct (d,cu) ->
       let cu = Future.chain ~pure:true cu (fun (c, u) -> hcons_constr c, u) in
       let id = Int.Map.cardinal prfs in
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index ec245b064..b71cd31b5 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -207,15 +207,55 @@ let get_opaque_body env cbo =
         (Opaqueproof.force_proof (Environ.opaque_tables env) opaque,
          Opaqueproof.force_constraints (Environ.opaque_tables env) opaque)
 
-let sideff_of_con env c =
+type private_constant = Entries.side_effect
+type private_constants = private_constant list
+
+type private_constant_role = Term_typing.side_effect_role =
+  | Subproof
+  | Schema of inductive * string
+
+let empty_private_constants = []
+let add_private x xs = x :: xs
+let concat_private xs ys = xs @ ys
+let mk_pure_proof = Term_typing.mk_pure_proof
+let inline_private_constants_in_constr = Term_typing.handle_side_effects
+let inline_private_constants_in_definition_entry = Term_typing.handle_entry_side_effects
+let side_effects_of_private_constants x = Term_typing.uniq_seff (List.rev x)
+
+let constant_entry_of_private_constant = function
+  | { Entries.eff = Entries.SEsubproof (kn, cb, eff_env) } ->
+      [ kn, Term_typing.constant_entry_of_side_effect cb eff_env ]
+  | { Entries.eff = Entries.SEscheme (l,_) } ->
+      List.map (fun (_,kn,cb,eff_env) ->
+        kn, Term_typing.constant_entry_of_side_effect cb eff_env) l
+
+let private_con_of_con env c =
   let cbo = Environ.lookup_constant c env.env in
-  SEsubproof (c, cbo, get_opaque_body env.env cbo)
-let sideff_of_scheme kind env cl =
-  SEscheme(
-    List.map (fun (i,c) ->
-      let cbo = Environ.lookup_constant c env.env in
-      i, c, cbo, get_opaque_body env.env cbo) cl,
-    kind)
+  { Entries.from_env = Ephemeron.create env.revstruct;
+    Entries.eff      = Entries.SEsubproof (c,cbo,get_opaque_body env.env cbo) }
+
+let private_con_of_scheme ~kind env cl =
+  { Entries.from_env = Ephemeron.create env.revstruct;
+    Entries.eff      = Entries.SEscheme(
+      List.map (fun (i,c) ->
+        let cbo = Environ.lookup_constant c env.env in
+        i, c, cbo, get_opaque_body env.env cbo) cl,
+      kind) }
+
+let universes_of_private eff =
+  let open Declarations in
+  List.fold_left (fun acc { Entries.eff } ->
+     match eff with
+     | Entries.SEscheme (l,s) ->
+        List.fold_left (fun acc (_,_,cb,c) ->
+          let acc = match c with
+            | `Nothing -> acc
+            | `Opaque (_, ctx) -> ctx :: acc in
+          if cb.const_polymorphic then acc
+          else (Univ.ContextSet.of_context cb.const_universes) :: acc)
+        acc l
+     | Entries.SEsubproof _ -> acc)
+   [] eff
 
 let env_of_safe_env senv = senv.env
 let env_of_senv = env_of_safe_env
@@ -337,7 +377,7 @@ let safe_push_named (id,_,_ as d) env =
 
 
 let push_named_def (id,de) senv =
-  let c,typ,univs = Term_typing.translate_local_def senv.env id de in
+  let c,typ,univs = Term_typing.translate_local_def senv.revstruct senv.env id de in
   let poly = de.Entries.const_entry_polymorphic in
   let univs = Univ.ContextSet.of_context univs in
   let c, univs = match c with
@@ -442,19 +482,16 @@ let update_resolver f senv = { senv with modresolver = f senv.modresolver }
 
 (** Insertion of constants and parameters in environment *)
 type global_declaration =
-  | ConstantEntry of Entries.constant_entry
+  | ConstantEntry of bool * private_constants Entries.constant_entry
   | GlobalRecipe of Cooking.recipe
 
-let add_constant dir l decl senv =
-  let kn = make_con senv.modpath dir l in
-  let cb = match decl with
-    | ConstantEntry ce -> Term_typing.translate_constant senv.env kn ce
-    | GlobalRecipe r ->
-      let cb = Term_typing.translate_recipe senv.env kn r in
-      if DirPath.is_empty dir then Declareops.hcons_const_body cb else cb
-  in
+type exported_private_constant = 
+  constant * private_constants Entries.constant_entry * private_constant_role
+
+let add_constant_aux no_section senv (kn, cb) =
+  let l = pi3 (Constant.repr3 kn) in
   let cb, otab = match cb.const_body with
-    | OpaqueDef lc when DirPath.is_empty dir ->
+    | OpaqueDef lc when no_section ->
       (* In coqc, opaque constants outside sections will be stored
          indirectly in a specific table *)
       let od, otab =
@@ -471,7 +508,33 @@ let add_constant dir l decl senv =
         (Mod_subst.add_inline_delta_resolver (user_con kn) (lev,None)) senv'
     | _ -> senv'
   in
-  kn, senv''
+  senv''
+
+let add_constant dir l decl senv =
+  let kn = make_con senv.modpath dir l in
+  let no_section = DirPath.is_empty dir in
+  let seff_to_export, decl =
+    match decl with
+    | ConstantEntry (true, ce) ->
+        let exports, ce =
+          Term_typing.validate_side_effects_for_export
+            senv.revstruct senv.env ce in
+        exports, ConstantEntry (false, ce)
+    | _ -> [], decl
+  in
+  let senv =
+    List.fold_left (add_constant_aux no_section) senv
+      (List.map (fun (kn,cb,_,_) -> kn, cb) seff_to_export) in
+  let senv =
+    let cb = 
+      match decl with
+      | ConstantEntry (export_seff,ce) ->
+        Term_typing.translate_constant senv.revstruct senv.env kn ce
+      | GlobalRecipe r ->
+        let cb = Term_typing.translate_recipe senv.env kn r in
+        if no_section then Declareops.hcons_const_body cb else cb in
+    add_constant_aux no_section senv (kn, cb) in
+  (kn, List.map (fun (kn,_,ce,r) -> kn, ce, r) seff_to_export), senv
 
 (** Insertion of inductive types *)
 
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index eac08eb83..2214cf8bb 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -39,10 +39,30 @@ type 'a safe_transformer = safe_environment -> 'a * safe_environment
 
 (** {6 Stm machinery } *)
 
-val sideff_of_con : safe_environment -> constant -> Declarations.side_effect
-val sideff_of_scheme :
-  string -> safe_environment -> (inductive * constant) list ->
-    Declarations.side_effect
+type private_constant
+type private_constants
+
+type private_constant_role =
+  | Subproof
+  | Schema of inductive * string
+
+val side_effects_of_private_constants :
+  private_constants -> Entries.side_effects
+
+val empty_private_constants : private_constants
+val add_private : private_constant -> private_constants -> private_constants
+val concat_private : private_constants -> private_constants -> private_constants
+
+val private_con_of_con : safe_environment -> constant -> private_constant
+val private_con_of_scheme : kind:string -> safe_environment -> (inductive * constant) list -> private_constant
+
+val mk_pure_proof : Constr.constr -> private_constants Entries.proof_output
+val inline_private_constants_in_constr :
+  Environ.env -> Constr.constr -> private_constants -> Constr.constr
+val inline_private_constants_in_definition_entry :
+  Environ.env -> private_constants Entries.definition_entry -> private_constants Entries.definition_entry
+
+val universes_of_private : private_constants -> Univ.universe_context_set list
 
 val is_curmod_library : safe_environment -> bool
 
@@ -63,16 +83,23 @@ val push_named_assum :
 (** Returns the full universe context necessary to typecheck the definition
   (futures are forced) *)
 val push_named_def :
-  Id.t * Entries.definition_entry -> Univ.universe_context_set safe_transformer
+  Id.t * private_constants Entries.definition_entry -> Univ.universe_context_set safe_transformer
 
 (** Insertion of global axioms or definitions *)
 
 type global_declaration =
-  | ConstantEntry of Entries.constant_entry
+                  (* bool: export private constants *)
+  | ConstantEntry of bool * private_constants Entries.constant_entry
   | GlobalRecipe of Cooking.recipe
 
+type exported_private_constant = 
+  constant * private_constants Entries.constant_entry * private_constant_role
+
+(** returns the main constant plus a list of auxiliary constants (empty
+    unless one requires the side effects to be exported) *)
 val add_constant :
-  DirPath.t -> Label.t -> global_declaration -> constant safe_transformer
+  DirPath.t -> Label.t -> global_declaration ->
+    (constant * exported_private_constant list) safe_transformer
 
 (** Adding an inductive type *)
 
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index cab99077f..d75bd73fb 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -43,10 +43,29 @@ 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), Declareops.no_seff
+let mk_pure_proof c = (c, Univ.ContextSet.empty), []
+
+let equal_eff e1 e2 =
+  let open Entries in
+  match e1, e2 with
+  | { eff = SEsubproof (c1,_,_) }, { eff = SEsubproof (c2,_,_) } ->
+        Names.Constant.equal c1 c2
+  | { eff = SEscheme (cl1,_) }, { eff = SEscheme (cl2,_) } ->
+        CList.for_all2eq
+          (fun (_,c1,_,_) (_,c2,_,_) -> Names.Constant.equal c1 c2)
+          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 "tological" order between effects we have to uniqize from the
+ * tail *)
+let uniq_seff l = List.rev (uniq_seff (List.rev l))
 
 let handle_side_effects env body ctx side_eff =
-  let handle_sideff (t,ctx) se =
+  let handle_sideff (t,ctx,sl) { eff = se; from_env = mb } =
     let cbl = match se with
       | SEsubproof (c,cb,b) -> [c,cb,b]
       | SEscheme (cl,_) -> List.map (fun (_,c,cb,b) -> c,cb,b) cl in
@@ -65,7 +84,7 @@ let handle_side_effects env body ctx side_eff =
     let rec sub_body c u b i x = match kind_of_term x with
       | Const (c',u') when eq_constant c c' -> 
 	Vars.subst_instance_constr u' b
-      | _ -> map_constr_with_binders ((+) 1) (fun i x -> sub_body c u b i x) i x in
+      | _ -> map_constr_with_binders ((+) 1) (sub_body c u b) i x in
     let fix_body (c,cb,b) (t,ctx) =
       match cb.const_body, b with
       | Def b, _ ->
@@ -87,17 +106,60 @@ let handle_side_effects env body ctx side_eff =
               let t = sub c 1 (Vars.lift 1 t) in
 	        mkApp (mkLambda (cname c, b_ty, t), [|b|]),
 		Univ.ContextSet.union ctx
-		  (Univ.ContextSet.of_context cb.const_universes)		
+		  (Univ.ContextSet.of_context cb.const_universes)
 	    else
 	      let univs = cb.const_universes in
 		sub_body c (Univ.UContext.instance univs) b 1 (Vars.lift 1 t), ctx
       | _ -> assert false
     in
-      List.fold_right fix_body cbl (t,ctx)
+    let t, ctx = List.fold_right fix_body cbl (t,ctx) in
+    t, ctx, (mb,List.length cbl) :: sl
   in
   (* CAVEAT: we assure a proper order *)
-  Declareops.fold_side_effects handle_sideff (body,ctx)
-    (Declareops.uniquize_side_effects side_eff)
+  List.fold_left handle_sideff (body,ctx,[]) (uniq_seff side_eff)
+
+let check_signatures curmb sl =
+  let is_direct_ancestor (sl, curmb) (mb, how_many) =
+    match curmb with
+    | None -> None, None
+    | Some curmb ->
+        try
+          let mb = Ephemeron.get mb in
+          match sl with
+          | None -> sl, None
+          | Some n ->
+              if List.length mb >= how_many && CList.skipn how_many mb == curmb
+              then Some (n + how_many), Some mb
+              else None, None
+        with Ephemeron.InvalidKey -> None, None in
+  let sl, _ = List.fold_left is_direct_ancestor (Some 0,Some curmb) sl in
+  sl
+
+let trust_seff sl b e =
+  let rec aux sl b e acc =
+    match sl, kind_of_term b with
+    | (None|Some 0), _ -> b, e, acc
+    | Some sl, LetIn (n,c,ty,bo) ->
+       aux (Some (sl-1)) bo
+         (Environ.push_rel (n,Some c,ty) e) (`Let(n,c,ty)::acc)
+    | Some sl, App(hd,arg) ->
+       begin match kind_of_term hd with
+       | Lambda (n,ty,bo) ->
+           aux (Some (sl-1)) bo
+             (Environ.push_rel (n,None,ty) e) (`Cut(n,ty,arg)::acc)
+       | _ -> assert false
+       end
+    | _ -> assert false
+    in
+  aux sl b e []
+
+let rec unzip ctx j =
+  match ctx with
+  | [] -> j
+  | `Let (n,c,ty) :: ctx ->
+      unzip ctx { j with uj_val = mkLetIn (n,c,ty,j.uj_val) }
+  | `Cut (n,ty,arg) :: ctx ->
+      unzip ctx { j with uj_val = mkApp (mkLambda (n,ty,j.uj_val),arg) }
 
 let hcons_j j =
   { uj_val = hcons_constr j.uj_val; uj_type = hcons_constr j.uj_type} 
@@ -105,7 +167,7 @@ let hcons_j j =
 let feedback_completion_typecheck =
   Option.iter (fun state_id -> Pp.feedback ~state_id Feedback.Complete)
 	      
-let infer_declaration env kn dcl =
+let infer_declaration ~trust env kn dcl =
   match dcl with
   | ParameterEntry (ctx,poly,(t,uctx),nl) ->
       let env = push_context ~strict:(not poly) uctx env in
@@ -124,9 +186,14 @@ let infer_declaration env kn dcl =
       let tyj = infer_type env typ in
       let proofterm =
         Future.chain ~greedy:true ~pure:true body (fun ((body, ctx),side_eff) ->
-          let body,ctx = handle_side_effects env body ctx side_eff in
+          let body, ctx, signatures =
+            handle_side_effects env body ctx side_eff in
+          let trusted_signatures = check_signatures trust signatures in
 	  let env' = push_context_set ctx env in
-          let j = infer env' body in
+          let j =
+            let body, env', zip_ctx = trust_seff trusted_signatures body env' in
+            let j = infer env' body in
+            unzip zip_ctx 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
@@ -143,7 +210,7 @@ let infer_declaration env kn dcl =
       let { const_entry_body = body; const_entry_feedback = feedback_id } = c in
       let (body, ctx), side_eff = Future.join body in
       let univsctx = Univ.ContextSet.of_context c.const_entry_universes in
-      let body, ctx = handle_side_effects env body
+      let body, ctx, _ = handle_side_effects env body
         (Univ.ContextSet.union univsctx ctx) side_eff in
       let env = push_context_set ~strict:(not c.const_entry_polymorphic) ctx env in
       let abstract = c.const_entry_polymorphic && not (Option.is_empty kn) in
@@ -294,8 +361,93 @@ let build_constant_declaration kn env (def,typ,proj,poly,univs,inline_code,ctx)
 
 (*s Global and local constant declaration. *)
 
-let translate_constant env kn ce =
-  build_constant_declaration kn env (infer_declaration env (Some kn) ce)
+let translate_constant mb env kn ce =
+  build_constant_declaration kn env
+    (infer_declaration ~trust:mb env (Some kn) ce)
+
+let constant_entry_of_side_effect cb u =
+  let pt =
+    match cb.const_body, u with
+    | OpaqueDef _, `Opaque (b, c) -> b, c
+    | Def b, `Nothing -> Mod_subst.force_constr b, Univ.ContextSet.empty
+    | _ -> assert false in
+  DefinitionEntry {
+    const_entry_body = Future.from_val (pt, []);
+    const_entry_secctx = None;
+    const_entry_feedback = None;
+    const_entry_type =
+      (match cb.const_type with RegularArity t -> Some t | _ -> None);
+    const_entry_polymorphic = cb.const_polymorphic;
+    const_entry_universes = cb.const_universes;
+    const_entry_opaque = Declareops.is_opaque cb;
+    const_entry_inline_code = cb.const_inline_code }
+;;
+
+let turn_direct (kn,cb,u,r as orig) =
+  match cb.const_body, u with
+  | OpaqueDef _, `Opaque (b,c) ->
+      let pt = Future.from_val (b,c) in
+      kn, { cb with const_body = OpaqueDef (Opaqueproof.create pt) }, u, r
+   | _ -> orig
+;;
+
+type side_effect_role =
+  | Subproof
+  | Schema of inductive * string
+
+type exported_side_effect = 
+  constant * constant_body * side_effects Entries.constant_entry * side_effect_role
+
+let validate_side_effects_for_export mb env ce =
+  match ce with
+  | ParameterEntry _ | ProjectionEntry _ -> [], ce
+  | DefinitionEntry c ->
+      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
+      let not_exists (c,_,_,_) =
+        try ignore(Environ.lookup_constant c env); false
+        with Not_found -> true in 
+      let aux (acc,sl) { eff = se; from_env = mb } =
+        let cbl = match se with
+          | SEsubproof (c,cb,b) -> [c,cb,b,Subproof]
+          | SEscheme (cl,k) ->
+              List.map (fun (i,c,cb,b) -> c,cb,b,Schema(i,k)) cl in
+        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 trusted = check_signatures mb signatures in
+      let push_seff env = function
+        | kn, cb, `Nothing, _ ->
+            Environ.add_constant kn cb env
+        | kn, cb, `Opaque(_, ctx), _ -> 
+            let env = Environ.add_constant kn cb env in
+            Environ.push_context_set
+              ~strict:(not cb.const_polymorphic) ctx env in
+      let rec translate_seff sl seff acc env =
+        match sl, seff with
+        | _, [] -> List.rev acc, ce
+        | (None | Some 0), cbs :: rest ->
+           let env, cbs =
+             List.fold_left (fun (env,cbs) (kn, ocb, u, r) ->
+               let ce = constant_entry_of_side_effect ocb u in
+               let cb = translate_constant mb env kn ce in
+               (push_seff env (kn, cb,`Nothing, Subproof),(kn,cb,ce,r) :: cbs)) 
+             (env,[]) cbs in
+           translate_seff sl rest (cbs @ acc) env
+        | Some sl, cbs :: rest ->
+           let cbs_len = List.length cbs in
+           let cbs = List.map turn_direct cbs in
+           let env = List.fold_left push_seff env cbs in
+           let ecbs = List.map (fun (kn,cb,u,r) ->
+             kn, cb, constant_entry_of_side_effect cb u, r) cbs in
+           translate_seff (Some (sl-cbs_len)) rest (ecbs @ acc) env
+     in
+       translate_seff trusted seff [] env
+;;
 
 let translate_local_assum env t =
   let j = infer env t in
@@ -305,9 +457,9 @@ let translate_local_assum env t =
 let translate_recipe env kn r =
   build_constant_declaration kn env (Cooking.cook_constant env r)
 
-let translate_local_def env id centry =
+let translate_local_def mb env id centry =
   let def,typ,proj,poly,univs,inline_code,ctx =
-    infer_declaration env None (DefinitionEntry centry) in
+    infer_declaration ~trust:mb env None (DefinitionEntry centry) in
   let typ = type_of_constant_type env typ in
   if ctx = None && !Flags.compilation_mode = Flags.BuildVo then begin
     match def with
@@ -332,9 +484,9 @@ let translate_mind env kn mie = Indtypes.check_inductive env kn mie
 let handle_entry_side_effects env ce = { ce with
   const_entry_body = Future.chain ~greedy:true ~pure:true
     ce.const_entry_body (fun ((body, ctx), side_eff) ->
-			 let body, ctx' = handle_side_effects env body ctx side_eff in
-			 (body, ctx'), Declareops.no_seff);
+      let body, ctx',_ = handle_side_effects env body ctx side_eff in
+      (body, ctx'), []);
 }
 
 let handle_side_effects env body side_eff =
-  fst (handle_side_effects env body Univ.ContextSet.empty side_eff)
+  pi1 (handle_side_effects env body Univ.ContextSet.empty side_eff)
diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli
index 8d92bcc68..509160ccc 100644
--- a/kernel/term_typing.mli
+++ b/kernel/term_typing.mli
@@ -12,23 +12,42 @@ open Environ
 open Declarations
 open Entries
 
-val translate_local_def : env -> Id.t -> definition_entry ->
+val translate_local_def : structure_body -> env -> Id.t -> side_effects definition_entry ->
   constant_def * types * constant_universes
 
 val translate_local_assum : env -> types -> types
 
-val mk_pure_proof : constr -> proof_output
+val mk_pure_proof : constr -> side_effects proof_output
 
-val handle_side_effects : env -> constr -> Declareops.side_effects -> constr
+val handle_side_effects : env -> constr -> side_effects -> constr
 (** Returns the term where side effects have been turned into let-ins or beta
     redexes. *)
 
-val handle_entry_side_effects : env -> definition_entry -> definition_entry
+val handle_entry_side_effects : env -> side_effects definition_entry -> side_effects definition_entry
 (** Same as {!handle_side_effects} but applied to entries. Only modifies the
     {!Entries.const_entry_body} field. It is meant to get a term out of a not
     yet type checked proof. *)
 
-val translate_constant : env -> constant -> constant_entry -> constant_body
+val uniq_seff : side_effects -> side_effects
+
+val translate_constant : structure_body -> env -> constant -> side_effects constant_entry -> constant_body
+
+(* Checks weather the side effects in constant_entry can be trusted.
+ * Returns the list of effects to be exported.
+ * Note: It forces the Future.computation.                           *)
+type side_effect_role =
+  | Subproof
+  | Schema of inductive * string
+
+type exported_side_effect = 
+  constant * constant_body * side_effects Entries.constant_entry * side_effect_role
+  
+val validate_side_effects_for_export :
+  structure_body -> env -> side_effects constant_entry ->
+    exported_side_effect list * side_effects constant_entry
+
+val constant_entry_of_side_effect :
+  constant_body -> seff_env -> side_effects constant_entry
 
 val translate_mind :
   env -> mutual_inductive -> mutual_inductive_entry -> mutual_inductive_body
@@ -37,8 +56,8 @@ val translate_recipe : env -> constant -> Cooking.recipe -> constant_body
 
 (** Internal functions, mentioned here for debug purpose only *)
 
-val infer_declaration : env -> constant option -> 
-  constant_entry -> Cooking.result
+val infer_declaration : trust:structure_body -> env -> constant option -> 
+  side_effects constant_entry -> Cooking.result
 
 val build_constant_declaration :
   constant -> env -> Cooking.result -> constant_body
diff --git a/library/declare.ml b/library/declare.ml
index 0004f45a2..63e5a7224 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -35,7 +35,7 @@ type internal_flag =
 (** Declaration of section variables and local definitions *)
 
 type section_variable_entry =
-  | SectionLocalDef of definition_entry
+  | SectionLocalDef of Safe_typing.private_constants definition_entry
   | SectionLocalAssum of types Univ.in_universe_context_set * polymorphic * bool (** Implicit status *)
 
 type variable_declaration = DirPath.t * section_variable_entry * logical_kind
@@ -93,9 +93,13 @@ type constant_obj = {
   cst_hyps : Dischargedhypsmap.discharged_hyps;
   cst_kind : logical_kind;
   cst_locl : bool;
+  mutable cst_exported : Safe_typing.exported_private_constant list;
+  (* mutable: to avoid change the libobject API, since cache_function
+   * does not return an updated object *)
+  mutable cst_was_seff : bool
 }
 
-type constant_declaration = constant_entry * logical_kind
+type constant_declaration = Safe_typing.private_constants constant_entry * logical_kind
 
 (* At load-time, the segment starting from the module name to the discharge *)
 (* section (if Remark or Fact) is needed to access a construction *)
@@ -131,8 +135,17 @@ let check_exists sp =
 let cache_constant ((sp,kn), obj) =
   let id = basename sp in
   let _,dir,_ = repr_kn kn in
-  let () = check_exists sp in
-  let kn' = Global.add_constant dir id obj.cst_decl in
+  let kn' =
+    if obj.cst_was_seff then begin
+      obj.cst_was_seff <- false;  
+      if Global.exists_objlabel (Label.of_id (basename sp))
+      then constant_of_kn kn
+      else Errors.anomaly Pp.(str"Ex seff not found: " ++ Id.print(basename sp))
+    end else
+      let () = check_exists sp in
+      let kn', exported = Global.add_constant dir id obj.cst_decl in
+      obj.cst_exported <- exported;
+      kn' in
   assert (eq_constant kn' (constant_of_kn kn));
   Nametab.push (Nametab.Until 1) sp (ConstRef (constant_of_kn kn));
   let cst = Global.lookup_constant kn' in
@@ -156,20 +169,23 @@ let discharge_constant ((sp, kn), obj) =
   Some { obj with cst_hyps = new_hyps; cst_decl = new_decl; }
 
 (* Hack to reduce the size of .vo: we keep only what load/open needs *)
-let dummy_constant_entry =
-  ConstantEntry (ParameterEntry (None,false,(mkProp,Univ.UContext.empty),None))
+let dummy_constant_entry = 
+  ConstantEntry
+    (false, ParameterEntry (None,false,(mkProp,Univ.UContext.empty),None))
 
 let dummy_constant cst = {
   cst_decl = dummy_constant_entry;
   cst_hyps = [];
   cst_kind = cst.cst_kind;
   cst_locl = cst.cst_locl;
+  cst_exported = [];
+  cst_was_seff = cst.cst_was_seff;
 }
 
 let classify_constant cst = Substitute (dummy_constant cst)
 
-let inConstant : constant_obj -> obj =
-  declare_object { (default_object "CONSTANT") with
+let (inConstant, outConstant : (constant_obj -> obj) * (obj -> constant_obj)) =
+  declare_object_full { (default_object "CONSTANT") with
     cache_function = cache_constant;
     load_function = load_constant;
     open_function = open_constant;
@@ -177,16 +193,40 @@ let inConstant : constant_obj -> obj =
     subst_function = ident_subst_function;
     discharge_function = discharge_constant }
 
+let declare_scheme = ref (fun _ _ -> assert false)
+let set_declare_scheme f = declare_scheme := f
+
 let declare_constant_common id cst =
-  let (sp,kn) = add_leaf id (inConstant cst) in
+  let update_tables c =
+(*  Printf.eprintf "tables: %s\n%!" (Names.Constant.to_string c); *)
+    declare_constant_implicits c;
+    Heads.declare_head (EvalConstRef c);
+    Notation.declare_ref_arguments_scope (ConstRef c) in
+  let o = inConstant cst in
+  let _, kn as oname = add_leaf id o in
+  List.iter (fun (c,ce,role) ->
+      (* handling of private_constants just exported *)
+      let o = inConstant {
+        cst_decl = ConstantEntry (false, ce);
+        cst_hyps = [] ;
+        cst_kind = IsProof Theorem;
+        cst_locl = false;
+        cst_exported = [];
+        cst_was_seff = true; } in
+      let id = Label.to_id (pi3 (Constant.repr3 c)) in
+      ignore(add_leaf id o);
+      update_tables c;
+      match role with
+      | Safe_typing.Subproof -> ()
+      | Safe_typing.Schema (ind, kind) -> !declare_scheme kind [|ind,c|])
+    (outConstant o).cst_exported;
+  pull_to_head oname;
   let c = Global.constant_of_delta_kn kn in
-  declare_constant_implicits c;
-  Heads.declare_head (EvalConstRef c);
-  Notation.declare_ref_arguments_scope (ConstRef c);
+  update_tables c;
   c
 
 let definition_entry ?(opaque=false) ?(inline=false) ?types
-    ?(poly=false) ?(univs=Univ.UContext.empty) ?(eff=Declareops.no_seff) body =
+    ?(poly=false) ?(univs=Univ.UContext.empty) ?(eff=Safe_typing.empty_private_constants) body =
   { const_entry_body = Future.from_val ((body,Univ.ContextSet.empty), eff);
     const_entry_secctx = None;
     const_entry_type = types;
@@ -196,90 +236,25 @@ let definition_entry ?(opaque=false) ?(inline=false) ?types
     const_entry_feedback = None;
     const_entry_inline_code = inline}
 
-let declare_scheme = ref (fun _ _ -> assert false)
-let set_declare_scheme f = declare_scheme := f
-let declare_sideff env fix_exn se =
-  let cbl, scheme = match se with
-    | SEsubproof (c, cb, pt) -> [c, cb, pt], None
-    | SEscheme (cbl, k) ->
-        List.map (fun (_,c,cb,pt) -> c,cb,pt) cbl, Some (cbl,k) in
-  let id_of c = Names.Label.to_id (Names.Constant.label c) in
-  let pt_opaque_of cb pt =
-    match cb, pt with
-    | { const_body = Def sc }, _ -> (Mod_subst.force_constr sc, Univ.ContextSet.empty), false
-    | { const_body = OpaqueDef _ }, `Opaque(pt,univ) -> (pt, univ), true
-    | _ -> assert false
-  in
-  let ty_of cb =
-    match cb.Declarations.const_type with
-    | Declarations.RegularArity t -> Some t
-    | Declarations.TemplateArity _ -> None in
-  let cst_of cb pt =
-    let pt, opaque = pt_opaque_of cb pt in
-    let univs, subst =
-      if cb.const_polymorphic then
-	let univs = Univ.instantiate_univ_context cb.const_universes in
-	  univs, Vars.subst_instance_constr (Univ.UContext.instance univs)
-      else cb.const_universes, fun x -> x
-    in
-    let pt = (subst (fst pt), snd pt) in
-    let ty = Option.map subst (ty_of cb) in
-    { cst_decl = ConstantEntry (DefinitionEntry {
-        const_entry_body = Future.from_here ~fix_exn (pt, Declareops.no_seff);
-        const_entry_secctx = Some cb.Declarations.const_hyps;
-        const_entry_type = ty;
-        const_entry_opaque = opaque;
-        const_entry_inline_code = false;
-        const_entry_feedback = None;
-	const_entry_polymorphic = cb.const_polymorphic;
-	const_entry_universes = univs;
-    });
-    cst_hyps = [] ;
-    cst_kind =  Decl_kinds.IsDefinition Decl_kinds.Definition;
-    cst_locl = true;
-  } in
-  let exists c =
-    try ignore(Environ.lookup_constant c env); true
-    with Not_found -> false in
-  let knl =
-    CList.map_filter (fun (c,cb,pt) ->
-      if exists c then None
-      else Some (c,declare_constant_common (id_of c) (cst_of cb pt))) cbl in
-  match scheme with
-  | None -> ()
-  | Some (inds_consts,kind) ->
-      !declare_scheme kind (Array.of_list
-         (List.map (fun (c,kn) ->
-             CList.find_map (fun (x,c',_,_) ->
-               if Constant.equal c c' then Some (x,kn) else None) inds_consts)
-           knl))
-
 let declare_constant ?(internal = UserIndividualRequest) ?(local = false) id ?(export_seff=false) (cd, kind) =
-  let cd = (* We deal with side effects *)
+  let export = (* We deal with side effects *)
     match cd with
-    | Entries.DefinitionEntry de ->
-        if export_seff ||
-           not de.const_entry_opaque ||
-           de.const_entry_polymorphic then
+    | DefinitionEntry de when
+        export_seff ||
+        not de.const_entry_opaque ||
+        de.const_entry_polymorphic ->
           let bo = de.const_entry_body in
           let _, seff = Future.force bo in
-          if Declareops.side_effects_is_empty seff then cd
-          else begin
-            let seff = Declareops.uniquize_side_effects seff in
-            Declareops.iter_side_effects
-              (declare_sideff (Global.env ()) (Future.fix_exn_of bo)) seff;
-            Entries.DefinitionEntry { de with
-              const_entry_body = Future.chain ~pure:true bo (fun (pt, _) ->
-                pt, Declareops.no_seff) }
-        end
-        else cd
-    | _ -> cd
+          Safe_typing.empty_private_constants <> seff
+    | _ -> false
   in
   let cst = {
-    cst_decl = ConstantEntry cd;
+    cst_decl = ConstantEntry (export,cd);
     cst_hyps = [] ;
     cst_kind = kind;
     cst_locl = local;
+    cst_exported = [];
+    cst_was_seff = false;
   } in
   let kn = declare_constant_common id cst in
   kn
diff --git a/library/declare.mli b/library/declare.mli
index 7ed451c3f..fdbd23561 100644
--- a/library/declare.mli
+++ b/library/declare.mli
@@ -22,7 +22,7 @@ open Decl_kinds
 (** Declaration of local constructions (Variable/Hypothesis/Local) *)
 
 type section_variable_entry =
-  | SectionLocalDef of definition_entry
+  | SectionLocalDef of Safe_typing.private_constants definition_entry
   | SectionLocalAssum of types Univ.in_universe_context_set * polymorphic * bool (** Implicit status *)
 
 type variable_declaration = DirPath.t * section_variable_entry * logical_kind
@@ -32,7 +32,7 @@ val declare_variable : variable -> variable_declaration -> object_name
 (** Declaration of global constructions 
    i.e. Definition/Theorem/Axiom/Parameter/... *)
 
-type constant_declaration = constant_entry * logical_kind
+type constant_declaration = Safe_typing.private_constants constant_entry * logical_kind
 
 (** [declare_constant id cd] declares a global declaration
    (constant/parameter) with name [id] in the current section; it returns
@@ -49,8 +49,8 @@ type internal_flag =
 
 (* Defaut definition entries, transparent with no secctx or proj information *)
 val definition_entry : ?opaque:bool -> ?inline:bool -> ?types:types -> 
-  ?poly:polymorphic -> ?univs:Univ.universe_context -> ?eff:Declareops.side_effects ->
-  constr -> definition_entry
+  ?poly:polymorphic -> ?univs:Univ.universe_context ->
+  ?eff:Safe_typing.private_constants -> constr -> Safe_typing.private_constants definition_entry
 
 val declare_constant :
  ?internal:internal_flag -> ?local:bool -> Id.t -> ?export_seff:bool -> constant_declaration -> constant
@@ -60,7 +60,7 @@ val declare_definition :
   ?local:bool -> ?poly:polymorphic -> Id.t -> ?types:constr -> 
   constr Univ.in_universe_context_set -> constant
 
-(** Since transparent constant's side effects are globally declared, we
+(** Since transparent constants' side effects are globally declared, we
  *  need that *)
 val set_declare_scheme :
   (string -> (inductive * constant) array -> unit) -> unit
diff --git a/library/global.mli b/library/global.mli
index ac231f7fd..03469bea4 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -31,10 +31,11 @@ val set_engagement : Declarations.engagement -> unit
 (** Variables, Local definitions, constants, inductive types *)
 
 val push_named_assum : (Id.t * Constr.types * bool) Univ.in_universe_context_set -> unit
-val push_named_def   : (Id.t * Entries.definition_entry) -> Univ.universe_context_set
+val push_named_def   : (Id.t * Safe_typing.private_constants Entries.definition_entry) -> Univ.universe_context_set
 
 val add_constant :
-  DirPath.t -> Id.t -> Safe_typing.global_declaration -> constant
+  DirPath.t -> Id.t -> Safe_typing.global_declaration ->
+    constant * Safe_typing.exported_private_constant list
 val add_mind :
   DirPath.t -> Id.t -> Entries.mutual_inductive_entry -> mutual_inductive
 
diff --git a/library/heads.ml b/library/heads.ml
index 5c153b067..73d2aa053 100644
--- a/library/heads.ml
+++ b/library/heads.ml
@@ -68,7 +68,10 @@ let kind_of_head env t =
         | None -> NotImmediatelyComputableHead)
   | Const (cst,_) ->
       (try on_subterm k l b (constant_head cst)
-       with Not_found -> assert false)
+       with Not_found ->
+         Errors.anomaly
+           Pp.(str "constant not found in kind_of_head: " ++
+               str (Names.Constant.to_string cst)))
   | Construct _ | CoFix _ ->
       if b then NotImmediatelyComputableHead else ConstructorHead
   | Sort _ | Ind _ | Prod _ -> RigidHead RigidType
diff --git a/library/libobject.ml b/library/libobject.ml
index 2ee57baf9..85c830ea2 100644
--- a/library/libobject.ml
+++ b/library/libobject.ml
@@ -108,6 +108,9 @@ let declare_object_full odecl =
 let declare_object odecl =
   try fst (declare_object_full odecl)
   with e -> Errors.fatal_error (Errors.print e) (Errors.is_anomaly e)
+let declare_object_full odecl =
+  try declare_object_full odecl
+  with e -> Errors.fatal_error (Errors.print e) (Errors.is_anomaly e)
 
 let missing_tab = (Hashtbl.create 17 : (string, unit) Hashtbl.t)
 
diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml
index c232ae31a..d6c29283f 100644
--- a/plugins/derive/derive.ml
+++ b/plugins/derive/derive.ml
@@ -6,8 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-let map_const_entry_body (f:Term.constr->Term.constr) (x:Entries.const_entry_body)
-    : Entries.const_entry_body =
+let map_const_entry_body (f:Term.constr->Term.constr) (x:Safe_typing.private_constants Entries.const_entry_body)
+    : Safe_typing.private_constants Entries.const_entry_body =
   Future.chain ~pure:true x begin fun ((b,ctx),fx) ->
     (f b , ctx) , fx
   end
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 9e27ddf2e..c43932324 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -334,7 +334,7 @@ let generate_functional_principle (evd: Evd.evar_map ref)
 	ignore(
 	  Declare.declare_constant
 	    name
-	    (Entries.DefinitionEntry ce,
+	    (DefinitionEntry ce,
 	     Decl_kinds.IsDefinition (Decl_kinds.Scheme))
 	);
 	Declare.definition_message name;
@@ -447,7 +447,7 @@ let get_funs_constant mp dp =
 exception No_graph_found
 exception Found_type of int
 
-let make_scheme evd (fas : (pconstant*glob_sort) list) : Entries.definition_entry list =
+let make_scheme evd (fas : (pconstant*glob_sort) list) : Safe_typing.private_constants definition_entry list =
   let env = Global.env () in
   let funs = List.map fst fas in
   let first_fun = List.hd funs in
@@ -541,7 +541,7 @@ let make_scheme evd (fas : (pconstant*glob_sort) list) : Entries.definition_entr
       let sorts = Array.of_list sorts in
       List.map (compute_new_princ_type_from_rel funs sorts) other_princ_types
     in
-    let first_princ_body,first_princ_type = const.Entries.const_entry_body, const.Entries.const_entry_type in
+    let first_princ_body,first_princ_type = const.const_entry_body, const.const_entry_type in
     let ctxt,fix = decompose_lam_assum (fst(fst(Future.force first_princ_body))) in (* the principle has for forall ...., fix .*)
     let (idxs,_),(_,ta,_ as decl) = destFix fix in
     let other_result =
@@ -585,9 +585,9 @@ let make_scheme evd (fas : (pconstant*glob_sort) list) : Entries.definition_entr
 	     Termops.it_mkLambda_or_LetIn (mkFix((idxs,i),decl)) ctxt
 	   in
 	   {const with
-	      Entries.const_entry_body = 
-                (Future.from_val (Term_typing.mk_pure_proof princ_body));
-	      Entries.const_entry_type = Some scheme_type
+	      const_entry_body = 
+                (Future.from_val (Safe_typing.mk_pure_proof princ_body));
+	      const_entry_type = Some scheme_type
 	   }
       )
       other_fun_princ_types
@@ -620,7 +620,7 @@ let build_scheme fas =
        ignore
 	 (Declare.declare_constant
 	    princ_id
-	    (Entries.DefinitionEntry def_entry,Decl_kinds.IsProof Decl_kinds.Theorem));
+	    (DefinitionEntry def_entry,Decl_kinds.IsProof Decl_kinds.Theorem));
        Declare.definition_message princ_id
     )
     fas
diff --git a/plugins/funind/functional_principles_types.mli b/plugins/funind/functional_principles_types.mli
index f6e5578d2..bc082f073 100644
--- a/plugins/funind/functional_principles_types.mli
+++ b/plugins/funind/functional_principles_types.mli
@@ -1,3 +1,11 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
 open Names
 open Term
 open Misctypes
@@ -29,7 +37,7 @@ val compute_new_princ_type_from_rel : constr array -> sorts array ->
 exception No_graph_found
 
 val make_scheme :   Evd.evar_map ref ->
- (pconstant*glob_sort) list -> Entries.definition_entry list
+ (pconstant*glob_sort) list -> Safe_typing.private_constants Entries.definition_entry list
 
 val build_scheme : (Id.t*Libnames.reference*glob_sort) list ->  unit
 val build_case_scheme : (Id.t*Libnames.reference*glob_sort)  ->  unit
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 35bd1c36d..aa47e2619 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -149,7 +149,7 @@ let get_locality = function
 | Global -> false
 
 let save with_clean id const (locality,_,kind) hook =
-  let fix_exn = Future.fix_exn_of const.Entries.const_entry_body in
+  let fix_exn = Future.fix_exn_of const.const_entry_body in
   let l,r = match locality with
     | Discharge when Lib.sections_are_opened () ->
         let k = Kindops.logical_kind_of_goal_kind kind in
diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli
index 10daf6e84..23f1da1ba 100644
--- a/plugins/funind/indfun_common.mli
+++ b/plugins/funind/indfun_common.mli
@@ -46,7 +46,7 @@ val const_of_id: Id.t ->  Globnames.global_reference(* constantyes *)
 val jmeq : unit -> Term.constr
 val jmeq_refl : unit -> Term.constr
 
-val save : bool -> Id.t -> Entries.definition_entry  -> Decl_kinds.goal_kind ->
+val save : bool -> Id.t -> Safe_typing.private_constants Entries.definition_entry  -> Decl_kinds.goal_kind ->
   unit Lemmas.declaration_hook Ephemeron.key -> unit
 
 (* [get_proof_clean do_reduce] : returns the proof name, definition, kind and hook and
@@ -54,7 +54,7 @@ val save : bool -> Id.t -> Entries.definition_entry  -> Decl_kinds.goal_kind ->
 *)
 val get_proof_clean : bool ->
   Names.Id.t *
-    (Entries.definition_entry * Decl_kinds.goal_kind)
+    (Safe_typing.private_constants Entries.definition_entry * Decl_kinds.goal_kind)
 
 
 
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 1107c2951..0593bbca8 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -579,7 +579,7 @@ type evar_map = {
   (** Metas *)
   metas      : clbinding Metamap.t;
   (** Interactive proofs *)
-  effects    : Declareops.side_effects;
+  effects    : Safe_typing.private_constants;
   future_goals : Evar.t list; (** list of newly created evars, to be
                                   eventually turned into goals if not solved.*)
   principal_future_goal : Evar.t option; (** if [Some e], [e] must be
@@ -768,7 +768,7 @@ let empty = {
   conv_pbs   = [];
   last_mods  = Evar.Set.empty;
   metas      = Metamap.empty;
-  effects    = Declareops.no_seff;
+  effects    = Safe_typing.empty_private_constants;
   evar_names = (EvMap.empty,Idmap.empty); (* id<->key for undefined evars *)
   future_goals = [];
   principal_future_goal = None;
@@ -1041,22 +1041,8 @@ let with_context_set rigid d (a, ctx) =
   (merge_context_set rigid d ctx, a)
 
 let emit_universe_side_effects eff u =
-  Declareops.fold_side_effects
-    (fun acc eff ->
-     match eff with
-     | Declarations.SEscheme (l,s) ->
-	List.fold_left
-	  (fun acc (_,_,cb,c) ->
-	   let acc = match c with
-	     | `Nothing -> acc
-	     | `Opaque (s, ctx) -> merge_uctx true univ_rigid acc ctx
-	   in if cb.Declarations.const_polymorphic then acc
-	      else
-		merge_uctx true univ_rigid acc
-			   (Univ.ContextSet.of_context cb.Declarations.const_universes))
-	  acc l
-     | Declarations.SEsubproof _ -> acc)
-    u eff
+  let uctxs = Safe_typing.universes_of_private eff in
+  List.fold_left (merge_uctx true univ_rigid) u uctxs
         
 let add_uctx_names s l (names, names_rev) =
     (UNameMap.add s l names, Univ.LMap.add l s names_rev)
@@ -1399,11 +1385,11 @@ let e_eq_constr_univs evdref t u =
 (* Side effects *)
 
 let emit_side_effects eff evd =
-  { evd with effects = Declareops.union_side_effects eff evd.effects;
+  { evd with effects = Safe_typing.concat_private eff evd.effects;
 	     universes = emit_universe_side_effects eff evd.universes }
 
 let drop_side_effects evd =
-  { evd with effects = Declareops.no_seff; }
+  { evd with effects = Safe_typing.empty_private_constants; }
 
 let eval_side_effects evd = evd.effects
 
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index 52d7d4212..9379b50b5 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -261,10 +261,10 @@ val dependent_evar_ident : existential_key -> evar_map -> Id.t
 
 (** {5 Side-effects} *)
 
-val emit_side_effects : Declareops.side_effects -> evar_map -> evar_map
+val emit_side_effects : Safe_typing.private_constants -> evar_map -> evar_map
 (** Push a side-effect into the evar map. *)
 
-val eval_side_effects : evar_map -> Declareops.side_effects
+val eval_side_effects : evar_map -> Safe_typing.private_constants
 (** Return the effects contained in the evar map. *)
 
 val drop_side_effects : evar_map -> evar_map
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 00ef8ecaf..02dbd1fdc 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -150,10 +150,14 @@ let build_by_tactic ?(side_eff=true) env ctx ?(poly=false) typ tac =
   let sign = val_of_named_context (named_context env) in
   let gk = Global, poly, Proof Theorem in
   let ce, status, univs = build_constant_by_tactic id ctx sign ~goal_kind:gk typ tac in
-  let ce = if side_eff then Term_typing.handle_entry_side_effects env ce else { ce with const_entry_body = Future.chain ~pure:true ce.const_entry_body (fun (pt, _) -> pt, Declareops.no_seff) } in
+  let ce =
+    if side_eff then Safe_typing.inline_private_constants_in_definition_entry env ce
+    else { ce with
+      const_entry_body = Future.chain ~pure:true ce.const_entry_body
+        (fun (pt, _) -> pt, Safe_typing.empty_private_constants) } in
   let (cb, ctx), se = Future.force ce.const_entry_body in
   let univs' = Evd.merge_context_set Evd.univ_rigid (Evd.from_ctx univs) ctx in
-  assert(Declareops.side_effects_is_empty se);
+  assert(Safe_typing.empty_private_constants = se);
   cb, status, Evd.evar_universe_context univs'
 
 let refine_by_tactic env sigma ty tac =
@@ -188,7 +192,7 @@ let refine_by_tactic env sigma ty tac =
       other goals that were already present during its invocation, so that
       those goals rely on effects that are not present anymore. Hopefully,
       this hack will work in most cases. *)
-  let ans = Term_typing.handle_side_effects env ans neff in
+  let ans = Safe_typing.inline_private_constants_in_constr env ans neff in
   ans, sigma
 
 (**********************************************************************)
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index b1fba132d..fc521ea43 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -69,11 +69,11 @@ val start_proof :
 val cook_this_proof :
     Proof_global.proof_object ->
   (Id.t *
-    (Entries.definition_entry * Proof_global.proof_universes * goal_kind))
+    (Safe_typing.private_constants Entries.definition_entry * Proof_global.proof_universes * goal_kind))
 
 val cook_proof : unit ->
   (Id.t *
-    (Entries.definition_entry * Proof_global.proof_universes * goal_kind))
+    (Safe_typing.private_constants Entries.definition_entry * Proof_global.proof_universes * goal_kind))
 
 (** {6 ... } *)
 (** [get_pftreestate ()] returns the current focused pending proof.
@@ -152,7 +152,7 @@ val instantiate_nth_evar_com : int -> Constrexpr.constr_expr -> unit
 val build_constant_by_tactic :
   Id.t -> Evd.evar_universe_context -> named_context_val -> ?goal_kind:goal_kind ->
   types -> unit Proofview.tactic -> 
-  Entries.definition_entry * bool * Evd.evar_universe_context
+  Safe_typing.private_constants Entries.definition_entry * bool * Evd.evar_universe_context
 
 val build_by_tactic : ?side_eff:bool -> env -> Evd.evar_universe_context -> ?poly:polymorphic ->
   types -> unit Proofview.tactic -> 
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index a0ead42ef..809ed41c7 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -67,7 +67,7 @@ type proof_universes = Evd.evar_universe_context
 
 type proof_object = {
   id : Names.Id.t;
-  entries : Entries.definition_entry list;
+  entries : Safe_typing.private_constants Entries.definition_entry list;
   persistence : Decl_kinds.goal_kind;
   universes: proof_universes;
   (* constraints : Univ.constraints; *)
@@ -315,13 +315,14 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now fpl =
         let open Universes in
         let body = c in
 	let typ =
-	  if not (keep_body_ucst_separate || not (Declareops.side_effects_is_empty eff)) then
+	  if not (keep_body_ucst_separate || not (Safe_typing.empty_private_constants = eff)) then
 	    nf t
 	  else t
 	in
         let used_univs_body = Universes.universes_of_constr body in
         let used_univs_typ = Universes.universes_of_constr typ in
-        if keep_body_ucst_separate || not (Declareops.side_effects_is_empty eff) then
+        if keep_body_ucst_separate ||
+           not (Safe_typing.empty_private_constants = eff) then
           let initunivs = Evd.evar_context_universe_context initial_euctx in
           let ctx = Evd.evar_universe_context_set initunivs universes in
           (* For vi2vo compilation proofs are computed now but we need to
@@ -365,7 +366,7 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now fpl =
   { id = pid; entries = entries; persistence = strength; universes = universes },
   fun pr_ending -> Ephemeron.get terminator pr_ending
 
-type closed_proof_output = (Term.constr * Declareops.side_effects) list * Evd.evar_universe_context
+type closed_proof_output = (Term.constr * Safe_typing.private_constants) list * Evd.evar_universe_context
 
 let return_proof ?(allow_partial=false) () =
  let { pid; proof; strength = (_,poly,_) } = cur_pstate () in
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index fcb706cc8..f8615e849 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -58,7 +58,7 @@ type lemma_possible_guards = int list list
 type proof_universes = Evd.evar_universe_context
 type proof_object = {
   id : Names.Id.t;
-  entries : Entries.definition_entry list;
+  entries : Safe_typing.private_constants Entries.definition_entry list;
   persistence : Decl_kinds.goal_kind;
   universes: proof_universes;
   (* constraints : Univ.constraints; *)
@@ -97,7 +97,7 @@ val close_proof : keep_body_ucst_separate:bool -> Future.fix_exn -> closed_proof
  * Both access the current proof state. The former is supposed to be
  * chained with a computation that completed the proof *)
 
-type closed_proof_output = (Term.constr * Declareops.side_effects) list * Evd.evar_universe_context
+type closed_proof_output = (Term.constr * Safe_typing.private_constants) list * Evd.evar_universe_context
 
 (* If allow_partial is set (default no) then an incomplete proof
  * is allowed (no error), and a warn is given if the proof is complete. *)
diff --git a/proofs/proofview.mli b/proofs/proofview.mli
index 5a9e7f39f..927df33a0 100644
--- a/proofs/proofview.mli
+++ b/proofs/proofview.mli
@@ -336,7 +336,7 @@ val tclENV : Environ.env tactic
 (** {7 Put-like primitives} *)
 
 (** [tclEFFECTS eff] add the effects [eff] to the current state. *)
-val tclEFFECTS : Declareops.side_effects -> unit tactic
+val tclEFFECTS : Safe_typing.private_constants -> unit tactic
 
 (** [mark_as_unsafe] declares the current tactic is unsafe. *)
 val mark_as_unsafe : unit tactic
diff --git a/stm/lemmas.ml b/stm/lemmas.ml
index c49ddfd8e..6c1832688 100644
--- a/stm/lemmas.ml
+++ b/stm/lemmas.ml
@@ -70,11 +70,12 @@ let adjust_guardness_conditions const = function
                   try ignore(Environ.lookup_constant c e); true
                   with Not_found -> false in 
                 if exists c e then e else Environ.add_constant c cb e in
-              let env = Declareops.fold_side_effects (fun env -> function
+              let env = List.fold_left (fun env { eff } ->
+                match eff with
                 | SEsubproof (c, cb,_) -> add c cb env
                 | SEscheme (l,_) ->
                     List.fold_left (fun e (_,c,cb,_) -> add c cb e) env l)
-                env (Declareops.uniquize_side_effects eff) in
+                env (Safe_typing.side_effects_of_private_constants eff) in
               let indexes =
 	        search_guard Loc.ghost env
                   possible_indexes fixdecls in
diff --git a/tactics/elimschemes.ml b/tactics/elimschemes.ml
index e6a8cbe3a..8a6d93cf7 100644
--- a/tactics/elimschemes.ml
+++ b/tactics/elimschemes.ml
@@ -52,7 +52,7 @@ let optimize_non_type_induction_scheme kind dep sort _ ind =
     let ctxset = Univ.ContextSet.of_context ctx in
     let ectx = Evd.evar_universe_context_of ctxset in
     let sigma, c = build_induction_scheme env (Evd.from_ctx ectx) (ind,u) dep sort in
-      (c, Evd.evar_universe_context sigma), Declareops.no_seff
+      (c, Evd.evar_universe_context sigma), Safe_typing.empty_private_constants
 
 let build_induction_scheme_in_type dep sort ind =
   let env = Global.env () in
@@ -68,15 +68,15 @@ let build_induction_scheme_in_type dep sort ind =
  
 let rect_scheme_kind_from_type =
   declare_individual_scheme_object "_rect_nodep"
-    (fun _ x -> build_induction_scheme_in_type false InType x, Declareops.no_seff)
+    (fun _ x -> build_induction_scheme_in_type false InType x, Safe_typing.empty_private_constants)
 
 let rect_scheme_kind_from_prop =
   declare_individual_scheme_object "_rect" ~aux:"_rect_from_prop"
-    (fun _ x -> build_induction_scheme_in_type false InType x, Declareops.no_seff)
+    (fun _ x -> build_induction_scheme_in_type false InType x, Safe_typing.empty_private_constants)
 
 let rect_dep_scheme_kind_from_type =
   declare_individual_scheme_object "_rect" ~aux:"_rect_from_type"
-    (fun _ x -> build_induction_scheme_in_type true InType x, Declareops.no_seff)
+    (fun _ x -> build_induction_scheme_in_type true InType x, Safe_typing.empty_private_constants)
 
 let ind_scheme_kind_from_type =
   declare_individual_scheme_object "_ind_nodep"
@@ -109,24 +109,24 @@ let build_case_analysis_scheme_in_type dep sort ind =
 
 let case_scheme_kind_from_type =
   declare_individual_scheme_object "_case_nodep"
-  (fun _ x -> build_case_analysis_scheme_in_type false InType x, Declareops.no_seff)
+  (fun _ x -> build_case_analysis_scheme_in_type false InType x, Safe_typing.empty_private_constants)
 
 let case_scheme_kind_from_prop =
   declare_individual_scheme_object "_case" ~aux:"_case_from_prop"
-  (fun _ x -> build_case_analysis_scheme_in_type false InType x, Declareops.no_seff)
+  (fun _ x -> build_case_analysis_scheme_in_type false InType x, Safe_typing.empty_private_constants)
 
 let case_dep_scheme_kind_from_type =
   declare_individual_scheme_object "_case" ~aux:"_case_from_type"
-  (fun _ x -> build_case_analysis_scheme_in_type true InType x, Declareops.no_seff)
+  (fun _ x -> build_case_analysis_scheme_in_type true InType x, Safe_typing.empty_private_constants)
 
 let case_dep_scheme_kind_from_type_in_prop =
   declare_individual_scheme_object "_casep_dep"
-  (fun _ x -> build_case_analysis_scheme_in_type true InProp x, Declareops.no_seff)
+  (fun _ x -> build_case_analysis_scheme_in_type true InProp x, Safe_typing.empty_private_constants)
 
 let case_dep_scheme_kind_from_prop =
   declare_individual_scheme_object "_case_dep"
-  (fun _ x -> build_case_analysis_scheme_in_type true InType x, Declareops.no_seff)
+  (fun _ x -> build_case_analysis_scheme_in_type true InType x, Safe_typing.empty_private_constants)
 
 let case_dep_scheme_kind_from_prop_in_prop =
   declare_individual_scheme_object "_casep"
-  (fun _ x -> build_case_analysis_scheme_in_type true InProp x, Declareops.no_seff)
+  (fun _ x -> build_case_analysis_scheme_in_type true InProp x, Safe_typing.empty_private_constants)
diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml
index f7d3ad5d0..b2603315d 100644
--- a/tactics/eqschemes.ml
+++ b/tactics/eqschemes.ml
@@ -193,7 +193,7 @@ let sym_scheme_kind =
   declare_individual_scheme_object "_sym_internal"
   (fun _ ind ->
     let c, ctx = build_sym_scheme (Global.env() (* side-effect! *)) ind in
-      (c, ctx), Declareops.no_seff)
+      (c, ctx), Safe_typing.empty_private_constants)
 
 (**********************************************************************)
 (* Build the involutivity of symmetry for an inductive type           *)
@@ -412,7 +412,8 @@ let build_l2r_rew_scheme dep env ind kind =
        [|main_body|])
    else
      main_body))))))
-  in (c, Evd.evar_universe_context_of ctx), Declareops.union_side_effects eff' eff
+  in (c, Evd.evar_universe_context_of ctx),
+      Safe_typing.concat_private eff' eff
 
 (**********************************************************************)
 (* Build the left-to-right rewriting lemma for hypotheses associated  *)
@@ -660,7 +661,7 @@ let rew_l2r_dep_scheme_kind =
 (**********************************************************************)
 let rew_r2l_dep_scheme_kind =
   declare_individual_scheme_object "_rew_dep"
-  (fun _ ind -> build_r2l_rew_scheme true (Global.env()) ind InType,Declareops.no_seff)
+  (fun _ ind -> build_r2l_rew_scheme true (Global.env()) ind InType,Safe_typing.empty_private_constants)
 
 (**********************************************************************)
 (* Dependent rewrite from right-to-left in hypotheses                 *)
@@ -670,7 +671,7 @@ let rew_r2l_dep_scheme_kind =
 (**********************************************************************)
 let rew_r2l_forward_dep_scheme_kind =
   declare_individual_scheme_object "_rew_fwd_dep"
-  (fun _ ind -> build_r2l_forward_rew_scheme true (Global.env()) ind InType,Declareops.no_seff)
+  (fun _ ind -> build_r2l_forward_rew_scheme true (Global.env()) ind InType,Safe_typing.empty_private_constants)
 
 (**********************************************************************)
 (* Dependent rewrite from left-to-right in hypotheses                 *)
@@ -680,7 +681,7 @@ let rew_r2l_forward_dep_scheme_kind =
 (**********************************************************************)
 let rew_l2r_forward_dep_scheme_kind =
   declare_individual_scheme_object "_rew_fwd_r_dep"
-  (fun _ ind -> build_l2r_forward_rew_scheme true (Global.env()) ind InType,Declareops.no_seff)
+  (fun _ ind -> build_l2r_forward_rew_scheme true (Global.env()) ind InType,Safe_typing.empty_private_constants)
 
 (**********************************************************************)
 (* Non-dependent rewrite from either left-to-right in conclusion or   *)
@@ -694,7 +695,7 @@ let rew_l2r_forward_dep_scheme_kind =
 let rew_l2r_scheme_kind =
   declare_individual_scheme_object "_rew_r"
   (fun _ ind -> fix_r2l_forward_rew_scheme
-     (build_r2l_forward_rew_scheme false (Global.env()) ind InType), Declareops.no_seff)
+     (build_r2l_forward_rew_scheme false (Global.env()) ind InType), Safe_typing.empty_private_constants)
 
 (**********************************************************************)
 (* Non-dependent rewrite from either right-to-left in conclusion or   *)
@@ -704,7 +705,7 @@ let rew_l2r_scheme_kind =
 (**********************************************************************)
 let rew_r2l_scheme_kind =
   declare_individual_scheme_object "_rew"
-  (fun _ ind -> build_r2l_rew_scheme false (Global.env()) ind InType, Declareops.no_seff)
+  (fun _ ind -> build_r2l_rew_scheme false (Global.env()) ind InType, Safe_typing.empty_private_constants)
 
 (* End of rewriting schemes *)
 
@@ -782,4 +783,4 @@ let build_congr env (eq,refl,ctx) ind =
 let congr_scheme_kind = declare_individual_scheme_object "_congr"
   (fun _ ind ->
     (* May fail if equality is not defined *)
-    build_congr (Global.env()) (get_coq_eq Univ.ContextSet.empty) ind, Declareops.no_seff)
+    build_congr (Global.env()) (get_coq_eq Univ.ContextSet.empty) ind, Safe_typing.empty_private_constants)
diff --git a/tactics/eqschemes.mli b/tactics/eqschemes.mli
index 6bb84808a..3fe330730 100644
--- a/tactics/eqschemes.mli
+++ b/tactics/eqschemes.mli
@@ -25,7 +25,7 @@ val rew_r2l_scheme_kind : individual scheme_kind
 val build_r2l_rew_scheme : bool -> env -> inductive -> sorts_family -> 
   constr Evd.in_evar_universe_context
 val build_l2r_rew_scheme : bool -> env -> inductive -> sorts_family -> 
-  constr Evd.in_evar_universe_context * Declareops.side_effects
+  constr Evd.in_evar_universe_context * Safe_typing.private_constants
 val build_r2l_forward_rew_scheme :
   bool -> env -> inductive -> sorts_family -> constr Evd.in_evar_universe_context
 val build_l2r_forward_rew_scheme :
@@ -37,7 +37,7 @@ val build_sym_scheme : env -> inductive -> constr Evd.in_evar_universe_context
 val sym_scheme_kind : individual scheme_kind
 
 val build_sym_involutive_scheme : env -> inductive -> 
-  constr Evd.in_evar_universe_context * Declareops.side_effects
+  constr Evd.in_evar_universe_context * Safe_typing.private_constants
 val sym_involutive_scheme_kind : individual scheme_kind
 
 (** Builds a congruence scheme for an equality type *)
diff --git a/tactics/equality.ml b/tactics/equality.ml
index bc711b81e..674c85af7 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -317,7 +317,7 @@ let find_elim hdcncl lft2rgt dep cls ot gl =
 	assert false
     in
       let sigma, elim = Evd.fresh_global (Global.env ()) (Proofview.Goal.sigma gl) (ConstRef c) in
-	sigma, elim, Declareops.no_seff
+	sigma, elim, Safe_typing.empty_private_constants
   else
   let scheme_name = match dep, lft2rgt, inccl with
     (* Non dependent case *)
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 1437b2462..0b920066f 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -4455,9 +4455,9 @@ let abstract_subproof id gk tac =
   (* let evd, lem = Evd.fresh_global (Global.env ()) evd (ConstRef cst) in *)
   let lem, ctx = Universes.unsafe_constr_of_global (ConstRef cst) in
   let evd = Evd.set_universe_context evd ectx in
-  let open Declareops in
-  let eff = Safe_typing.sideff_of_con (Global.safe_env ()) cst in
-  let effs = cons_side_effects eff
+  let open Safe_typing in
+  let eff = private_con_of_con (Global.safe_env ()) cst in
+  let effs = add_private eff
     Entries.(snd (Future.force const.const_entry_body)) in
   let args = List.rev (instance_from_named_context sign) in
   let solve =
diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml
index 8ac273c84..7a89b9f54 100644
--- a/toplevel/auto_ind_decl.ml
+++ b/toplevel/auto_ind_decl.ml
@@ -179,12 +179,12 @@ let build_beq_scheme mode kn =
       let rec aux c =
 	let (c,a) = Reductionops.whd_betaiota_stack Evd.empty c in
 	match kind_of_term c with
-        | Rel x -> mkRel (x-nlist+ndx), Declareops.no_seff
-        | Var x -> mkVar (id_of_string ("eq_"^(string_of_id x))), Declareops.no_seff
+        | Rel x -> mkRel (x-nlist+ndx), Safe_typing.empty_private_constants
+        | Var x -> mkVar (id_of_string ("eq_"^(string_of_id x))), Safe_typing.empty_private_constants
         | Cast (x,_,_) -> aux (applist (x,a))
         | App _ -> assert false
         | Ind ((kn',i as ind'),u) (*FIXME: universes *) -> 
-            if eq_mind kn kn' then mkRel(eqA-nlist-i+nb_ind-1), Declareops.no_seff
+            if eq_mind kn kn' then mkRel(eqA-nlist-i+nb_ind-1), Safe_typing.empty_private_constants
             else begin
               try
                 let eq, eff =
@@ -193,9 +193,8 @@ let build_beq_scheme mode kn =
                 let eqa, eff =
                   let eqa, effs = List.split (List.map aux a) in
                   Array.of_list eqa,
-                  Declareops.union_side_effects
-                    (Declareops.flatten_side_effects (List.rev effs))
-                    eff in
+                  List.fold_left Safe_typing.concat_private eff (List.rev effs)
+                  in
                 let args =
                   Array.append 
                     (Array.of_list (List.map (fun x -> lift lifti x) a)) eqa in
@@ -238,7 +237,7 @@ let build_beq_scheme mode kn =
     let constrsi = constrs (3+nparrec) in
     let n = Array.length constrsi in
     let ar = Array.make n (Lazy.force ff) in
-    let eff = ref Declareops.no_seff in
+    let eff = ref Safe_typing.empty_private_constants in
 	for i=0 to n-1 do
 	  let nb_cstr_args = List.length constrsi.(i).cs_args in
 	  let ar2 = Array.make n (Lazy.force ff) in
@@ -256,7 +255,7 @@ let build_beq_scheme mode kn =
                                           (nb_cstr_args+ndx+1)
                                           cc
                           in
-                          eff := Declareops.union_side_effects eff' !eff;
+                          eff := Safe_typing.concat_private eff' !eff;
                           Array.set eqs ndx
                               (mkApp (eqA,
                                 [|mkRel (ndx+1+nb_cstr_args);mkRel (ndx+1)|]
@@ -288,7 +287,7 @@ let build_beq_scheme mode kn =
     let names = Array.make nb_ind Anonymous and
         types = Array.make nb_ind mkSet and
         cores = Array.make nb_ind mkSet in
-    let eff = ref Declareops.no_seff in
+    let eff = ref Safe_typing.empty_private_constants in
     let u = Univ.Instance.empty in
     for i=0 to (nb_ind-1) do
         names.(i) <- Name (Id.of_string (rec_name i));
@@ -296,7 +295,7 @@ let build_beq_scheme mode kn =
                      (mkArrow (mkFullInd ((kn,i),u) 1) (Lazy.force bb));
         let c, eff' = make_one_eq i in
         cores.(i) <- c;
-        eff := Declareops.union_side_effects eff' !eff
+        eff := Safe_typing.concat_private eff' !eff
     done;
       (Array.init nb_ind (fun i ->
       let kelim = Inductive.elim_sorts (mib,mib.mind_packets.(i)) in
@@ -875,7 +874,7 @@ let compute_dec_tact ind lnamesparrec nparrec =
     Not_found ->
       Tacticals.New.tclZEROMSG (str "Error during the decidability part, leibniz to boolean equality is required.")
   end >>= fun (lbI,eff'') ->
-  let eff = (Declareops.union_side_effects eff'' (Declareops.union_side_effects eff' eff)) in
+  let eff = (Safe_typing.concat_private eff'' (Safe_typing.concat_private eff' eff)) in
   Tacticals.New.tclTHENLIST [
         Proofview.tclEFFECTS eff;
         intros_using fresh_first_intros;
@@ -942,7 +941,7 @@ let make_eq_decidability mode mind =
     (compute_dec_goal (ind,u) lnamesparrec nparrec)
     (compute_dec_tact ind lnamesparrec nparrec)
   in
-  ([|ans|], ctx), Declareops.no_seff
+  ([|ans|], ctx), Safe_typing.empty_private_constants
 
 let eq_dec_scheme_kind =
   declare_mutual_scheme_object "_eq_dec" make_eq_decidability
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 805a29e39..e750f0ca2 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -187,7 +187,7 @@ let new_instance ?(abstract=false) ?(global=false) poly ctx (instid, bk, cl) pro
 	Evarutil.check_evars env Evd.empty !evars termtype;
 	let ctx = Evd.universe_context !evars in
 	let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest id
-	  (Entries.ParameterEntry 
+	  (ParameterEntry 
             (None,poly,(termtype,ctx),None), Decl_kinds.IsAssumption Decl_kinds.Logical)
 	in instance_hook k None global imps ?hook (ConstRef cst); id
       end
diff --git a/toplevel/command.ml b/toplevel/command.ml
index d75efeca1..433ef4dcc 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -169,7 +169,7 @@ let declare_definition ident (local, p, k) ce imps hook =
     gr
   | Discharge | Local | Global ->
     declare_global_definition ident ce local k imps in
-  Lemmas.call_hook (Future.fix_exn_of ce.Entries.const_entry_body) hook local r
+  Lemmas.call_hook (Future.fix_exn_of ce.const_entry_body) hook local r
 
 let _ = Obligations.declare_definition_ref := declare_definition
 
@@ -178,7 +178,7 @@ let do_definition ident k pl bl red_option c ctypopt hook =
     if Flags.is_program_mode () then
       let env = Global.env () in
       let (c,ctx), sideff = Future.force ce.const_entry_body in
-      assert(Declareops.side_effects_is_empty sideff);
+      assert(Safe_typing.empty_private_constants = sideff);
       assert(Univ.ContextSet.is_empty ctx);
       let typ = match ce.const_entry_type with 
 	| Some t -> t
@@ -1139,7 +1139,7 @@ let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) ind
       List.map_i (fun i _ -> mkFix ((indexes,i),fixdecls)) 0 fixnames in
     let evd = Evd.from_ctx ctx in
     let evd = Evd.restrict_universe_context evd vars in
-    let fixdecls = List.map Term_typing.mk_pure_proof fixdecls in
+    let fixdecls = List.map Safe_typing.mk_pure_proof fixdecls in
     let ctx = Evd.universe_context ?names:pl evd in
     ignore (List.map4 (declare_fix (local, poly, Fixpoint) ctx)
 	      fixnames fixdecls fixtypes fiximps);
@@ -1169,7 +1169,7 @@ let declare_cofixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) n
     let fixdecls = prepare_recursive_declaration fixnames fixtypes fixdefs in
     let fixdecls = List.map_i (fun i _ -> mkCoFix (i,fixdecls)) 0 fixnames in
     let vars = Universes.universes_of_constr (List.hd fixdecls) in
-    let fixdecls = List.map Term_typing.mk_pure_proof fixdecls in
+    let fixdecls = List.map Safe_typing.mk_pure_proof fixdecls in
     let fiximps = List.map (fun (len,imps,idx) -> imps) fiximps in
     let evd = Evd.from_ctx ctx in
     let evd = Evd.restrict_universe_context evd vars in
diff --git a/toplevel/command.mli b/toplevel/command.mli
index 94b4af9dd..a031677b4 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -26,17 +26,17 @@ val do_constraint : polymorphic ->
 
 (** {6 Hooks for Pcoq} *)
 
-val set_declare_definition_hook : (definition_entry -> unit) -> unit
-val get_declare_definition_hook : unit -> (definition_entry -> unit)
+val set_declare_definition_hook : (Safe_typing.private_constants definition_entry -> unit) -> unit
+val get_declare_definition_hook : unit -> (Safe_typing.private_constants definition_entry -> unit)
 
 (** {6 Definitions/Let} *)
 
 val interp_definition :
   lident list option -> local_binder list -> polymorphic -> red_expr option -> constr_expr ->
-  constr_expr option -> definition_entry * Evd.evar_map * Impargs.manual_implicits
+  constr_expr option -> Safe_typing.private_constants definition_entry * Evd.evar_map * Impargs.manual_implicits
 
 val declare_definition : Id.t -> definition_kind ->
-  definition_entry -> Impargs.manual_implicits ->
+  Safe_typing.private_constants definition_entry -> Impargs.manual_implicits ->
     Globnames.global_reference Lemmas.declaration_hook -> Globnames.global_reference
 
 val do_definition : Id.t -> definition_kind -> lident list option ->
@@ -170,4 +170,4 @@ val do_cofixpoint :
 val check_mutuality : Environ.env -> bool -> (Id.t * types) list -> unit
 
 val declare_fix : ?opaque:bool -> definition_kind -> Univ.universe_context -> Id.t ->
-  Entries.proof_output -> types -> Impargs.manual_implicits -> global_reference
+  Safe_typing.private_constants Entries.proof_output -> types -> Impargs.manual_implicits -> global_reference
diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml
index 7d5d61fb8..b6da21e5a 100644
--- a/toplevel/discharge.ml
+++ b/toplevel/discharge.ml
@@ -20,8 +20,8 @@ open Cooking
 (* Discharging mutual inductive *)
 
 let detype_param = function
-  | (Name id,None,p) -> id, Entries.LocalAssum p
-  | (Name id,Some p,_) -> id, Entries.LocalDef p
+  | (Name id,None,p) -> id, LocalAssum p
+  | (Name id,Some p,_) -> id, LocalDef p
   | (Anonymous,_,_) -> anomaly (Pp.str "Unnamed inductive local variable")
 
 (* Replace
diff --git a/toplevel/ind_tables.ml b/toplevel/ind_tables.ml
index 218c47b28..dde801a7f 100644
--- a/toplevel/ind_tables.ml
+++ b/toplevel/ind_tables.ml
@@ -29,9 +29,9 @@ open Pp
 (* Registering schemes in the environment *)
 
 type mutual_scheme_object_function =
-  internal_flag -> mutual_inductive -> constr array Evd.in_evar_universe_context * Declareops.side_effects
+  internal_flag -> mutual_inductive -> constr array Evd.in_evar_universe_context * Safe_typing.private_constants
 type individual_scheme_object_function =
-  internal_flag -> inductive -> constr Evd.in_evar_universe_context * Declareops.side_effects
+  internal_flag -> inductive -> constr Evd.in_evar_universe_context * Safe_typing.private_constants
 
 type 'a scheme_kind = string
 
@@ -124,7 +124,9 @@ let define internal id c p univs =
   let c = Vars.subst_univs_fn_constr 
     (Universes.make_opt_subst (Evd.evar_universe_context_subst ctx)) c in
   let entry = {
-    const_entry_body = Future.from_val ((c,Univ.ContextSet.empty), Declareops.no_seff);
+    const_entry_body =
+      Future.from_val ((c,Univ.ContextSet.empty),
+                       Safe_typing.empty_private_constants);
     const_entry_secctx = None;
     const_entry_type = None;
     const_entry_polymorphic = p;
@@ -148,8 +150,8 @@ let define_individual_scheme_base kind suff f mode idopt (mind,i as ind) =
     | None -> add_suffix mib.mind_packets.(i).mind_typename suff in
   let const = define mode id c mib.mind_polymorphic ctx in
   declare_scheme kind [|ind,const|];
-  const, Declareops.cons_side_effects
-     (Safe_typing.sideff_of_scheme kind (Global.safe_env()) [ind,const]) eff
+  const, Safe_typing.add_private
+     (Safe_typing.private_con_of_scheme kind (Global.safe_env()) [ind,const]) eff
 
 let define_individual_scheme kind mode names (mind,i as ind) =
   match Hashtbl.find scheme_object_table kind with
@@ -168,8 +170,8 @@ let define_mutual_scheme_base kind suff f mode names mind =
   let schemes = Array.mapi (fun i cst -> ((mind,i),cst)) consts in
   declare_scheme kind schemes;
   consts,
-  Declareops.cons_side_effects 
-    (Safe_typing.sideff_of_scheme
+  Safe_typing.add_private 
+    (Safe_typing.private_con_of_scheme
       kind (Global.safe_env()) (Array.to_list schemes))
     eff 
 
@@ -181,10 +183,10 @@ let define_mutual_scheme kind mode names mind =
 
 let find_scheme_on_env_too kind ind =
   let s = String.Map.find kind (Indmap.find ind !scheme_map) in
-  s, Declareops.cons_side_effects
-      (Safe_typing.sideff_of_scheme
+  s, Safe_typing.add_private
+      (Safe_typing.private_con_of_scheme
             kind (Global.safe_env()) [ind, s])
-      Declareops.no_seff 
+      Safe_typing.empty_private_constants
 
 let find_scheme ?(mode=InternalTacticRequest) kind (mind,i as ind) =
   try find_scheme_on_env_too kind ind
diff --git a/toplevel/ind_tables.mli b/toplevel/ind_tables.mli
index d0844dd94..abd951c31 100644
--- a/toplevel/ind_tables.mli
+++ b/toplevel/ind_tables.mli
@@ -20,9 +20,9 @@ type individual
 type 'a scheme_kind
 
 type mutual_scheme_object_function =
-  internal_flag -> mutual_inductive -> constr array Evd.in_evar_universe_context * Declareops.side_effects
+  internal_flag -> mutual_inductive -> constr array Evd.in_evar_universe_context * Safe_typing.private_constants
 type individual_scheme_object_function =
-  internal_flag -> inductive -> constr Evd.in_evar_universe_context * Declareops.side_effects
+  internal_flag -> inductive -> constr Evd.in_evar_universe_context * Safe_typing.private_constants
 
 (** Main functions to register a scheme builder *)
 
@@ -37,13 +37,13 @@ val declare_individual_scheme_object : string -> ?aux:string ->
 
 val define_individual_scheme : individual scheme_kind -> 
   internal_flag (** internal *) ->
-  Id.t option -> inductive -> constant * Declareops.side_effects
+  Id.t option -> inductive -> constant * Safe_typing.private_constants
 
 val define_mutual_scheme : mutual scheme_kind -> internal_flag (** internal *) ->
-  (int * Id.t) list -> mutual_inductive -> constant array * Declareops.side_effects
+  (int * Id.t) list -> mutual_inductive -> constant array * Safe_typing.private_constants
 
 (** Main function to retrieve a scheme in the cache or to generate it *)
-val find_scheme : ?mode:internal_flag -> 'a scheme_kind -> inductive -> constant * Declareops.side_effects
+val find_scheme : ?mode:internal_flag -> 'a scheme_kind -> inductive -> constant * Safe_typing.private_constants
 
 val check_scheme : 'a scheme_kind -> inductive -> bool
 
diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml
index ae8ee7670..0b021254e 100644
--- a/toplevel/indschemes.ml
+++ b/toplevel/indschemes.ml
@@ -371,7 +371,7 @@ let do_mutual_induction_scheme lnamedepindsort =
   let declare decl fi lrecref =
     let decltype = Retyping.get_type_of env0 sigma decl in
     (* let decltype = refresh_universes decltype in *)
-    let proof_output = Future.from_val ((decl,Univ.ContextSet.empty),Declareops.no_seff) in
+    let proof_output = Future.from_val ((decl,Univ.ContextSet.empty),Safe_typing.empty_private_constants) in
     let cst = define fi UserIndividualRequest sigma proof_output (Some decltype) in
     ConstRef cst :: lrecref
   in
@@ -469,7 +469,7 @@ let do_combined_scheme name schemes =
       schemes
   in
   let body,typ = build_combined_scheme (Global.env ()) csts in
-  let proof_output = Future.from_val ((body,Univ.ContextSet.empty),Declareops.no_seff) in
+  let proof_output = Future.from_val ((body,Univ.ContextSet.empty),Safe_typing.empty_private_constants) in
   ignore (define (snd name) UserIndividualRequest Evd.empty proof_output (Some typ));
   fixpoint_message None [snd name]
 
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index 665926922..e488f84f8 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -541,7 +541,7 @@ let compute_possible_guardness_evidences (n,_) fixbody fixtype =
       let ctx = fst (decompose_prod_n_assum m fixtype) in
 	List.map_i (fun i _ -> i) 0 ctx
 
-let mk_proof c = ((c, Univ.ContextSet.empty), Declareops.no_seff)
+let mk_proof c = ((c, Univ.ContextSet.empty), Safe_typing.empty_private_constants)
 
 let declare_mutual_definition l =
   let len = List.length l in
@@ -619,7 +619,7 @@ let declare_obligation prg obl body ty uctx =
 	  shrink_body body else [], body, [||] 
       in
       let ce = 
-        { const_entry_body = Future.from_val((body,Univ.ContextSet.empty),Declareops.no_seff);
+        { const_entry_body = Future.from_val((body,Univ.ContextSet.empty),Safe_typing.empty_private_constants);
           const_entry_secctx = None;
 	  const_entry_type = if List.is_empty ctx then ty else None;
 	  const_entry_polymorphic = poly;
@@ -796,12 +796,12 @@ let solve_by_tac name evi t poly ctx =
   let (entry,_,ctx') = Pfedit.build_constant_by_tactic 
     id ~goal_kind:(goal_kind poly) ctx evi.evar_hyps concl (Tacticals.New.tclCOMPLETE t) in
   let env = Global.env () in
-  let entry = Term_typing.handle_entry_side_effects env entry in
-  let body, eff = Future.force entry.Entries.const_entry_body in
-  assert(Declareops.side_effects_is_empty eff);
+  let entry = Safe_typing.inline_private_constants_in_definition_entry env entry in
+  let body, eff = Future.force entry.const_entry_body in
+  assert(Safe_typing.empty_private_constants = eff);
   let ctx' = Evd.merge_context_set ~sideff:true Evd.univ_rigid (Evd.from_ctx ctx') (snd body) in
   Inductiveops.control_only_guard (Global.env ()) (fst body);
-  (fst body), entry.Entries.const_entry_type, Evd.evar_universe_context ctx'
+  (fst body), entry.const_entry_type, Evd.evar_universe_context ctx'
 
 let obligation_hook prg obl num auto ctx' _ gr =
   let obls, rem = prg.prg_obligations in
diff --git a/toplevel/obligations.mli b/toplevel/obligations.mli
index 40f124ca3..61a8ee520 100644
--- a/toplevel/obligations.mli
+++ b/toplevel/obligations.mli
@@ -17,11 +17,11 @@ open Decl_kinds
 
 (** Forward declaration. *)
 val declare_fix_ref : (?opaque:bool -> definition_kind -> Univ.universe_context -> Id.t ->
-  Entries.proof_output -> types -> Impargs.manual_implicits -> global_reference) ref
+  Safe_typing.private_constants Entries.proof_output -> types -> Impargs.manual_implicits -> global_reference) ref
 
 val declare_definition_ref :
   (Id.t -> definition_kind ->
-     Entries.definition_entry -> Impargs.manual_implicits
+     Safe_typing.private_constants Entries.definition_entry -> Impargs.manual_implicits
        -> global_reference Lemmas.declaration_hook -> global_reference) ref
 
 val check_evars : env -> evar_map -> unit
diff --git a/toplevel/record.ml b/toplevel/record.ml
index 60fe76bb8..b1be4c92a 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -160,8 +160,8 @@ let degenerate_decl (na,b,t) =
     | Name id -> id
     | Anonymous -> anomaly (Pp.str "Unnamed record variable") in
   match b with
-    | None -> (id, Entries.LocalAssum t)
-    | Some b -> (id, Entries.LocalDef b)
+    | None -> (id, LocalAssum t)
+    | Some b -> (id, LocalDef b)
 
 type record_error =
   | MissingProj of Id.t * Id.t list
@@ -297,7 +297,7 @@ let declare_projections indsp ?(kind=StructureComponent) binder_name coers field
 	        try
 		  let entry = {
 		    const_entry_body =
-		      Future.from_val (Term_typing.mk_pure_proof proj);
+		      Future.from_val (Safe_typing.mk_pure_proof proj);
 		    const_entry_secctx = None;
 		    const_entry_type = Some projtyp;
 		    const_entry_polymorphic = poly;