30 files changed, 388 insertions, 286 deletions
diff --git a/kernel/byterun/coq_memory.c b/kernel/byterun/coq_memory.c
index 542a05fd25..a1c49bee95 100644
--- a/kernel/byterun/coq_memory.c
+++ b/kernel/byterun/coq_memory.c
@@ -105,7 +105,7 @@ value init_coq_vm(value unit) /* ML */
     init_coq_interpreter();
     
     /* Some predefined pointer code.
-     * It is typically contained in accumlator blocks whose tag is 0 and thus
+     * It is typically contained in accumulator blocks whose tag is 0 and thus
      * scanned by the GC, so make it look like an OCaml block. */
     value accu_block = (value) coq_stat_alloc(2 * sizeof(value));
     Hd_hp (accu_block) = Make_header (1, Abstract_tag, Caml_black);        \
diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml
index 95f88c0306..fc7d1a54f2 100644
--- a/kernel/cClosure.ml
+++ b/kernel/cClosure.ml
@@ -226,7 +226,7 @@ let unfold_red kn =
  * this constant or abstraction.
  *  * i_tab is the cache table of the results
  *
- * ref_value_cache searchs in the tab, otherwise uses i_repr to
+ * ref_value_cache searches in the tab, otherwise uses i_repr to
  * compute the result and store it in the table. If the constant can't
  * be unfolded, returns None, but does not store this failure.  * This
  * doesn't take the RESET into account. You mustn't keep such a table
@@ -645,7 +645,7 @@ and subst_constr subst c = match [@ocaml.warning "-4"] Constr.kind c with
 and comp_subs el s =
   Esubst.lift_subst (fun el c -> lazy (to_constr el c)) el s
 
-(* This function defines the correspondance between constr and
+(* This function defines the correspondence between constr and
    fconstr. When we find a closure whose substitution is the identity,
    then we directly return the constr to avoid possibly huge
    reallocation. *)
diff --git a/kernel/cClosure.mli b/kernel/cClosure.mli
index 1a790eaed6..60185464c5 100644
--- a/kernel/cClosure.mli
+++ b/kernel/cClosure.mli
@@ -200,7 +200,7 @@ val whd_val : clos_infos -> clos_tab -> fconstr -> constr
 val whd_stack :
   clos_infos -> clos_tab -> fconstr -> stack -> fconstr * stack
 
-(** [eta_expand_ind_stack env ind c s t] computes stacks correspoding
+(** [eta_expand_ind_stack env ind c s t] computes stacks corresponding
     to the conversion of the eta expansion of t, considered as an inhabitant
     of ind, and the Constructor c of this inductive type applied to arguments
     s.
diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml
index 69f004307d..90fbcb8ae3 100644
--- a/kernel/cbytegen.ml
+++ b/kernel/cbytegen.ml
@@ -386,7 +386,7 @@ let rec is_tailcall = function
   | Klabel _ :: c -> is_tailcall c
   | _ -> None
 
-(* Extention of the continuation *)
+(* Extension of the continuation *)
 
 (* Add a Kpop n instruction in front of a continuation *)
 let rec add_pop n = function
diff --git a/kernel/constr.mli b/kernel/constr.mli
index 7fc57cdb8a..aa5878c9d7 100644
--- a/kernel/constr.mli
+++ b/kernel/constr.mli
@@ -141,7 +141,7 @@ val mkRef : GlobRef.t Univ.puniverses -> constr
     [mkCase ci p c ac] stand for match [c] as [x] in [I args] return [p] with [ac] 
     presented as describe in [ci].
 
-    [p] stucture is [fun args x -> "return clause"]
+    [p] structure is [fun args x -> "return clause"]
 
     [ac]{^ ith} element is ith constructor case presented as 
     {e lambda construct_args (without params). case_term } *)
diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index 9b6e37251f..1336e3e8bf 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -165,25 +165,33 @@ type 'opaque result = {
   cook_context : Constr.named_context option;
 }
 
-let on_body ml hy f = function
-  | Undef _ as x -> x
-  | Def cs -> Def (Mod_subst.from_val (f (Mod_subst.force_constr cs)))
-  | OpaqueDef o ->
-    OpaqueDef (Opaqueproof.discharge_direct_opaque ~cook_constr:f
-                 { Opaqueproof.modlist = ml; abstract = hy } o)
-  | Primitive _ -> CErrors.anomaly (Pp.str "Primitives cannot be cooked")
-
 let expmod_constr_subst cache modlist subst c =
   let subst = Univ.make_instance_subst subst in
   let c = expmod_constr cache modlist c in
     Vars.subst_univs_level_constr subst c
 
-let cook_constr { Opaqueproof.modlist ; abstract = (vars, subst, _) } c =
-  let cache = RefTable.create 13 in
-  let expmod = expmod_constr_subst cache modlist subst in
-  let hyps = Context.Named.map expmod vars in
-  let hyps = abstract_context hyps in
-  abstract_constant_body (expmod c) hyps
+let discharge_abstract_universe_context subst abs_ctx auctx =
+  (** Given a named instance [subst := u₀ ... uₙ₋₁] together with an abstract
+      context [auctx0 := 0 ... n - 1 |= C{0, ..., n - 1}] of the same length,
+      and another abstract context relative to the former context
+      [auctx := 0 ... m - 1 |= C'{u₀, ..., uₙ₋₁, 0, ..., m - 1}],
+      construct the lifted abstract universe context
+      [0 ... n - 1 n ... n + m - 1 |=
+        C{0, ... n - 1} ∪
+        C'{0, ..., n - 1, n, ..., n + m - 1} ]
+      together with the instance
+      [u₀ ... uₙ₋₁ Var(0) ... Var (m - 1)].
+  *)
+  if (Univ.Instance.is_empty subst) then
+    (** Still need to take the union for the constraints between globals *)
+    subst, (AUContext.union abs_ctx auctx)
+  else
+    let open Univ in
+    let ainst = make_abstract_instance auctx in
+    let subst = Instance.append subst ainst in
+    let substf = make_instance_subst subst in
+    let auctx = Univ.subst_univs_level_abstract_universe_context substf auctx in
+    subst, (AUContext.union abs_ctx auctx)
 
 let lift_univs cb subst auctx0 =
   match cb.const_universes with
@@ -191,28 +199,26 @@ let lift_univs cb subst auctx0 =
     assert (AUContext.is_empty auctx0);
     subst, (Monomorphic ctx)
   | Polymorphic auctx ->
-    (** Given a named instance [subst := u₀ ... uₙ₋₁] together with an abstract
-        context [auctx0 := 0 ... n - 1 |= C{0, ..., n - 1}] of the same length,
-        and another abstract context relative to the former context
-        [auctx := 0 ... m - 1 |= C'{u₀, ..., uₙ₋₁, 0, ..., m - 1}],
-        construct the lifted abstract universe context
-        [0 ... n - 1 n ... n + m - 1 |=
-          C{0, ... n - 1} ∪
-          C'{0, ..., n - 1, n, ..., n + m - 1} ]
-        together with the instance
-        [u₀ ... uₙ₋₁ Var(0) ... Var (m - 1)].
-    *)
-    if (Univ.Instance.is_empty subst) then
-      (** Still need to take the union for the constraints between globals *)
-      subst, (Polymorphic (AUContext.union auctx0 auctx))
-    else
-      let ainst = Univ.make_abstract_instance auctx in
-      let subst = Instance.append subst ainst in
-      let substf = Univ.make_instance_subst subst in
-      let auctx' = Univ.subst_univs_level_abstract_universe_context substf auctx in
-      subst, (Polymorphic (AUContext.union auctx0 auctx'))
-
-let cook_constant ~hcons { from = cb; info } =
+    let subst, auctx = discharge_abstract_universe_context subst auctx0 auctx in
+    subst, (Polymorphic auctx)
+
+let cook_constr { Opaqueproof.modlist ; abstract } (univs, c) =
+  let cache = RefTable.create 13 in
+  let abstract, usubst, abs_ctx = abstract in
+  let ainst = Instance.of_array (Array.init univs Level.var) in
+  let usubst = Instance.append usubst ainst in
+  let expmod = expmod_constr_subst cache modlist usubst in
+  let hyps = Context.Named.map expmod abstract in
+  let hyps = abstract_context hyps in
+  let c = abstract_constant_body (expmod c) hyps in
+  univs + AUContext.size abs_ctx, c
+
+let cook_constr infos univs c =
+  let fold info (univs, c) = cook_constr info (univs, c) in
+  let (_, c) = List.fold_right fold infos (univs, c) in
+  c
+
+let cook_constant { from = cb; info } =
   let { Opaqueproof.modlist; abstract } = info in
   let cache = RefTable.create 13 in
   let abstract, usubst, abs_ctx = abstract in
@@ -220,13 +226,13 @@ let cook_constant ~hcons { from = cb; info } =
   let expmod = expmod_constr_subst cache modlist usubst in
   let hyps0 = Context.Named.map expmod abstract in
   let hyps = abstract_context hyps0 in
-  let map c =
-    let c = abstract_constant_body (expmod c) hyps in
-    if hcons then Constr.hcons c else c
-  in
-  let body = on_body modlist (hyps0, usubst, abs_ctx)
-    map
-    cb.const_body
+  let map c = abstract_constant_body (expmod c) hyps in
+  let body = match cb.const_body with
+  | Undef _ as x -> x
+  | Def cs -> Def (Mod_subst.from_val (map (Mod_subst.force_constr cs)))
+  | OpaqueDef o ->
+    OpaqueDef (Opaqueproof.discharge_direct_opaque info o)
+  | Primitive _ -> CErrors.anomaly (Pp.str "Primitives cannot be cooked")
   in
   let const_hyps =
     Context.Named.fold_outside (fun decl hyps ->
@@ -251,4 +257,115 @@ let cook_constant ~hcons { from = cb; info } =
 (* let cook_constant_key = CProfile.declare_profile "cook_constant" *)
 (* let cook_constant = CProfile.profile2 cook_constant_key cook_constant *)
 
+(********************************)
+(* Discharging mutual inductive *)
+
+(* Replace
+
+     Var(y1)..Var(yq):C1..Cq |- Ij:Bj
+     Var(y1)..Var(yq):C1..Cq; I1..Ip:B1..Bp |- ci : Ti
+
+   by
+
+     |- Ij: (y1..yq:C1..Cq)Bj
+     I1..Ip:(B1 y1..yq)..(Bp y1..yq) |- ci : (y1..yq:C1..Cq)Ti[Ij:=(Ij y1..yq)]
+*)
+
+let it_mkNamedProd_wo_LetIn b d =
+  List.fold_left (fun c d -> mkNamedProd_wo_LetIn d c) b d
+
+let abstract_inductive decls nparamdecls inds =
+  let open Entries in
+  let ntyp = List.length inds in
+  let ndecls = Context.Named.length decls in
+  let args = Context.Named.to_instance mkVar (List.rev decls) in
+  let args = Array.of_list args in
+  let subs = List.init ntyp (fun k -> lift ndecls (mkApp(mkRel (k+1),args))) in
+  let inds' =
+    List.map
+      (function (tname,arity,template,cnames,lc) ->
+        let lc' = List.map (Vars.substl subs) lc in
+        let lc'' = List.map (fun b -> it_mkNamedProd_wo_LetIn b decls) lc' in
+        let arity' = it_mkNamedProd_wo_LetIn arity decls in
+        (tname,arity',template,cnames,lc''))
+        inds in
+  let nparamdecls' = nparamdecls + Array.length args in
+(* To be sure to be the same as before, should probably be moved to cook_inductive *)
+  let params' = let (_,arity,_,_,_) = List.hd inds' in
+                let (params,_) = decompose_prod_n_assum nparamdecls' arity in
+    params
+  in
+  let ind'' =
+  List.map
+    (fun (a,arity,template,c,lc) ->
+      let _, short_arity = decompose_prod_n_assum nparamdecls' arity in
+      let shortlc =
+        List.map (fun c -> snd (decompose_prod_n_assum nparamdecls' c)) lc in
+      { mind_entry_typename = a;
+        mind_entry_arity = short_arity;
+        mind_entry_template = template;
+        mind_entry_consnames = c;
+        mind_entry_lc = shortlc })
+    inds'
+  in (params',ind'')
+
+let refresh_polymorphic_type_of_inductive (_,mip) =
+  match mip.mind_arity with
+  | RegularArity s -> s.mind_user_arity, false
+  | TemplateArity ar ->
+    let ctx = List.rev mip.mind_arity_ctxt in
+      mkArity (List.rev ctx, Sorts.sort_of_univ ar.template_level), true
+
+let dummy_variance = let open Entries in function
+  | Monomorphic_entry _ -> assert false
+  | Polymorphic_entry (_,uctx) -> Array.make (Univ.UContext.size uctx) Univ.Variance.Irrelevant
+
+let cook_inductive { Opaqueproof.modlist; abstract } mib =
+  let open Entries in
+  let (section_decls, subst, abs_uctx) = abstract in
+  let nparamdecls = Context.Rel.length mib.mind_params_ctxt in
+  let subst, ind_univs =
+    match mib.mind_universes with
+    | Monomorphic ctx -> Univ.empty_level_subst, Monomorphic_entry ctx
+    | Polymorphic auctx ->
+      let subst, auctx = discharge_abstract_universe_context subst abs_uctx auctx in
+      let subst = Univ.make_instance_subst subst in
+      let nas = Univ.AUContext.names auctx in
+      let auctx = Univ.AUContext.repr auctx in
+      subst, Polymorphic_entry (nas, auctx)
+  in
+  let variance = match mib.mind_variance with
+    | None -> None
+    | Some _ -> Some (dummy_variance ind_univs)
+  in
+  let cache = RefTable.create 13 in
+  let discharge c = Vars.subst_univs_level_constr subst (expmod_constr cache modlist c) in
+  let inds =
+    Array.map_to_list
+      (fun mip ->
+        let ty, template = refresh_polymorphic_type_of_inductive (mib,mip) in
+        let arity = discharge ty in
+        let lc = Array.map discharge mip.mind_user_lc  in
+          (mip.mind_typename,
+           arity, template,
+           Array.to_list mip.mind_consnames,
+           Array.to_list lc))
+      mib.mind_packets in
+  let section_decls' = Context.Named.map discharge section_decls in
+  let (params',inds') = abstract_inductive section_decls' nparamdecls inds in
+  let record = match mib.mind_record with
+    | PrimRecord info ->
+      Some (Some (Array.map (fun (x,_,_,_) -> x) info))
+    | FakeRecord -> Some None
+    | NotRecord -> None
+  in
+  { mind_entry_record = record;
+    mind_entry_finite = mib.mind_finite;
+    mind_entry_params = params';
+    mind_entry_inds = inds';
+    mind_entry_private = mib.mind_private;
+    mind_entry_variance = variance;
+    mind_entry_universes = ind_univs
+  }
+
 let expmod_constr modlist c = expmod_constr (RefTable.create 13) modlist c
diff --git a/kernel/cooking.mli b/kernel/cooking.mli
index b022e2ac09..934b7c6b50 100644
--- a/kernel/cooking.mli
+++ b/kernel/cooking.mli
@@ -27,8 +27,11 @@ type 'opaque result = {
   cook_context : Constr.named_context option;
 }
 
-val cook_constant : hcons:bool -> recipe -> Opaqueproof.opaque result
-val cook_constr : Opaqueproof.cooking_info -> constr -> constr
+val cook_constant : recipe -> Opaqueproof.opaque result
+val cook_constr : Opaqueproof.cooking_info list -> int -> constr -> constr
+
+val cook_inductive :
+  Opaqueproof.cooking_info -> mutual_inductive_body -> Entries.mutual_inductive_entry
 
 (** {6 Utility functions used in module [Discharge]. } *)
 
diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index 36ee952099..388b4f14bf 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -22,11 +22,11 @@ type engagement = set_predicativity
 (** {6 Representation of constants (Definition/Axiom) } *)
 
 (** Non-universe polymorphic mode polymorphism (Coq 8.2+): inductives
-    and constants hiding inductives are implicitely polymorphic when
+    and constants hiding inductives are implicitly polymorphic when
     applied to parameters, on the universes appearing in the whnf of
     their parameters and their conclusion, in a template style.
     
-    In truely universe polymorphic mode, we always use RegularArity.
+    In truly universe polymorphic mode, we always use RegularArity.
 *)
 
 type template_arity = {
@@ -165,7 +165,7 @@ type one_inductive_body = {
 
     mind_nrealdecls : int; (** Length of realargs context (with let, no params) *)
 
-    mind_kelim : Sorts.family list; (** List of allowed elimination sorts *)
+    mind_kelim : Sorts.family; (** Highest allowed elimination sort *)
 
     mind_nf_lc : (rel_context * types) array; (** Head normalized constructor types so that their conclusion exposes the inductive type *)
 
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 05f342a82a..c47bde0864 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -483,16 +483,6 @@ let constant_value_and_type env (kn, u) =
   in
   b', subst_instance_constr u cb.const_type, cst
 
-let body_of_constant_body env cb =
-  let otab = opaque_tables env in
-  match cb.const_body with
-  | Undef _ | Primitive _ ->
-     None
-  | Def c ->
-     Some (Mod_subst.force_constr c, Declareops.constant_polymorphic_context cb)
-  | OpaqueDef o ->
-     Some (Opaqueproof.force_proof otab o, Declareops.constant_polymorphic_context cb)
-
 (* These functions should be called under the invariant that [env] 
    already contains the constraints corresponding to the constant 
    application. *)
diff --git a/kernel/environ.mli b/kernel/environ.mli
index f6cd41861e..2abcea148a 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -215,12 +215,6 @@ val constant_value_and_type : env -> Constant.t puniverses ->
     polymorphic *)
 val constant_context : env -> Constant.t -> Univ.AUContext.t
 
-(** Returns the body of the constant if it has any, and the polymorphic context
-    it lives in. For monomorphic constant, the latter is empty, and for
-    polymorphic constants, the term contains De Bruijn universe variables that
-    need to be instantiated. *)
-val body_of_constant_body : env -> Opaqueproof.opaque constant_body -> (Constr.constr * Univ.AUContext.t) option
-
 (* These functions should be called under the invariant that [env] 
    already contains the constraints corresponding to the constant 
    application. *)
diff --git a/kernel/indTyping.ml b/kernel/indTyping.ml
index 4e6e595331..65298938fa 100644
--- a/kernel/indTyping.ml
+++ b/kernel/indTyping.ml
@@ -232,18 +232,9 @@ let check_record data =
 (* - all_sorts in case of small, unitary Prop (not smashed) *)
 (* - logical_sorts in case of large, unitary Prop (smashed) *)
 
-let all_sorts = [InSProp;InProp;InSet;InType]
-let small_sorts = [InSProp;InProp;InSet]
-let logical_sorts = [InSProp;InProp]
-let sprop_sorts = [InSProp]
-
 let allowed_sorts {ind_squashed;ind_univ;ind_min_univ=_;ind_has_relevant_arg=_} =
-  if not ind_squashed then all_sorts
-  else match Sorts.family (Sorts.sort_of_univ ind_univ) with
-    | InType -> assert false
-    | InSet -> small_sorts
-    | InProp -> logical_sorts
-    | InSProp -> sprop_sorts
+  if not ind_squashed then InType
+  else Sorts.family (Sorts.sort_of_univ ind_univ)
 
 (* Returns the list [x_1, ..., x_n] of levels contributing to template
    polymorphism. The elements x_k is None if the k-th parameter (starting
diff --git a/kernel/indTyping.mli b/kernel/indTyping.mli
index ad51af66a2..ef2c30b76a 100644
--- a/kernel/indTyping.mli
+++ b/kernel/indTyping.mli
@@ -22,7 +22,7 @@ open Declarations
     - for each inductive,
       (arity * constructors) (with params)
       * (indices * splayed constructor types) (both without params)
-      * allowed eliminations
+      * top allowed elimination
  *)
 val typecheck_inductive : env -> mutual_inductive_entry ->
   env
@@ -31,5 +31,5 @@ val typecheck_inductive : env -> mutual_inductive_entry ->
   * Constr.rel_context
   * ((inductive_arity * Constr.types array) *
      (Constr.rel_context * (Constr.rel_context * Constr.types) array) *
-     Sorts.family list)
+     Sorts.family)
     array
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index d9335d39b5..beff8f4421 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -166,7 +166,7 @@ let make_subst env =
         (* template, it is identity substitution  otherwise (ie. when u is *)
         (* already in the domain of the substitution) [remember_subst] will *)
         (* update its image [x] by [sup x u] in order not to forget the *)
-        (* dependency in [u] that remains to be fullfilled. *)
+        (* dependency in [u] that remains to be fulfilled. *)
         make (remember_subst u subst) (sign, exp, [])
     | _sign, [], _ ->
         (* Uniform parameters are exhausted *)
@@ -289,7 +289,7 @@ let get_instantiated_arity (_ind,u) (mib,mip) params =
   let sign, s = mind_arity mip in
   full_inductive_instantiate mib u params sign, s
 
-let elim_sorts (_,mip) = mip.mind_kelim
+let elim_sort (_,mip) = mip.mind_kelim
 
 let is_private (mib,_) = mib.mind_private = Some true
 let is_primitive_record (mib,_) = 
@@ -305,12 +305,12 @@ let build_dependent_inductive ind (_,mip) params =
        @ Context.Rel.to_extended_list mkRel 0 realargs)
 
 (* This exception is local *)
-exception LocalArity of (Sorts.family list * Sorts.family * Sorts.family * arity_error) option
+exception LocalArity of (Sorts.family * Sorts.family * Sorts.family * arity_error) option
 
 let check_allowed_sort ksort specif =
-  if not (CList.exists (Sorts.family_equal ksort) (elim_sorts specif)) then
+  if not (Sorts.family_leq ksort (elim_sort specif)) then
     let s = inductive_sort_family (snd specif) in
-    raise (LocalArity (Some(elim_sorts specif, ksort,s,error_elim_explain ksort s)))
+    raise (LocalArity (Some(elim_sort specif, ksort,s,error_elim_explain ksort s)))
 
 let is_correct_arity env c pj ind specif params =
   let arsign,_ = get_instantiated_arity ind specif params in
diff --git a/kernel/inductive.mli b/kernel/inductive.mli
index 997a620742..f705cdf646 100644
--- a/kernel/inductive.mli
+++ b/kernel/inductive.mli
@@ -52,7 +52,7 @@ val type_of_inductive : env -> mind_specif puniverses -> types
 val type_of_inductive_knowing_parameters :
   env -> ?polyprop:bool -> mind_specif puniverses -> types Lazy.t array -> types
 
-val elim_sorts : mind_specif -> Sorts.family list
+val elim_sort : mind_specif -> Sorts.family
 
 val is_private : mind_specif -> bool
 val is_primitive_record : mind_specif -> bool
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index 2de5faa6df..72393d0081 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -188,7 +188,7 @@ let rec check_with_mod env struc (idl,mp1) mp equiv =
       in
       let new_equiv = add_delta_resolver equiv new_mb.mod_delta in
       (* we propagate the new equality in the rest of the signature
-	 with the identity substitution accompagned by the new resolver*)
+         with the identity substitution accompanied by the new resolver*)
       let id_subst = map_mp mp' mp' new_mb.mod_delta in
       let new_after = subst_structure id_subst after in
       before@(lab,SFBmodule new_mb')::new_after, new_equiv, cst
diff --git a/kernel/modops.ml b/kernel/modops.ml
index 4fdd7ab334..472fddb829 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -515,7 +515,7 @@ and strengthen_and_subst_struct str subst mp_from mp_to alias incl reso =
      "Module M:=P." or "Module M. Include P. End M."
     We need to perform two operations to compute the body of M.
     - The first one is applying the substitution {P <- M} on the type of P
-    - The second one is strenghtening. *)
+    - The second one is strengthening. *)
 
 let strengthen_and_subst_mb mb mp include_b = match mb.mod_type with
   |NoFunctor struc ->
diff --git a/kernel/opaqueproof.ml b/kernel/opaqueproof.ml
index 18c1bcc0f8..e18b726111 100644
--- a/kernel/opaqueproof.ml
+++ b/kernel/opaqueproof.ml
@@ -16,15 +16,22 @@ open Mod_subst
 type work_list = (Instance.t * Id.t array) Cmap.t * 
   (Instance.t * Id.t array) Mindmap.t
 
-type cooking_info = { 
-  modlist : work_list; 
+type cooking_info = {
+  modlist : work_list;
   abstract : Constr.named_context * Univ.Instance.t * Univ.AUContext.t }
+
+type indirect_accessor = {
+  access_proof : DirPath.t -> int -> constr option;
+  access_discharge : cooking_info list -> int -> constr -> constr;
+}
+
 type proofterm = (constr * Univ.ContextSet.t) Future.computation
+type universes = int
 type opaque =
   | Indirect of substitution list * DirPath.t * int (* subst, lib, index *)
-  | Direct of cooking_info list * proofterm
+  | Direct of universes * cooking_info list * proofterm
 type opaquetab = {
-  opaque_val : (cooking_info list * proofterm) Int.Map.t;
+  opaque_val : (int * cooking_info list * proofterm) Int.Map.t;
   (** Actual proof terms *)
   opaque_len : int;
   (** Size of the above map *)
@@ -36,35 +43,28 @@ let empty_opaquetab = {
   opaque_dir = DirPath.initial;
 }
 
-(* hooks *)
-let default_get_opaque dp _ =
-  CErrors.user_err Pp.(pr_sequence str ["Cannot access opaque proofs in library"; DirPath.to_string dp])
-let default_get_univ dp _ =
-  CErrors.user_err (Pp.pr_sequence Pp.str [
-    "Cannot access universe constraints of opaque proofs in library ";
-    DirPath.to_string dp])
-
-let get_opaque = ref default_get_opaque
-let get_univ = ref default_get_univ
+let not_here () =
+  CErrors.user_err Pp.(str "Cannot access opaque delayed proof")
 
-let set_indirect_opaque_accessor f = (get_opaque := f)
-let set_indirect_univ_accessor f = (get_univ := f)
-(* /hooks *)
-
-let create cu = Direct ([],cu)
+let create ~univs cu = Direct (univs, [],cu)
 
 let turn_indirect dp o tab = match o with
   | Indirect (_,_,i) ->
       if not (Int.Map.mem i tab.opaque_val)
       then CErrors.anomaly (Pp.str "Indirect in a different table.")
       else CErrors.anomaly (Pp.str "Already an indirect opaque.")
-  | Direct (d,cu) ->
-      (** Uncomment to check dynamically that all terms turned into
-          indirections are hashconsed. *)
-(* let check_hcons c = let c' = hcons_constr c in assert (c' == c); c in *)
-(* let cu = Future.chain ~pure:true cu (fun (c, u) -> check_hcons c; c, u) in *)
+  | Direct (nunivs, d, cu) ->
+    (* Invariant: direct opaques only exist inside sections, we turn them
+      indirect as soon as we are at toplevel. At this moment, we perform
+      hashconsing of their contents, potentially as a future. *)
+      let hcons (c, u) =
+        let c = Constr.hcons c in
+        let u = Univ.hcons_universe_context_set u in
+        (c, u)
+      in
+      let cu = Future.chain cu hcons in
       let id = tab.opaque_len in
-      let opaque_val = Int.Map.add id (d,cu) tab.opaque_val in
+      let opaque_val = Int.Map.add id (nunivs, d,cu) tab.opaque_val in
       let opaque_dir =
         if DirPath.equal dp tab.opaque_dir then tab.opaque_dir
         else if DirPath.equal tab.opaque_dir DirPath.initial then dp
@@ -77,10 +77,10 @@ let subst_opaque sub = function
   | Indirect (s,dp,i) -> Indirect (sub::s,dp,i)
   | Direct _ -> CErrors.anomaly (Pp.str "Substituting a Direct opaque.")
 
-let discharge_direct_opaque ~cook_constr ci = function
+let discharge_direct_opaque ci = function
   | Indirect _ -> CErrors.anomaly (Pp.str "Not a direct opaque.")
-  | Direct (d,cu) ->
-      Direct (ci::d,Future.chain cu (fun (c, u) -> cook_constr c, u))
+  | Direct (n, d, cu) ->
+      Direct (n, ci :: d, cu)
 
 let join except cu = match except with
 | None -> ignore (Future.join cu)
@@ -89,57 +89,61 @@ let join except cu = match except with
   else ignore (Future.join cu)
 
 let join_opaque ?except { opaque_val = prfs; opaque_dir = odp; _ } = function
-  | Direct (_,cu) -> join except cu
+  | Direct (_,_,cu) -> join except cu
   | Indirect (_,dp,i) ->
       if DirPath.equal dp odp then
-        let fp = snd (Int.Map.find i prfs) in
+        let (_, _, fp) = Int.Map.find i prfs in
         join except fp
 
-let force_proof { opaque_val = prfs; opaque_dir = odp; _ } = function
-  | Direct (_,cu) ->
-      fst(Future.force cu)
+let force_proof access { opaque_val = prfs; opaque_dir = odp; _ } = function
+  | Direct (n, d, cu) ->
+    let (c, _) = Future.force cu in
+    access.access_discharge d n c
   | Indirect (l,dp,i) ->
-      let pt =
+      let c =
         if DirPath.equal dp odp
-        then Future.chain (snd (Int.Map.find i prfs)) fst
-        else !get_opaque dp i in
-      let c = Future.force pt in
+        then
+          let (n, d, cu) = Int.Map.find i prfs in
+          let (c, _) = Future.force cu in
+          access.access_discharge d n c
+        else match access.access_proof dp i with
+        | None -> not_here ()
+        | Some v -> v
+      in
       force_constr (List.fold_right subst_substituted l (from_val c))
 
-let force_constraints { opaque_val = prfs; opaque_dir = odp; _ } = function
-  | Direct (_,cu) -> snd(Future.force cu)
+let force_constraints _access { opaque_val = prfs; opaque_dir = odp; _ } = function
+  | Direct (_,_,cu) ->
+    snd(Future.force cu)
   | Indirect (_,dp,i) ->
       if DirPath.equal dp odp
-      then snd (Future.force (snd (Int.Map.find i prfs)))
-      else match !get_univ dp i with
-        | None -> Univ.ContextSet.empty
-        | Some u -> Future.force u
+      then
+        let (_, _, cu) = Int.Map.find i prfs in
+        snd (Future.force cu)
+      else Univ.ContextSet.empty
 
-let get_constraints { opaque_val = prfs; opaque_dir = odp; _ } = function
-  | Direct (_,cu) -> Some(Future.chain cu snd)
-  | Indirect (_,dp,i) ->
-      if DirPath.equal dp odp
-      then Some(Future.chain (snd (Int.Map.find i prfs)) snd)
-      else !get_univ dp i
+let get_direct_constraints = function
+| Indirect _ -> CErrors.anomaly (Pp.str "Not a direct opaque.")
+| Direct (_, _, cu) -> Future.chain cu snd
 
 module FMap = Future.UUIDMap
 
-let a_constr = Future.from_val (mkRel 1)
-let a_univ = Future.from_val Univ.ContextSet.empty
-let a_discharge : cooking_info list = []
-
-let dump { opaque_val = otab; opaque_len = n; _ } =
-  let opaque_table = Array.make n a_constr in
-  let univ_table = Array.make n a_univ in
-  let disch_table = Array.make n a_discharge in
+let dump ?(except = Future.UUIDSet.empty) { opaque_val = otab; opaque_len = n; _ } =
+  let opaque_table = Array.make n ([], 0, None) in
   let f2t_map = ref FMap.empty in
-  Int.Map.iter (fun n (d,cu) ->
-    let c, u = Future.split2 cu in
-    Future.sink u;
-    Future.sink c;
-    opaque_table.(n) <- c;
-    univ_table.(n) <- u;
-    disch_table.(n) <- d;
-    f2t_map := FMap.add (Future.uuid cu) n !f2t_map)
-  otab;
-  opaque_table, univ_table, disch_table, !f2t_map
+  let iter n (univs, d, cu) =
+    let uid = Future.uuid cu in
+    let () = f2t_map := FMap.add (Future.uuid cu) n !f2t_map in
+    let c =
+      if Future.is_val cu then
+        let (c, _) = Future.force cu in
+        Some c
+      else if Future.UUIDSet.mem uid except then None
+      else
+        CErrors.anomaly
+          Pp.(str"Proof object "++int n++str" is not checked nor to be checked")
+    in
+    opaque_table.(n) <- (d, univs, c)
+  in
+  let () = Int.Map.iter iter otab in
+  opaque_table, !f2t_map
diff --git a/kernel/opaqueproof.mli b/kernel/opaqueproof.mli
index 4e8956af06..6e275649cd 100644
--- a/kernel/opaqueproof.mli
+++ b/kernel/opaqueproof.mli
@@ -28,53 +28,42 @@ type opaque
 val empty_opaquetab : opaquetab
 
 (** From a [proofterm] to some [opaque]. *)
-val create : proofterm -> opaque
+val create : univs:int -> proofterm -> opaque
 
 (** Turn a direct [opaque] into an indirect one. It is your responsibility to
   hashcons the inner term beforehand. The integer is an hint of the maximum id
   used so far *)
 val turn_indirect : DirPath.t -> opaque -> opaquetab -> opaque * opaquetab
 
-(** From a [opaque] back to a [constr]. This might use the
-    indirect opaque accessor configured below. *)
-val force_proof : opaquetab -> opaque -> constr
-val force_constraints : opaquetab -> opaque -> Univ.ContextSet.t
-val get_constraints :
-  opaquetab -> opaque -> Univ.ContextSet.t Future.computation option
-
-val subst_opaque : substitution -> opaque -> opaque
-
-type work_list = (Univ.Instance.t * Id.t array) Cmap.t * 
+type work_list = (Univ.Instance.t * Id.t array) Cmap.t *
   (Univ.Instance.t * Id.t array) Mindmap.t
 
-type cooking_info = { 
-  modlist : work_list; 
+type cooking_info = {
+  modlist : work_list;
   abstract : Constr.named_context * Univ.Instance.t * Univ.AUContext.t }
 
-(* The type has two caveats:
-   1) cook_constr is defined after
-   2) we have to store the input in the [opaque] in order to be able to
-      discharge it when turning a .vi into a .vo *)
-val discharge_direct_opaque :
-  cook_constr:(constr -> constr) -> cooking_info -> opaque -> opaque
+type indirect_accessor = {
+  access_proof : DirPath.t -> int -> constr option;
+  access_discharge : cooking_info list -> int -> constr -> constr;
+}
+(** When stored indirectly, opaque terms are indexed by their library
+    dirpath and an integer index. The two functions above activate
+    this indirect storage, by telling how to retrieve terms.
+*)
 
-val join_opaque : ?except:Future.UUIDSet.t -> opaquetab -> opaque -> unit
+(** From a [opaque] back to a [constr]. This might use the
+    indirect opaque accessor given as an argument. *)
+val force_proof : indirect_accessor -> opaquetab -> opaque -> constr
+val force_constraints : indirect_accessor -> opaquetab -> opaque -> Univ.ContextSet.t
+val get_direct_constraints : opaque -> Univ.ContextSet.t Future.computation
 
-val dump : opaquetab ->
-  Constr.t Future.computation array *
-  Univ.ContextSet.t Future.computation array *
-  cooking_info list array *
-  int Future.UUIDMap.t
+val subst_opaque : substitution -> opaque -> opaque
 
-(** When stored indirectly, opaque terms are indexed by their library
-    dirpath and an integer index. The following two functions activate
-    this indirect storage, by telling how to store and retrieve terms.
-    Default creator always returns [None], preventing the creation of
-    any indirect link, and default accessor always raises an error.
-*)
+val discharge_direct_opaque :
+  cooking_info -> opaque -> opaque
 
-val set_indirect_opaque_accessor :
-  (DirPath.t -> int -> constr Future.computation) -> unit
-val set_indirect_univ_accessor :
-  (DirPath.t -> int -> Univ.ContextSet.t Future.computation option) -> unit
+val join_opaque : ?except:Future.UUIDSet.t -> opaquetab -> opaque -> unit
 
+val dump : ?except:Future.UUIDSet.t -> opaquetab ->
+  (cooking_info list * int * Constr.t option) array *
+  int Future.UUIDMap.t
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index a5d8a480ee..759cbe22ee 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -458,19 +458,11 @@ let labels_of_mib mib =
   Array.iter visit_mip mib.mind_packets;
   get ()
 
-let globalize_constant_universes env cb =
+let globalize_constant_universes cb =
   match cb.const_universes with
   | Monomorphic cstrs ->
-    Now (false, cstrs) ::
-    (match cb.const_body with
-     | (Undef _ | Def _ | Primitive _) -> []
-     | OpaqueDef lc ->
-       match Opaqueproof.get_constraints (Environ.opaque_tables env) lc with
-       | None -> []
-       | Some fc ->
-            match Future.peek_val fc with
-             | None -> [Later fc]
-             | Some c -> [Now (false, c)])
+    (* Constraints hidden in the opaque body are added by [add_constant_aux] *)
+    [Now (false, cstrs)]
   | Polymorphic _ ->
     [Now (true, Univ.ContextSet.empty)]
       
@@ -480,9 +472,9 @@ let globalize_mind_universes mb =
     [Now (false, ctx)]
   | Polymorphic _ -> [Now (true, Univ.ContextSet.empty)]
 
-let constraints_of_sfb env sfb = 
+let constraints_of_sfb sfb =
   match sfb with
-  | SFBconst cb -> globalize_constant_universes env cb
+  | SFBconst cb -> globalize_constant_universes cb
   | SFBmind mib -> globalize_mind_universes mib
   | SFBmodtype mtb -> [Now (false, mtb.mod_constraints)]
   | SFBmodule mb -> [Now (false, mb.mod_constraints)]
@@ -520,7 +512,8 @@ let add_field ?(is_include=false) ((l,sfb) as field) gn senv =
          separately. *)
       senv
     else
-      let cst = constraints_of_sfb senv.env sfb in
+      (* Delayed constraints from opaque body are added by [add_constant_aux] *)
+      let cst = constraints_of_sfb sfb in
       add_constraints_list cst senv
   in
   let env' = match sfb, gn with
@@ -553,6 +546,17 @@ type exported_private_constant =
 
 let add_constant_aux ~in_section senv (kn, cb) =
   let l = Constant.label kn in
+  let delayed_cst = match cb.const_body with
+  | OpaqueDef o when not (Declareops.constant_is_polymorphic cb) ->
+    let fc = Opaqueproof.get_direct_constraints o in
+    begin match Future.peek_val fc with
+    | None -> [Later fc]
+    | Some c -> [Now (false, c)]
+    end
+  | Undef _ | Def _ | Primitive _ | OpaqueDef _ -> []
+  in
+  (* This is the only place where we hashcons the contents of a constant body *)
+  let cb = if in_section then cb else Declareops.hcons_const_body cb in
   let cb, otab = match cb.const_body with
     | OpaqueDef lc when not in_section ->
       (* In coqc, opaque constants outside sections will be stored
@@ -565,6 +569,7 @@ let add_constant_aux ~in_section senv (kn, cb) =
   in
   let senv = { senv with env = Environ.set_opaque_tables senv.env otab } in
   let senv' = add_field (l,SFBconst cb) (C kn) senv in
+  let senv' = add_constraints_list delayed_cst senv' in
   let senv'' = match cb.const_body with
     | Undef (Some lev) ->
       update_resolver
@@ -645,18 +650,10 @@ let inline_side_effects env body side_eff =
     let body = List.fold_right fold_arg args body in
     (body, ctx, sigs)
 
-let inline_private_constants_in_definition_entry env ce =
-  let open Entries in
-  { ce with
-  const_entry_body = Future.chain
-    ce.const_entry_body (fun ((body, ctx), side_eff) ->
-      let body, ctx',_ = inline_side_effects env body side_eff in
-      let ctx' = Univ.ContextSet.union ctx ctx' in
-      (body, ctx'), ());
-  }
-
-let inline_private_constants_in_constr env body side_eff =
-  pi1 (inline_side_effects env body side_eff)
+let inline_private_constants env ((body, ctx), side_eff) =
+  let body, ctx',_ = inline_side_effects env body side_eff in
+  let ctx' = Univ.ContextSet.union ctx ctx' in
+  (body, ctx')
 
 let is_suffix l suf = match l with
 | [] -> false
@@ -709,13 +706,7 @@ let constant_entry_of_side_effect eff =
 let export_eff eff =
   (eff.seff_constant, eff.seff_body, eff.seff_role)
 
-let export_side_effects mb env c =
-  let open Entries in
-      let body = c.const_entry_body in
-      let _, eff = Future.force body in
-      let ce = { c with
-        Entries.const_entry_body = Future.chain body
-          (fun (b_ctx, _) -> b_ctx, ()) } in
+let export_side_effects mb env (b_ctx, eff) =
       let not_exists e =
         try ignore(Environ.lookup_constant e.seff_constant env); false
         with Not_found -> true in
@@ -739,7 +730,7 @@ let export_side_effects mb env c =
       in
       let rec translate_seff sl seff acc env =
         match seff with
-        | [] -> List.rev acc, ce
+        | [] -> List.rev acc, b_ctx
         | eff :: rest ->
           if Int.equal sl 0 then
             let env, cb =
@@ -758,9 +749,13 @@ let export_side_effects mb env c =
      in
        translate_seff trusted seff [] env
 
+let n_univs cb = match cb.const_universes with
+| Monomorphic _ -> 0
+| Polymorphic auctx -> Univ.AUContext.size auctx
+
 let export_private_constants ~in_section ce senv =
   let exported, ce = export_side_effects senv.revstruct senv.env ce in
-  let map (kn, cb, _) = (kn, map_constant (fun p -> Opaqueproof.create (Future.from_val p)) cb) in
+  let map (kn, cb, _) = (kn, map_constant (fun p -> Opaqueproof.create ~univs:(n_univs cb) (Future.from_val p)) cb) in
   let bodies = List.map map exported in
   let exported = List.map (fun (kn, _, r) -> (kn, r)) exported in
   let senv = List.fold_left (add_constant_aux ~in_section) senv bodies in
@@ -768,8 +763,7 @@ let export_private_constants ~in_section ce senv =
 
 let add_recipe ~in_section l r senv =
   let kn = Constant.make2 senv.modpath l in
-  let cb = Term_typing.translate_recipe ~hcons:(not in_section) senv.env kn r in
-  let cb = if in_section then cb else Declareops.hcons_const_body cb in
+  let cb = Term_typing.translate_recipe senv.env kn r in
   let senv = add_constant_aux ~in_section senv (kn, cb) in
   kn, senv
 
@@ -788,7 +782,7 @@ let add_constant ?role ~in_section l decl senv =
         Term_typing.translate_constant Term_typing.Pure senv.env kn ce
     in
   let senv =
-    let cb = map_constant Opaqueproof.create cb in
+    let cb = map_constant (fun c -> Opaqueproof.create ~univs:(n_univs cb) c) cb in
     add_constant_aux ~in_section senv (kn, cb) in
   let senv =
     match decl with
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 36ca3d8c47..770caf5406 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -49,10 +49,8 @@ val concat_private : private_constants -> private_constants -> private_constants
     [e1] must be more recent than those of [e2]. *)
 
 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 -> unit Entries.definition_entry
+val inline_private_constants :
+  Environ.env -> private_constants Entries.proof_output -> Constr.constr Univ.in_universe_context_set
 
 val push_private_constants : Environ.env -> private_constants -> Environ.env
 (** Push the constants in the environment if not already there. *)
@@ -93,8 +91,8 @@ type exported_private_constant =
   Constant.t * Entries.side_effect_role
 
 val export_private_constants : in_section:bool ->
-  private_constants Entries.definition_entry ->
-  (unit Entries.definition_entry * exported_private_constant list) safe_transformer
+  private_constants Entries.proof_output ->
+  (Constr.constr Univ.in_universe_context_set * 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) *)
diff --git a/kernel/sorts.ml b/kernel/sorts.ml
index 09c98ca1bc..b5a929697e 100644
--- a/kernel/sorts.ml
+++ b/kernel/sorts.ml
@@ -91,6 +91,8 @@ let family_compare a b = match a,b with
 
 let family_equal = (==)
 
+let family_leq a b = family_compare a b <= 0
+
 open Hashset.Combine
 
 let hash = function
@@ -101,11 +103,6 @@ let hash = function
     let h = Univ.Universe.hash u in
     combinesmall 2 h
 
-module List = struct
-  let mem = List.memq
-  let intersect l l' = CList.intersect family_equal l l'
-end
-
 module Hsorts =
   Hashcons.Make(
     struct
diff --git a/kernel/sorts.mli b/kernel/sorts.mli
index c49728b146..3769e31465 100644
--- a/kernel/sorts.mli
+++ b/kernel/sorts.mli
@@ -37,11 +37,7 @@ val hcons : t -> t
 
 val family_compare : family -> family -> int
 val family_equal : family -> family -> bool
-
-module List : sig
-  val mem : family -> family list -> bool
-  val intersect : family list -> family list -> family list
-end
+val family_leq : family -> family -> bool
 
 val univ_of_sort : t -> Univ.Universe.t
 val sort_of_univ : Univ.Universe.t -> t
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 74c6189a65..f984088f47 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -74,7 +74,7 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
       let j = Typeops.infer env t in
       let usubst, univs = Declareops.abstract_universes uctx in
       let r = Typeops.assumption_of_judgment env j in
-      let t = Constr.hcons (Vars.subst_univs_level_constr usubst j.uj_val) in
+      let t = Vars.subst_univs_level_constr usubst j.uj_val in
       {
         Cooking.cook_body = Undef nl;
         cook_type = t;
@@ -95,7 +95,7 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
       | Some typ ->
         let typ = Typeops.infer_type env typ in
         Typeops.check_primitive_type env op_t typ.utj_val;
-        Constr.hcons typ.utj_val
+        typ.utj_val
       | None ->
         match op_t with
         | CPrimitives.OT_op op -> Typeops.type_of_prim env op
@@ -115,16 +115,8 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
       }
 
   (** Definition [c] is opaque (Qed), non polymorphic and with a specified type,
-      so we delay the typing and hash consing of its body.
-      Remark: when the universe quantification is given explicitly, we could
-      delay even in the polymorphic case.  *)
+      so we delay the typing and hash consing of its body. *)
 
-(** Definition is opaque (Qed) and non polymorphic with known type, so we delay
-the typing and hash consing of its body.
-
-TODO: if the universe quantification is given explicitly, we could delay even in
-the polymorphic case
-  *)
   | DefinitionEntry ({ const_entry_type = Some typ;
                        const_entry_opaque = true;
                        const_entry_universes = Monomorphic_entry univs; _ } as c) ->
@@ -151,7 +143,7 @@ the polymorphic case
             let _ = Typeops.judge_of_cast env j DEFAULTcast tyj in
             j, uctx
           in
-          let c = Constr.hcons j.uj_val in
+          let c = j.uj_val in
           feedback_completion_typecheck feedback_id;
           c, uctx) in
       let def = OpaqueDef proofterm in
@@ -165,16 +157,59 @@ the polymorphic case
         cook_context = c.const_entry_secctx;
       }
 
+  (** Similar case for polymorphic entries. TODO: also delay type-checking of
+      the body. *)
+
+  | DefinitionEntry ({ const_entry_type = Some typ;
+                       const_entry_opaque = true;
+                       const_entry_universes = Polymorphic_entry (nas, uctx); _ } as c) ->
+      let { const_entry_body = body; const_entry_feedback = feedback_id; _ } = c in
+      let env = push_context ~strict:false uctx env in
+      let tj = Typeops.infer_type env typ in
+      let sbst, auctx = Univ.abstract_universes nas uctx in
+      let usubst = Univ.make_instance_subst sbst in
+      let (def, private_univs) =
+        let (body, ctx), side_eff = Future.join body in
+        let body, ctx = match trust with
+        | Pure -> body, ctx
+        | SideEffects handle ->
+          let body, ctx', _ = handle env body side_eff in
+          body, Univ.ContextSet.union ctx ctx'
+        in
+        (** [ctx] must contain local universes, such that it has no impact
+            on the rest of the graph (up to transitivity). *)
+        let env = push_subgraph ctx env in
+        let private_univs = on_snd (Univ.subst_univs_level_constraints usubst) ctx in
+        let j = Typeops.infer env body in
+        let _ = Typeops.judge_of_cast env j DEFAULTcast tj in
+        let def = Vars.subst_univs_level_constr usubst j.uj_val in
+        def, private_univs
+      in
+      let def = OpaqueDef (Future.from_val (def, Univ.ContextSet.empty)) in
+      let typ = Vars.subst_univs_level_constr usubst tj.utj_val in
+        feedback_completion_typecheck feedback_id;
+      {
+        Cooking.cook_body = def;
+        cook_type = typ;
+        cook_universes = Polymorphic auctx;
+        cook_private_univs = Some private_univs;
+        cook_relevance = Sorts.relevance_of_sort tj.utj_type;
+        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_type = typ; _ } = c in
       let { const_entry_body = body; const_entry_feedback = feedback_id; _ } = c in
-      let (body, ctx), side_eff = Future.join body in
+      (* Opaque constants must be provided with a non-empty const_entry_type,
+         and thus should have been treated above. *)
+      let () = assert (not c.const_entry_opaque) in
       let body, ctx = match trust with
-      | Pure -> body, ctx
-      | SideEffects handle ->
-        let body, ctx', _ = handle env body side_eff in
-        body, Univ.ContextSet.union ctx ctx'
+      | Pure ->
+        let (body, ctx), () = Future.join body in
+        body, ctx
+      | SideEffects _ -> assert false
       in
       let env, usubst, univs, private_univs = match c.const_entry_universes with
       | Monomorphic_entry univs ->
@@ -188,9 +223,6 @@ the polymorphic case
         let sbst, auctx = Univ.abstract_universes nas uctx in
         let sbst = Univ.make_instance_subst sbst in
         let env, local =
-          if opaque then
-            push_subgraph ctx env, Some (on_snd (Univ.subst_univs_level_constraints sbst) ctx)
-          else
           if Univ.ContextSet.is_empty ctx then env, None
           else CErrors.anomaly Pp.(str "Local universes in non-opaque polymorphic definition.")
         in
@@ -205,11 +237,8 @@ the polymorphic case
            let _ = Typeops.judge_of_cast env j DEFAULTcast tj in
            Vars.subst_univs_level_constr usubst tj.utj_val
       in
-      let def = Constr.hcons (Vars.subst_univs_level_constr usubst j.uj_val) in
-      let def = 
-        if opaque then OpaqueDef (Future.from_val (def, Univ.ContextSet.empty))
-	else Def (Mod_subst.from_val def) 
-      in
+      let def = Vars.subst_univs_level_constr usubst j.uj_val in
+      let def = Def (Mod_subst.from_val def) in
 	feedback_completion_typecheck feedback_id;
       {
         Cooking.cook_body = def;
@@ -328,9 +357,9 @@ let translate_local_assum env t =
   let t = Typeops.assumption_of_judgment env j in
     j.uj_val, t
 
-let translate_recipe ~hcons env _kn r =
+let translate_recipe env _kn r =
   let open Cooking in
-  let result = Cooking.cook_constant ~hcons r in
+  let result = Cooking.cook_constant r in
   let univs = result.cook_universes in
   let res = Cbytegen.compile_constant_body ~fail_on_error:false env univs result.cook_body in
   let tps = Option.map Cemitcodes.from_val res in
diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli
index 592a97e132..fd0f2a18e4 100644
--- a/kernel/term_typing.mli
+++ b/kernel/term_typing.mli
@@ -35,7 +35,7 @@ val translate_constant :
   'a trust -> env -> Constant.t -> 'a constant_entry ->
     Opaqueproof.proofterm constant_body
 
-val translate_recipe : hcons:bool -> env -> Constant.t -> Cooking.recipe -> Opaqueproof.opaque constant_body
+val translate_recipe : env -> Constant.t -> Cooking.recipe -> Opaqueproof.opaque constant_body
 
 (** Internal functions, mentioned here for debug purpose only *)
 
diff --git a/kernel/type_errors.ml b/kernel/type_errors.ml
index c45fe1cf00..857e4fabf7 100644
--- a/kernel/type_errors.ml
+++ b/kernel/type_errors.ml
@@ -49,7 +49,7 @@ type ('constr, 'types) ptype_error =
   | BadAssumption of ('constr, 'types) punsafe_judgment
   | ReferenceVariables of Id.t * 'constr
   | ElimArity of pinductive * 'constr * ('constr, 'types) punsafe_judgment
-      * (Sorts.family list * Sorts.family * Sorts.family * arity_error) option
+      * (Sorts.family * Sorts.family * Sorts.family * arity_error) option
   | CaseNotInductive of ('constr, 'types) punsafe_judgment
   | WrongCaseInfo of pinductive * case_info
   | NumberBranches of ('constr, 'types) punsafe_judgment * int
diff --git a/kernel/type_errors.mli b/kernel/type_errors.mli
index 88165a4f07..8e25236851 100644
--- a/kernel/type_errors.mli
+++ b/kernel/type_errors.mli
@@ -50,7 +50,7 @@ type ('constr, 'types) ptype_error =
   | BadAssumption of ('constr, 'types) punsafe_judgment
   | ReferenceVariables of Id.t * 'constr
   | ElimArity of pinductive * 'constr * ('constr, 'types) punsafe_judgment
-      * (Sorts.family list * Sorts.family * Sorts.family * arity_error) option
+      * (Sorts.family * Sorts.family * Sorts.family * arity_error) option
   | CaseNotInductive of ('constr, 'types) punsafe_judgment
   | WrongCaseInfo of pinductive * case_info
   | NumberBranches of ('constr, 'types) punsafe_judgment * int
@@ -104,7 +104,7 @@ val error_reference_variables : env -> Id.t -> constr -> 'a
 
 val error_elim_arity :
   env -> pinductive -> constr -> unsafe_judgment ->
-      (Sorts.family list * Sorts.family * Sorts.family * arity_error) option -> 'a
+      (Sorts.family * Sorts.family * Sorts.family * arity_error) option -> 'a
 
 val error_case_not_inductive : env -> unsafe_judgment -> 'a
 
diff --git a/kernel/uint63.mli b/kernel/uint63.mli
index f25f24512d..93632da110 100644
--- a/kernel/uint63.mli
+++ b/kernel/uint63.mli
@@ -13,7 +13,7 @@ val of_uint : int -> t
 
 val hash : t -> int
 
-     (* convertion to a string *)
+     (* conversion to a string *)
 val to_string : t -> string
 val of_string : string -> t
 
diff --git a/kernel/univ.ml b/kernel/univ.ml
index b1bbc25fe6..2b88d6884d 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -726,7 +726,7 @@ let univ_level_rem u v min =
   | Some u' -> if Level.equal u u' then min else v
   | None -> List.filter (fun (l, n) -> not (Int.equal n 0 && Level.equal u l)) v
 
-(* Is u mentionned in v (or equals to v) ? *)
+(* Is u mentioned in v (or equals to v) ? *)
 
 
 (**********************************************************************)
diff --git a/kernel/univ.mli b/kernel/univ.mli
index db178c4bb0..ddb204dd52 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -163,7 +163,7 @@ val super : Universe.t -> Universe.t
 
 val universe_level : Universe.t -> Level.t option
 
-(** [univ_level_mem l u] Is l is mentionned in u ? *)
+(** [univ_level_mem l u] Is l is mentioned in u ? *)
 
 val univ_level_mem : Level.t -> Universe.t -> bool
 
diff --git a/kernel/vmvalues.ml b/kernel/vmvalues.ml
index 777a207013..88fcb71e77 100644
--- a/kernel/vmvalues.ml
+++ b/kernel/vmvalues.ml
@@ -11,10 +11,10 @@ open Names
 open Univ
 open Constr
 
-(*******************************************)
-(* Initalization of the abstract machine ***)
-(* Necessary for [relaccu_tbl]             *)
-(*******************************************)
+(********************************************)
+(* Initialization of the abstract machine ***)
+(* Necessary for [relaccu_tbl]              *)
+(********************************************)
 
 external init_vm : unit -> unit = "init_coq_vm"