Merge PR #888: Stronger kernel types

7 files changed, 178 insertions, 96 deletions

diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index 95822fac68..63614e20f7 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -151,9 +151,14 @@ let abstract_constant_body =
 type recipe = { from : constant_body; info : Opaqueproof.cooking_info }
 type inline = bool
 
-type result =
-  constant_def * constant_type * projection_body option * 
-    constant_universes * inline * Context.Named.t option
+type result = {
+  cook_body : constant_def;
+  cook_type : constant_type;
+  cook_proj : projection_body option;
+  cook_universes : constant_universes;
+  cook_inline : inline;
+  cook_context : Context.Named.t option;
+}
 
 let on_body ml hy f = function
   | Undef _ as x -> x
@@ -254,9 +259,14 @@ let cook_constant ~hcons env { from = cb; info } =
     | Polymorphic_const auctx -> 
       Polymorphic_const (AUContext.union abs_ctx auctx)
   in
-    (body, typ, Option.map projection cb.const_proj, 
-     univs, cb.const_inline_code, 
-     Some const_hyps)
+  {
+    cook_body = body;
+    cook_type = typ;
+    cook_proj = Option.map projection cb.const_proj;
+    cook_universes = univs;
+    cook_inline = cb.const_inline_code;
+    cook_context = Some const_hyps;
+  }
 
 (* let cook_constant_key = Profile.declare_profile "cook_constant" *)
 (* let cook_constant = Profile.profile2 cook_constant_key cook_constant *)
diff --git a/kernel/cooking.mli b/kernel/cooking.mli
index 79a028d760..f386fd9362 100644
--- a/kernel/cooking.mli
+++ b/kernel/cooking.mli
@@ -16,9 +16,14 @@ type recipe = { from : constant_body; info : Opaqueproof.cooking_info }
 
 type inline = bool
 
-type result =
-  constant_def * constant_type * projection_body option * 
-    constant_universes * inline * Context.Named.t option
+type result = {
+  cook_body : constant_def;
+  cook_type : constant_type;
+  cook_proj : projection_body option;
+  cook_universes : constant_universes;
+  cook_inline : inline;
+  cook_context : Context.Named.t option;
+}
 
 val cook_constant : hcons:bool -> env -> recipe -> result
 val cook_constr : Opaqueproof.cooking_info -> Term.constr -> Term.constr
diff --git a/kernel/entries.ml b/kernel/entries.ml
index 3fa25c142a..a1ccbdbc1b 100644
--- a/kernel/entries.ml
+++ b/kernel/entries.ml
@@ -64,6 +64,10 @@ type mutual_inductive_entry = {
 type 'a proof_output = constr Univ.in_universe_context_set * 'a
 type 'a const_entry_body = 'a proof_output Future.computation
 
+type constant_universes_entry =
+  | Monomorphic_const_entry of Univ.universe_context
+  | Polymorphic_const_entry of Univ.universe_context
+
 type 'a definition_entry = {
   const_entry_body   : 'a const_entry_body;
   (* List of section variables *)
@@ -71,8 +75,7 @@ type 'a definition_entry = {
   (* State id on which the completion of type checking is reported *)
   const_entry_feedback : Stateid.t option;
   const_entry_type        : types option;
-  const_entry_polymorphic : bool;
-  const_entry_universes   : Univ.universe_context;
+  const_entry_universes   : constant_universes_entry;
   const_entry_opaque      : bool;
   const_entry_inline_code : bool }
 
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index ed4c7d57ad..04051f2e23 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -382,12 +382,13 @@ let safe_push_named d env =
 
 
 let push_named_def (id,de) senv =
-  let c,typ,univs = 
-    match Term_typing.translate_local_def senv.revstruct senv.env id de with
-    | c, typ, Monomorphic_const ctx -> c, typ, ctx
-    | _, _, Polymorphic_const _ -> assert false
+  let open Entries in
+  let trust = Term_typing.SideEffects senv.revstruct in
+  let c,typ,univs = Term_typing.translate_local_def trust senv.env id de in
+  let poly = match de.Entries.const_entry_universes with
+  | Monomorphic_const_entry _ -> false
+  | Polymorphic_const_entry _ -> true
   in
-  let poly = de.Entries.const_entry_polymorphic in
   let univs = Univ.ContextSet.of_context univs in
   let c, univs = match c with
     | Def c -> Mod_subst.force_constr c, univs
@@ -492,12 +493,16 @@ let add_field ((l,sfb) as field) gn senv =
 let update_resolver f senv = { senv with modresolver = f senv.modresolver }
 
 (** Insertion of constants and parameters in environment *)
+type 'a effect_entry =
+| EffectEntry : private_constants effect_entry
+| PureEntry : unit effect_entry
+
 type global_declaration =
-  | ConstantEntry of bool * private_constants Entries.constant_entry
+  | ConstantEntry : 'a effect_entry * 'a Entries.constant_entry -> global_declaration
   | GlobalRecipe of Cooking.recipe
 
 type exported_private_constant = 
-  constant * private_constants Entries.constant_entry * private_constant_role
+  constant * private_constant_role
 
 let add_constant_aux no_section senv (kn, cb) =
   let l = pi3 (Constant.repr3 kn) in
@@ -521,30 +526,29 @@ let add_constant_aux no_section senv (kn, cb) =
   in
   senv''
 
+let export_private_constants ~in_section ce senv =
+  let exported, ce = Term_typing.export_side_effects senv.revstruct senv.env ce in
+  let bodies = List.map (fun (kn, cb, _) -> (kn, cb)) exported in
+  let exported = List.map (fun (kn, _, r) -> (kn, r)) exported in
+  let no_section = not in_section in
+  let senv = List.fold_left (add_constant_aux no_section) senv bodies in
+  (ce, exported), 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.export_side_effects 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
+      | ConstantEntry (EffectEntry, ce) ->
+        Term_typing.translate_constant (Term_typing.SideEffects senv.revstruct) senv.env kn ce
+      | ConstantEntry (PureEntry, ce) ->
+        Term_typing.translate_constant Term_typing.Pure 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
+  kn, senv
 
 (** Insertion of inductive types *)
 
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 5bb8ceb1a5..752fdd793e 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -67,7 +67,7 @@ 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
+  Environ.env -> private_constants Entries.definition_entry -> unit Entries.definition_entry
 
 val universes_of_private : private_constants -> Univ.universe_context_set list
 
@@ -94,19 +94,26 @@ val push_named_def :
 
 (** Insertion of global axioms or definitions *)
 
+type 'a effect_entry =
+| EffectEntry : private_constants effect_entry
+| PureEntry : unit effect_entry
+
 type global_declaration =
-                  (* bool: export private constants *)
-  | ConstantEntry of bool * private_constants Entries.constant_entry
+  | ConstantEntry : 'a effect_entry * 'a Entries.constant_entry -> global_declaration
   | GlobalRecipe of Cooking.recipe
 
 type exported_private_constant = 
-  constant * private_constants Entries.constant_entry * private_constant_role
+  constant * private_constant_role
+
+val export_private_constants : in_section:bool ->
+  private_constants Entries.constant_entry ->
+  (unit Entries.constant_entry * exported_private_constant list) safe_transformer
 
 (** 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 * exported_private_constant list) safe_transformer
+    constant safe_transformer
 
 (** Adding an inductive type *)
 
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index cf82d54ec1..43c099712a 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -77,6 +77,10 @@ end
 
 type side_effects = SideEffects.t
 
+type _ trust =
+| Pure : unit trust
+| SideEffects : structure_body -> side_effects trust
+
 let uniq_seff_rev = SideEffects.repr
 let uniq_seff l = List.rev (SideEffects.repr l)
 
@@ -232,7 +236,7 @@ let abstract_constant_universes abstract uctx =
     let sbst, auctx = Univ.abstract_universes uctx in
     sbst, Polymorphic_const auctx
 
-let infer_declaration ~trust env kn dcl =
+let infer_declaration (type a) ~(trust : a trust) env kn (dcl : a constant_entry) =
   match dcl with
   | ParameterEntry (ctx,poly,(t,uctx),nl) ->
       let env = push_context ~strict:(not poly) uctx env in
@@ -243,7 +247,14 @@ let infer_declaration ~trust env kn dcl =
       in
       let c = Typeops.assumption_of_judgment env j in
       let t = hcons_constr (Vars.subst_univs_level_constr usubst c) in
-	Undef nl, RegularArity t, None, univs, false, ctx
+      {
+        Cooking.cook_body = Undef nl;
+        cook_type = RegularArity t;
+        cook_proj = None;
+        cook_universes = univs;
+        cook_inline = false;
+        cook_context = ctx;
+      }
 
   (** Definition [c] is opaque (Qed), non polymorphic and with a specified type,
       so we delay the typing and hash consing of its body.
@@ -251,46 +262,65 @@ let infer_declaration ~trust env kn dcl =
       delay even in the polymorphic case.  *)
   | DefinitionEntry ({ const_entry_type = Some typ;
                        const_entry_opaque = true;
-		       const_entry_polymorphic = false} as c) ->
-      let env = push_context ~strict:true c.const_entry_universes env in
+		       const_entry_universes = Monomorphic_const_entry univs } as c) ->
+      let env = push_context ~strict:true univs env in
       let { const_entry_body = body; const_entry_feedback = feedback_id } = c in
       let tyj = infer_type env typ in
       let proofterm =
         Future.chain ~pure:true body (fun ((body,uctx),side_eff) ->
-          let body, uctx, signatures =
-            inline_side_effects env body uctx side_eff in
-          let valid_signatures = check_signatures trust signatures in
-	  let env = push_context_set uctx env in
-          let j =
+          let j, uctx = match trust with
+          | Pure ->
+            let env = push_context_set uctx env in
+            let j = infer env body in
+            let _ = judge_of_cast env j DEFAULTcast tyj in
+            j, uctx
+          | SideEffects mb ->
+            let (body, uctx, signatures) = inline_side_effects env body uctx side_eff in
+            let valid_signatures = check_signatures mb signatures in
+            let env = push_context_set uctx env in
             let body,env,ectx = skip_trusted_seff valid_signatures body env in
             let j = infer env body in
-            unzip ectx j in
-          let _ = judge_of_cast env j DEFAULTcast tyj in
+            let j = unzip ectx j in
+            let _ = judge_of_cast env j DEFAULTcast tyj in
+            j, uctx
+          in
           let c = hcons_constr j.uj_val in
           feedback_completion_typecheck feedback_id;
           c, uctx) in
       let def = OpaqueDef (Opaqueproof.create proofterm) in
-      def, RegularArity typ, None,
-      (Monomorphic_const c.const_entry_universes),
-      c.const_entry_inline_code, c.const_entry_secctx
+      {
+        Cooking.cook_body = def;
+        cook_type = RegularArity typ;
+        cook_proj = None;
+        cook_universes = Monomorphic_const univs;
+        cook_inline = c.const_entry_inline_code;
+        cook_context = c.const_entry_secctx;
+      }
 
   (** Other definitions have to be processed immediately. *)
   | DefinitionEntry c ->
       let { const_entry_type = typ; const_entry_opaque = opaque } = c in
       let { const_entry_body = body; const_entry_feedback = feedback_id } = c in
       let (body, ctx), side_eff = Future.join body in
-      let univsctx = Univ.ContextSet.of_context c.const_entry_universes in
-      let body, ctx, _ = inline_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
+      let poly, univs = match c.const_entry_universes with
+      | Monomorphic_const_entry univs -> false, univs
+      | Polymorphic_const_entry univs -> true, univs
+      in
+      let univsctx = Univ.ContextSet.of_context univs in
+      let ctx = Univ.ContextSet.union univsctx ctx in
+      let body, ctx, _ = match trust with
+      | Pure -> body, ctx, []
+      | SideEffects _ -> inline_side_effects env body ctx side_eff
+      in
+      let env = push_context_set ~strict:(not poly) ctx env in
+      let abstract = poly && not (Option.is_empty kn) in
       let usubst, univs =
         abstract_constant_universes abstract (Univ.ContextSet.to_context ctx)
       in      
       let j = infer env body in
       let typ = match typ with
         | None ->
-           if not c.const_entry_polymorphic then (* Old-style polymorphism *)
+           if not poly then (* Old-style polymorphism *)
              make_polymorphic_if_constant_for_ind env j
            else RegularArity (Vars.subst_univs_level_constr usubst j.uj_type)
         | Some t ->
@@ -304,7 +334,14 @@ let infer_declaration ~trust env kn dcl =
 	else Def (Mod_subst.from_val def) 
       in
 	feedback_completion_typecheck feedback_id;
-	def, typ, None, univs, c.const_entry_inline_code, c.const_entry_secctx
+      {
+        Cooking.cook_body = def;
+        cook_type = typ;
+        cook_proj = None;
+        cook_universes = univs;
+        cook_inline = c.const_entry_inline_code;
+        cook_context = c.const_entry_secctx;
+      }
 
   | ProjectionEntry {proj_entry_ind = ind; proj_entry_arg = i} ->
     let mib, _ = Inductive.lookup_mind_specif env (ind,0) in
@@ -324,8 +361,14 @@ let infer_declaration ~trust env kn dcl =
         Polymorphic_const (Univ.ACumulativityInfo.univ_context acumi)
     in
     let term, typ = pb.proj_eta in
-      Def (Mod_subst.from_val (hcons_constr term)), RegularArity typ, Some pb,
-      univs, false, None
+    {
+      Cooking.cook_body = Def (Mod_subst.from_val (hcons_constr term));
+      cook_type = RegularArity typ;
+      cook_proj = Some pb;
+      cook_universes = univs;
+      cook_inline = false;
+      cook_context = None;
+    }
 
 let global_vars_set_constant_type env = function
   | RegularArity t -> global_vars_set env t
@@ -349,7 +392,9 @@ let record_aux env s_ty s_bo suggested_expr =
 let suggest_proof_using = ref (fun _ _ _ _ _ -> "")
 let set_suggest_proof_using f = suggest_proof_using := f
 
-let build_constant_declaration kn env (def,typ,proj,univs,inline_code,ctx) =
+let build_constant_declaration kn env result =
+  let open Cooking in
+  let typ = result.cook_type in
   let check declared inferred =
     let mk_set l = List.fold_right Id.Set.add (List.map NamedDecl.get_id l) Id.Set.empty in
     let inferred_set, declared_set = mk_set inferred, mk_set declared in
@@ -376,7 +421,8 @@ let build_constant_declaration kn env (def,typ,proj,univs,inline_code,ctx) =
   (* We try to postpone the computation of used section variables *)
   let hyps, def =
     let context_ids = List.map NamedDecl.get_id (named_context env) in
-    match ctx with
+    let def = result.cook_body in
+    match result.cook_context with
     | None when not (List.is_empty context_ids) -> 
         (* No declared section vars, and non-empty section context:
            we must look at the body NOW, if any *)
@@ -419,9 +465,10 @@ let build_constant_declaration kn env (def,typ,proj,univs,inline_code,ctx) =
               let ids_def = global_vars_set env c in
               let inferred = keep_hyps env (Idset.union ids_typ ids_def) in
               check declared inferred) lc) in
+  let univs = result.cook_universes in
   let tps = 
     let res =
-      match proj with
+      match result.cook_proj with
       | None -> compile_constant_body env univs def
       | Some pb ->
 	(* The compilation of primitive projections is a bit tricky, because
@@ -434,10 +481,10 @@ let build_constant_declaration kn env (def,typ,proj,univs,inline_code,ctx) =
 	  { const_hyps = hyps;
 	    const_body = def;
 	    const_type = typ;
-	    const_proj = proj;
+	    const_proj = result.cook_proj;
 	    const_body_code = None;
 	    const_universes = univs;
-	    const_inline_code = inline_code;
+	    const_inline_code = result.cook_inline;
 	    const_typing_flags = Environ.typing_flags env;
 	    }
 	in
@@ -448,10 +495,10 @@ let build_constant_declaration kn env (def,typ,proj,univs,inline_code,ctx) =
   { const_hyps = hyps;
     const_body = def;
     const_type = typ;
-    const_proj = proj;
+    const_proj = result.cook_proj;
     const_body_code = tps;
     const_universes = univs;
-    const_inline_code = inline_code;
+    const_inline_code = result.cook_inline;
     const_typing_flags = Environ.typing_flags env }
 
 (*s Global and local constant declaration. *)
@@ -461,11 +508,12 @@ let translate_constant mb env kn ce =
     (infer_declaration ~trust:mb env (Some kn) ce)
 
 let constant_entry_of_side_effect cb u =
-  let poly, univs =
+  let univs =
     match cb.const_universes with
-    | Monomorphic_const ctx -> false, ctx
+    | Monomorphic_const uctx ->
+      Monomorphic_const_entry uctx
     | Polymorphic_const auctx -> 
-      true, Univ.AUContext.repr auctx
+      Polymorphic_const_entry (Univ.AUContext.repr auctx)
   in
   let pt =
     match cb.const_body, u with
@@ -473,12 +521,11 @@ let constant_entry_of_side_effect cb u =
     | Def b, `Nothing -> Mod_subst.force_constr b, Univ.ContextSet.empty
     | _ -> assert false in
   DefinitionEntry {
-    const_entry_body = Future.from_val (pt, empty_seff);
+    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 = poly;
     const_entry_universes = univs;
     const_entry_opaque = Declareops.is_opaque cb;
     const_entry_inline_code = cb.const_inline_code }
@@ -497,17 +544,18 @@ type side_effect_role =
   | Schema of inductive * string
 
 type exported_side_effect = 
-  constant * constant_body * side_effects constant_entry * side_effect_role
+  constant * constant_body * side_effect_role
 
 let export_side_effects mb env ce =
   match ce with
-  | ParameterEntry _ | ProjectionEntry _ -> [], ce
+  | ParameterEntry e -> [], ParameterEntry e
+  | ProjectionEntry e -> [], ProjectionEntry e
   | 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 ~pure:true body
-          (fun (b_ctx, _) -> b_ctx, empty_seff) } in
+          (fun (b_ctx, _) -> b_ctx, ()) } in
       let not_exists (c,_,_,_) =
         try ignore(Environ.lookup_constant c env); false
         with Not_found -> true in 
@@ -547,8 +595,8 @@ let export_side_effects mb env ce =
            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)) 
+               let cb = translate_constant Pure env kn ce in
+               (push_seff env (kn, cb,`Nothing, Subproof),(kn,cb,r) :: cbs)) 
              (env,[]) cbs in
            translate_seff sl rest (cbs @ acc) env
         | Some sl, cbs :: rest ->
@@ -556,7 +604,7 @@ let export_side_effects mb env ce =
            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
+             kn, cb, r) cbs in
            translate_seff (Some (sl-cbs_len)) rest (ecbs @ acc) env
      in
        translate_seff trusted seff [] env
@@ -575,11 +623,11 @@ let translate_recipe env kn r =
   build_constant_declaration kn env (Cooking.cook_constant ~hcons env r)
 
 let translate_local_def mb env id centry =
-  let def,typ,proj,univs,inline_code,ctx =
-    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
+  let open Cooking in
+  let decl = infer_declaration ~trust:mb env None (DefinitionEntry centry) in
+  let typ = type_of_constant_type env decl.cook_type in
+  if Option.is_empty decl.cook_context && !Flags.compilation_mode = Flags.BuildVo then begin
+    match decl.cook_body with
     | Undef _ -> ()
     | Def _ -> ()
     | OpaqueDef lc ->
@@ -592,7 +640,11 @@ let translate_local_def mb env id centry =
            env ids_def ids_typ context_ids in
        record_aux env ids_typ ids_def expr
   end;
-  def, typ, univs
+  let univs = match decl.cook_universes with
+  | Monomorphic_const ctx -> ctx
+  | Polymorphic_const _ -> assert false
+  in
+  decl.cook_body, typ, univs
 
 (* Insertion of inductive types. *)
 
@@ -602,7 +654,7 @@ let inline_entry_side_effects env ce = { ce with
   const_entry_body = Future.chain ~pure:true
     ce.const_entry_body (fun ((body, ctx), side_eff) ->
       let body, ctx',_ = inline_side_effects env body ctx side_eff in
-      (body, ctx'), empty_seff);
+      (body, ctx'), ());
 }
 
 let inline_side_effects env body side_eff =
diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli
index 77d126074f..24153343e7 100644
--- a/kernel/term_typing.mli
+++ b/kernel/term_typing.mli
@@ -14,8 +14,12 @@ open Entries
 
 type side_effects
 
-val translate_local_def : structure_body -> env -> Id.t -> side_effects definition_entry ->
-  constant_def * types * constant_universes
+type _ trust =
+| Pure : unit trust
+| SideEffects : structure_body -> side_effects trust
+
+val translate_local_def : 'a trust -> env -> Id.t -> 'a definition_entry ->
+  constant_def * types * Univ.universe_context
 
 val translate_local_assum : env -> types -> types
 
@@ -26,7 +30,7 @@ val inline_side_effects : env -> constr -> side_effects -> constr
     redexes. *)
 
 val inline_entry_side_effects :
-  env -> side_effects definition_entry -> side_effects definition_entry
+  env -> side_effects definition_entry -> unit definition_entry
 (** Same as {!inline_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. *)
@@ -43,7 +47,7 @@ val uniq_seff : side_effects -> side_effect list
 val equal_eff : side_effect -> side_effect -> bool
 
 val translate_constant :
-  structure_body -> env -> constant -> side_effects constant_entry ->
+  'a trust -> env -> constant -> 'a constant_entry ->
     constant_body
 
 type side_effect_role =
@@ -51,7 +55,7 @@ type side_effect_role =
   | Schema of inductive * string
 
 type exported_side_effect = 
-  constant * constant_body * side_effects constant_entry * side_effect_role
+  constant * constant_body * side_effect_role
   
 (* Given a constant entry containing side effects it exports them (either
  * by re-checking them or trusting them).  Returns the constant bodies to
@@ -59,10 +63,7 @@ type exported_side_effect =
  * needs to be translated as usual after this step. *)
 val export_side_effects :
   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
+    exported_side_effect list * unit constant_entry
 
 val translate_mind :
   env -> mutual_inductive -> mutual_inductive_entry -> mutual_inductive_body
@@ -71,8 +72,8 @@ val translate_recipe : env -> constant -> Cooking.recipe -> constant_body
 
 (** Internal functions, mentioned here for debug purpose only *)
 
-val infer_declaration : trust:structure_body -> env -> constant option -> 
-  side_effects constant_entry -> Cooking.result
+val infer_declaration : trust:'a trust -> env -> constant option -> 
+  'a constant_entry -> Cooking.result
 
 val build_constant_declaration :
   constant -> env -> Cooking.result -> constant_body