Merge PR #888: Stronger kernel types

18 files changed, 277 insertions, 173 deletions

diff --git a/API/API.mli b/API/API.mli
index 03b890a54..a042ad802 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -1345,6 +1345,9 @@ sig
   type inline = int option
   type 'a proof_output = Constr.t 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 *)
@@ -1352,8 +1355,7 @@ sig
                                  (* State id on which the completion of type checking is reported *)
                                  const_entry_feedback    : Stateid.t option;
                                  const_entry_type        : Constr.types option;
-                                 const_entry_polymorphic : bool;
-                                 const_entry_universes   : Univ.UContext.t;
+                                 const_entry_universes   : constant_universes_entry;
                                  const_entry_opaque      : bool;
                                  const_entry_inline_code : bool }
   type parameter_entry = Context.Named.t option * bool * Constr.types Univ.in_universe_context * inline
diff --git a/interp/declare.ml b/interp/declare.ml
index 154793a32..70f422b51 100644
--- a/interp/declare.ml
+++ b/interp/declare.ml
@@ -63,8 +63,12 @@ let cache_variable ((sp,_),o) =
 	impl, true, poly, ctx
     | SectionLocalDef (de) ->
       let univs = Global.push_named_def (id,de) in
+      let poly = match de.const_entry_universes with
+      | Monomorphic_const_entry _ -> false
+      | Polymorphic_const_entry _ -> true
+      in
       Explicit, de.const_entry_opaque,
-      de.const_entry_polymorphic, univs in
+      poly, univs in
   Nametab.push (Nametab.Until 1) (restrict_path 0 sp) (VarRef id);
   add_section_variable id impl poly ctx;
   Dischargedhypsmap.set_discharged_hyps sp [];
@@ -98,14 +102,12 @@ let declare_variable id obj =
 (** Declaration of constants and parameters *)
 
 type constant_obj = {
-  cst_decl : global_declaration;
+  cst_decl : global_declaration option;
+  (** [None] when the declaration is a side-effect and has already been defined
+      in the global environment. *)
   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 = Safe_typing.private_constants constant_entry * logical_kind
@@ -145,16 +147,15 @@ let cache_constant ((sp,kn), obj) =
   let id = basename sp in
   let _,dir,_ = repr_kn kn in
   let kn' =
-    if obj.cst_was_seff then begin
-      obj.cst_was_seff <- false;  
+    match obj.cst_decl with
+    | None ->
       if Global.exists_objlabel (Label.of_id (basename sp))
       then constant_of_kn kn
       else CErrors.anomaly Pp.(str"Ex seff not found: " ++ Id.print(basename sp) ++ str".")
-    end else
+    | Some decl ->
       let () = check_exists sp in
-      let kn', exported = Global.add_constant dir id obj.cst_decl in
-      obj.cst_exported <- exported;
-      kn' in
+      Global.add_constant dir id decl
+  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
@@ -175,26 +176,20 @@ let discharge_constant ((sp, kn), obj) =
   let new_hyps = (discharged_hyps kn hyps) @ obj.cst_hyps in
   let abstract = (named_of_variable_context hyps, subst, uctx) in
   let new_decl = GlobalRecipe{ from; info = { Opaqueproof.modlist; abstract}} in
-  Some { obj with cst_hyps = new_hyps; cst_decl = new_decl; }
+  Some { obj with cst_hyps = new_hyps; cst_decl = Some new_decl; }
 
 (* Hack to reduce the size of .vo: we keep only what load/open needs *)
-let dummy_constant_entry = 
-  ConstantEntry
-    (false, ParameterEntry (None,false,(mkProp,Univ.UContext.empty),None))
-
 let dummy_constant cst = {
-  cst_decl = dummy_constant_entry;
+  cst_decl = None;
   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, outConstant : (constant_obj -> obj) * (obj -> constant_obj)) =
-  declare_object_full { (default_object "CONSTANT") with
+let (inConstant : constant_obj -> obj) =
+  declare_object { (default_object "CONSTANT") with
     cache_function = cache_constant;
     load_function = load_constant;
     open_function = open_constant;
@@ -205,31 +200,14 @@ let (inConstant, outConstant : (constant_obj -> obj) * (obj -> constant_obj)) =
 let declare_scheme = ref (fun _ _ -> assert false)
 let set_declare_scheme f = declare_scheme := f
 
+let update_tables c =
+  declare_constant_implicits c;
+  Heads.declare_head (EvalConstRef c);
+  Notation.declare_ref_arguments_scope (ConstRef c)
+
 let declare_constant_common id cst =
-  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;
-      let () = if_xml (Hook.get f_xml_declare_constant) (InternalTacticRequest, c) in
-      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
   update_tables c;
@@ -237,34 +215,58 @@ let declare_constant_common id cst =
 
 let definition_entry ?fix_exn ?(opaque=false) ?(inline=false) ?types
     ?(poly=false) ?(univs=Univ.UContext.empty) ?(eff=Safe_typing.empty_private_constants) body =
+  let univs =
+    if poly then Polymorphic_const_entry univs
+    else Monomorphic_const_entry univs
+  in
   { const_entry_body = Future.from_val ?fix_exn ((body,Univ.ContextSet.empty), eff);
     const_entry_secctx = None;
     const_entry_type = types;
-    const_entry_polymorphic = poly;
     const_entry_universes = univs;
     const_entry_opaque = opaque;
     const_entry_feedback = None;
     const_entry_inline_code = inline}
 
 let declare_constant ?(internal = UserIndividualRequest) ?(local = false) id ?(export_seff=false) (cd, kind) =
-  let export = (* We deal with side effects *)
+  let is_poly de = match de.const_entry_universes with
+  | Monomorphic_const_entry _ -> false
+  | Polymorphic_const_entry _ -> true
+  in
+  let in_section = Lib.sections_are_opened () in
+  let export, decl = (* We deal with side effects *)
     match cd with
     | 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
-          Safe_typing.empty_private_constants <> seff
-    | _ -> false
+        is_poly de ->
+      (** This globally defines the side-effects in the environment. We mark
+          exported constants as being side-effect not to redeclare them at
+          caching time. *)
+      let cd, export = Global.export_private_constants ~in_section cd in
+      export, ConstantEntry (PureEntry, cd)
+    | _ -> [], ConstantEntry (EffectEntry, cd)
+  in
+  let iter_eff (c, role) =
+    let o = inConstant {
+      cst_decl = None;
+      cst_hyps = [] ;
+      cst_kind = IsProof Theorem;
+      cst_locl = false;
+    } in
+    let id = Label.to_id (pi3 (Constant.repr3 c)) in
+    ignore(add_leaf id o);
+    update_tables c;
+    let () = if_xml (Hook.get f_xml_declare_constant) (InternalTacticRequest, c) in
+    match role with
+    | Safe_typing.Subproof -> ()
+    | Safe_typing.Schema (ind, kind) -> !declare_scheme kind [|ind,c|]
   in
+  let () = List.iter iter_eff export in
   let cst = {
-    cst_decl = ConstantEntry (export,cd);
+    cst_decl = Some decl;
     cst_hyps = [] ;
     cst_kind = kind;
     cst_locl = local;
-    cst_exported = [];
-    cst_was_seff = false;
   } in
   let kn = declare_constant_common id cst in
   let () = if_xml (Hook.get f_xml_declare_constant) (internal, kn) in
diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index 95822fac6..63614e20f 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 79a028d76..f386fd936 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 3fa25c142..a1ccbdbc1 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 ed4c7d57a..04051f2e2 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 5bb8ceb1a..752fdd793 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 cf82d54ec..43c099712 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 77d126074..24153343e 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
diff --git a/library/global.ml b/library/global.ml
index 5b17855dc..00a3a4986 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -86,6 +86,7 @@ let push_context b c = globalize0 (Safe_typing.push_context b c)
 
 let set_engagement c = globalize0 (Safe_typing.set_engagement c)
 let set_typing_flags c = globalize0 (Safe_typing.set_typing_flags c)
+let export_private_constants ~in_section cd = globalize (Safe_typing.export_private_constants ~in_section cd)
 let add_constant dir id d = globalize (Safe_typing.add_constant dir (i2l id) d)
 let add_mind dir id mie = globalize (Safe_typing.add_mind dir (i2l id) mie)
 let add_modtype id me inl = globalize (Safe_typing.add_modtype (i2l id) me inl)
diff --git a/library/global.mli b/library/global.mli
index 48bcfa989..c777691d1 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -34,9 +34,12 @@ val set_typing_flags : Declarations.typing_flags -> unit
 val push_named_assum : (Id.t * Constr.types * bool) Univ.in_universe_context_set -> unit
 val push_named_def   : (Id.t * Safe_typing.private_constants Entries.definition_entry) -> Univ.universe_context_set
 
+val export_private_constants : in_section:bool ->
+  Safe_typing.private_constants Entries.constant_entry ->
+  unit Entries.constant_entry * Safe_typing.exported_private_constant list
+
 val add_constant :
-  DirPath.t -> Id.t -> Safe_typing.global_declaration ->
-    constant * Safe_typing.exported_private_constant list
+  DirPath.t -> Id.t -> Safe_typing.global_declaration -> constant
 val add_mind :
   DirPath.t -> Id.t -> Entries.mutual_inductive_entry -> mutual_inductive
 
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index a949c8e91..193788558 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -157,10 +157,9 @@ let build_by_tactic ?(side_eff=true) env sigma ?(poly=false) typ tac =
     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
+        (fun (pt, _) -> pt, ()) } in
+  let (cb, ctx), () = Future.force ce.const_entry_body in
   let univs' = Evd.merge_context_set Evd.univ_rigid (Evd.from_ctx univs) ctx in
-  assert(Safe_typing.empty_private_constants = se);
   cb, status, Evd.evar_universe_context univs'
 
 let refine_by_tactic env sigma ty tac =
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 52d6787d4..2ade797f6 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -378,6 +378,10 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now
       let t = EConstr.Unsafe.to_constr t in
       let univstyp, body = make_body t p in
       let univs, typ = Future.force univstyp in
+      let univs =
+        if poly then Entries.Polymorphic_const_entry univs
+        else Entries.Monomorphic_const_entry univs
+      in
 	{ Entries.
 	  const_entry_body = body;
 	  const_entry_secctx = section_vars;
@@ -386,7 +390,7 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now
 	  const_entry_inline_code = false;
 	  const_entry_opaque = true;
 	  const_entry_universes = univs;
-	  const_entry_polymorphic = poly})
+        })
 		fpl initial_goals in
   let binders =
     Option.map (fun names -> fst (Evd.universe_context ~names (Evd.from_ctx universes)))
diff --git a/tactics/ind_tables.ml b/tactics/ind_tables.ml
index 0407c1e36..7f087ea01 100644
--- a/tactics/ind_tables.ml
+++ b/tactics/ind_tables.ml
@@ -123,14 +123,18 @@ let define internal id c p univs =
   let ctx = Evd.normalize_evar_universe_context univs in
   let c = Vars.subst_univs_fn_constr 
     (Universes.make_opt_subst (Evd.evar_universe_context_subst ctx)) c in
+  let univs = Evd.evar_context_universe_context ctx in
+  let univs =
+    if p then Polymorphic_const_entry univs
+    else Monomorphic_const_entry univs
+  in
   let entry = {
     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;
-    const_entry_universes = Evd.evar_context_universe_context ctx;
+    const_entry_universes = univs;
     const_entry_opaque = false;
     const_entry_inline_code = false;
     const_entry_feedback = None;
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 8a95ad177..cb905e749 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -5004,8 +5004,9 @@ let cache_term_by_tactic_then ~opaque ?(goal_type=None) id gk tac tacK =
   in
   let cst = Impargs.with_implicit_protection cst () in
   let lem =
-    if const.Entries.const_entry_polymorphic then
-      let uctx = Univ.ContextSet.of_context const.Entries.const_entry_universes in
+    match const.Entries.const_entry_universes with
+    | Entries.Polymorphic_const_entry uctx ->
+      let uctx = Univ.ContextSet.of_context uctx in
       (** Hack: the kernel may generate definitions whose universe variables are
           not the same as requested in the entry because of constraints delayed
           in the body, even in polymorphic mode. We mimick what it does for now
@@ -5014,7 +5015,8 @@ let cache_term_by_tactic_then ~opaque ?(goal_type=None) id gk tac tacK =
       let uctx = Univ.ContextSet.to_context (Univ.ContextSet.union uctx body_uctx) in
       let u = Univ.UContext.instance uctx in
       mkConstU (cst, EInstance.make u)
-    else mkConst cst
+    | Entries.Monomorphic_const_entry _ ->
+      mkConst cst
   in
   let evd = Evd.set_universe_context evd ectx in
   let open Safe_typing in
diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml
index 3d97a767c..6ea8bc7f2 100644
--- a/vernac/indschemes.ml
+++ b/vernac/indschemes.ml
@@ -109,13 +109,17 @@ let _ =
 
 let define id internal ctx c t =
   let f = declare_constant ~internal in
+  let _, univs = Evd.universe_context ctx in
+  let univs =
+    if Flags.is_universe_polymorphism () then Polymorphic_const_entry univs
+    else Monomorphic_const_entry univs
+  in
   let kn = f id
     (DefinitionEntry
       { const_entry_body = c;
         const_entry_secctx = None;
         const_entry_type = t;
-	const_entry_polymorphic = Flags.is_universe_polymorphism ();
-	const_entry_universes = snd (Evd.universe_context ctx);
+	const_entry_universes = univs;
         const_entry_opaque = false;
         const_entry_inline_code = false;
         const_entry_feedback = None;
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index 10d3317f8..28aeaa725 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -636,12 +636,12 @@ let declare_obligation prg obl body ty uctx =
 	  shrink_body body ty else [], body, ty, [||]
       in
       let body = ((body,Univ.ContextSet.empty),Safe_typing.empty_private_constants) in
+      let univs = if poly then Polymorphic_const_entry uctx else Monomorphic_const_entry uctx in
       let ce =
         { const_entry_body = Future.from_val ~fix_exn:(fun x -> x) body;
           const_entry_secctx = None;
 	  const_entry_type = ty;
-	  const_entry_polymorphic = poly;
-	  const_entry_universes = uctx;
+	  const_entry_universes = univs;
 	  const_entry_opaque = opaque;
           const_entry_inline_code = false;
           const_entry_feedback = None;
@@ -818,8 +818,7 @@ let solve_by_tac name evi t poly ctx =
     id ~goal_kind:(goal_kind poly) ctx evi.evar_hyps concl (Tacticals.New.tclCOMPLETE t) in
   let env = Global.env () in
   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 body, () = Future.force entry.const_entry_body in
   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.const_entry_type, Evd.evar_universe_context ctx'
@@ -836,8 +835,7 @@ let obligation_terminator name num guard hook auto pf =
       let env = Global.env () in
       let entry = Safe_typing.inline_private_constants_in_definition_entry env entry in
       let ty = entry.Entries.const_entry_type in
-      let (body, cstr), eff = Future.force entry.Entries.const_entry_body in
-      assert(Safe_typing.empty_private_constants = eff);
+      let (body, cstr), () = Future.force entry.Entries.const_entry_body in
       let sigma = Evd.from_ctx (fst uctx) in
       let sigma = Evd.merge_context_set ~sideff:true Evd.univ_rigid sigma cstr in
       Inductiveops.control_only_guard (Global.env ()) body;
diff --git a/vernac/record.ml b/vernac/record.ml
index 63ca22786..a2e443e5f 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -322,13 +322,16 @@ let declare_projections indsp ?(kind=StructureComponent) binder_name coers field
 		let projtyp =
                   it_mkProd_or_LetIn (mkProd (x,rp,ccl)) paramdecls in
 	        try
+                  let univs =
+                    if poly then Polymorphic_const_entry ctx
+                    else Monomorphic_const_entry ctx
+                  in
 		  let entry = {
 		    const_entry_body =
 		      Future.from_val (Safe_typing.mk_pure_proof proj);
 		    const_entry_secctx = None;
 		    const_entry_type = Some projtyp;
-		    const_entry_polymorphic = poly;
-		    const_entry_universes = ctx;
+		    const_entry_universes = univs;
 		    const_entry_opaque = false;
 		    const_entry_inline_code = false;
 		    const_entry_feedback = None } in