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.

9 files changed, 341 insertions, 90 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