Merge PR #10884: Last stop before CEP 40

Reviewed-by: SkySkimmer
Reviewed-by: ejgallego
Reviewed-by: gares

5 files changed, 192 insertions, 196 deletions

diff --git a/kernel/entries.ml b/kernel/entries.ml
index 1e6bc14935..046ea86872 100644
--- a/kernel/entries.ml
+++ b/kernel/entries.ml
@@ -99,14 +99,10 @@ type primitive_entry = {
 type 'a proof_output = constr Univ.in_universe_context_set * 'a
 type 'a const_entry_body = 'a proof_output Future.computation
 
-(** Dummy wrapper type discriminable from unit *)
-type 'a seff_wrap = { seff_wrap : 'a }
-
-type _ constant_entry =
-  | DefinitionEntry : definition_entry -> unit constant_entry
-  | OpaqueEntry : 'a const_entry_body opaque_entry -> 'a seff_wrap constant_entry
-  | ParameterEntry : parameter_entry -> unit constant_entry
-  | PrimitiveEntry : primitive_entry -> unit constant_entry
+type constant_entry =
+  | DefinitionEntry : definition_entry -> constant_entry
+  | ParameterEntry : parameter_entry -> constant_entry
+  | PrimitiveEntry : primitive_entry -> constant_entry
 
 (** {6 Modules } *)
 
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 98465c070b..00559206ee 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -299,13 +299,6 @@ let lift_constant c =
   in
   { c with const_body = body }
 
-let map_constant f c =
-  let body = match c.const_body with
-  | OpaqueDef o -> OpaqueDef (f o)
-  | Def _ | Undef _ | Primitive _ as body -> body
-  in
-  { c with const_body = body }
-
 let push_private_constants env eff =
   let eff = side_effects_of_private_constants eff in
   let add_if_undefined env eff =
@@ -579,13 +572,9 @@ let add_field ?(is_include=false) ((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 Entries.seff_wrap effect_entry
-| PureEntry : unit effect_entry
-
 type global_declaration =
-  | ConstantEntry : 'a effect_entry * 'a Entries.constant_entry -> global_declaration
+| ConstantEntry : Entries.constant_entry -> global_declaration
+| OpaqueEntry : private_constants Entries.const_entry_body Entries.opaque_entry -> global_declaration
 
 type exported_private_constant = Constant.t
 
@@ -704,7 +693,7 @@ let check_signatures curmb sl =
 
 type side_effect_declaration =
 | DefinitionEff : Entries.definition_entry -> side_effect_declaration
-| OpaqueEff : unit Entries.const_entry_body Entries.opaque_entry -> side_effect_declaration
+| OpaqueEff : Constr.constr Entries.opaque_entry -> side_effect_declaration
 
 let constant_entry_of_side_effect eff =
   let cb = eff.seff_body in
@@ -723,7 +712,7 @@ let constant_entry_of_side_effect eff =
     | _ -> assert false in
   if Declareops.is_opaque cb then
   OpaqueEff {
-    opaque_entry_body = Future.from_val ((p, Univ.ContextSet.empty), ());
+    opaque_entry_body = p;
     opaque_entry_secctx = Context.Named.to_vars cb.const_hyps;
     opaque_entry_feedback = None;
     opaque_entry_type = cb.const_type;
@@ -741,6 +730,25 @@ let constant_entry_of_side_effect eff =
 let export_eff eff =
   (eff.seff_constant, eff.seff_body)
 
+let is_empty_private = function
+| Opaqueproof.PrivateMonomorphic ctx -> Univ.ContextSet.is_empty ctx
+| Opaqueproof.PrivatePolymorphic (_, ctx) -> Univ.ContextSet.is_empty ctx
+
+let empty_private univs = match univs with
+| Monomorphic _ -> Opaqueproof.PrivateMonomorphic Univ.ContextSet.empty
+| Polymorphic auctx -> Opaqueproof.PrivatePolymorphic (Univ.AUContext.size auctx, Univ.ContextSet.empty)
+
+(* Special function to call when the body of an opaque definition is provided.
+  It performs the type-checking of the body immediately. *)
+let translate_direct_opaque env kn ce =
+  let cb, ctx = Term_typing.translate_opaque env kn ce in
+  let body = ce.Entries.opaque_entry_body, Univ.ContextSet.empty in
+  let handle _env c () = (c, Univ.ContextSet.empty, 0) in
+  let (c, u) = Term_typing.check_delayed handle ctx (body, ()) in
+  (* No constraints can be generated, we set it empty everywhere *)
+  let () = assert (is_empty_private u) in
+  { cb with const_body = OpaqueDef c }
+
 let export_side_effects mb env (b_ctx, eff) =
       let not_exists e =
         try ignore(Environ.lookup_constant e.seff_constant env); false
@@ -765,26 +773,14 @@ let export_side_effects mb env (b_ctx, eff) =
           if Int.equal sl 0 then
             let env, cb =
               let kn = eff.seff_constant in
-               let ce = constant_entry_of_side_effect eff in
-               let open Entries in
-               let open Term_typing in
-               let cb = match ce with
-               | DefinitionEff ce ->
-                Term_typing.translate_constant Pure env kn (DefinitionEntry ce)
-               | OpaqueEff ce ->
-                let handle _env c () = (c, Univ.ContextSet.empty, 0) in
-                Term_typing.translate_constant (SideEffects handle) env kn (OpaqueEntry ce)
-               in
-              let map cu =
-                let (c, u) = Future.force cu in
-                let () = match u with
-                | Opaqueproof.PrivateMonomorphic ctx
-                | Opaqueproof.PrivatePolymorphic (_, ctx) ->
-                  assert (Univ.ContextSet.is_empty ctx)
-                in
-                c
+              let ce = constant_entry_of_side_effect eff in
+              let open Entries in
+              let cb = match ce with
+              | DefinitionEff ce ->
+                Term_typing.translate_constant env kn (DefinitionEntry ce)
+              | OpaqueEff ce ->
+                translate_direct_opaque env kn ce
               in
-               let cb = map_constant map cb in
                let eff = { eff with seff_body = cb } in
                (push_seff env eff, export_eff eff)
             in
@@ -805,10 +801,7 @@ let export_private_constants ce senv =
   let exported, ce = export_side_effects senv.revstruct senv.env ce in
   let map senv (kn, c) = match c.const_body with
   | OpaqueDef p ->
-    let local = match c.const_universes with
-    | Monomorphic _ -> Opaqueproof.PrivateMonomorphic Univ.ContextSet.empty
-    | Polymorphic auctx -> Opaqueproof.PrivatePolymorphic (Univ.AUContext.size auctx, Univ.ContextSet.empty)
-    in
+    let local = empty_private c.const_universes in
     let senv, o = push_opaque_proof (Future.from_val (p, local)) senv in
     senv, (kn, { c with const_body = OpaqueDef o })
   | Def _ | Undef _ | Primitive _ as body ->
@@ -820,19 +813,22 @@ let export_private_constants ce senv =
   let senv = List.fold_left add_constant_aux senv bodies in
   (ce, exported), senv
 
-let add_constant (type a) ~(side_effect : a effect_entry) l decl senv : (Constant.t * a) * safe_environment =
+let add_constant l decl senv =
   let kn = Constant.make2 senv.modpath l in
-    let cb = 
+    let cb =
       match decl with
-      | ConstantEntry (EffectEntry, ce) ->
+      | OpaqueEntry ce ->
         let handle env body eff =
           let body, uctx, signatures = inline_side_effects env body eff in
           let trusted = check_signatures senv.revstruct signatures in
           body, uctx, trusted
         in
-        Term_typing.translate_constant (Term_typing.SideEffects handle) senv.env kn ce
-      | ConstantEntry (PureEntry, ce) ->
-        Term_typing.translate_constant Term_typing.Pure senv.env kn ce
+        let cb, ctx = Term_typing.translate_opaque senv.env kn ce in
+        let map pf = Term_typing.check_delayed handle ctx pf in
+        let pf = Future.chain ce.Entries.opaque_entry_body map in
+        { cb with const_body = OpaqueDef pf }
+      | ConstantEntry ce ->
+        Term_typing.translate_constant senv.env kn ce
     in
   let senv =
     let senv, cb, delayed_cst = match cb.const_body with
@@ -860,37 +856,39 @@ let add_constant (type a) ~(side_effect : a effect_entry) l decl senv : (Constan
 
   let senv =
     match decl with
-    | ConstantEntry (_,(Entries.PrimitiveEntry { Entries.prim_entry_content = CPrimitives.OT_type t; _ })) ->
+    | ConstantEntry (Entries.PrimitiveEntry { Entries.prim_entry_content = CPrimitives.OT_type t; _ }) ->
       if sections_are_opened senv then CErrors.anomaly (Pp.str "Primitive type not allowed in sections");
       add_retroknowledge (Retroknowledge.Register_type(t,kn)) senv
     | _ -> senv
   in
-  let eff : a = match side_effect with
-  | PureEntry -> ()
-  | EffectEntry ->
-    let body, univs = match cb.const_body with
-    | (Primitive _ | Undef _) -> assert false
-    | Def c -> (Def c, cb.const_universes)
-    | OpaqueDef o ->
-      let (b, delayed) = Future.force o in
-      match cb.const_universes, delayed with
-      | Monomorphic ctx', Opaqueproof.PrivateMonomorphic ctx ->
-        OpaqueDef b, Monomorphic (Univ.ContextSet.union ctx ctx')
-      | Polymorphic auctx, Opaqueproof.PrivatePolymorphic (_, ctx) ->
-        (* Upper layers enforce that there are no internal constraints *)
-        let () = assert (Univ.ContextSet.is_empty ctx) in
-        OpaqueDef b, Polymorphic auctx
-      | (Monomorphic _ | Polymorphic _), (Opaqueproof.PrivateMonomorphic _ | Opaqueproof.PrivatePolymorphic _) ->
-        assert false
+  kn, senv
+
+let add_private_constant l decl senv : (Constant.t * private_constants) * safe_environment =
+  let kn = Constant.make2 senv.modpath l in
+    let cb =
+      match decl with
+      | OpaqueEff ce ->
+        translate_direct_opaque senv.env kn ce
+      | DefinitionEff ce ->
+        Term_typing.translate_constant senv.env kn (Entries.DefinitionEntry ce)
     in
-    let cb = { cb with const_body = body; const_universes = univs } in
+  let senv, dcb = match cb.const_body with
+  | Def _ as const_body -> senv, { cb with const_body }
+  | OpaqueDef c ->
+    let local = empty_private cb.const_universes in
+    let senv, o = push_opaque_proof (Future.from_val (c, local)) senv in
+    senv, { cb with const_body = OpaqueDef o }
+  | Undef _ | Primitive _ -> assert false
+  in
+  let senv = add_constant_aux senv (kn, dcb) in
+  let eff =
     let from_env = CEphemeron.create senv.revstruct in
     let eff = {
       from_env = from_env;
       seff_constant = kn;
       seff_body = cb;
     } in
-    { Entries.seff_wrap = SideEffects.add eff empty_private_constants }
+    SideEffects.add eff empty_private_constants
   in
   (kn, eff), senv
 
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 1ce790ebbb..b2f6668577 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -73,12 +73,13 @@ val is_joined_environment : safe_environment -> bool
 
 (** Insertion of global axioms or definitions *)
 
-type 'a effect_entry =
-| EffectEntry : private_constants Entries.seff_wrap effect_entry
-| PureEntry : unit effect_entry
-
 type global_declaration =
-  | ConstantEntry : 'a effect_entry * 'a Entries.constant_entry -> global_declaration
+| ConstantEntry : Entries.constant_entry -> global_declaration
+| OpaqueEntry : private_constants Entries.const_entry_body Entries.opaque_entry -> global_declaration
+
+type side_effect_declaration =
+| DefinitionEff : Entries.definition_entry -> side_effect_declaration
+| OpaqueEff : Constr.constr Entries.opaque_entry -> side_effect_declaration
 
 type exported_private_constant = Constant.t
 
@@ -86,10 +87,13 @@ val export_private_constants :
   private_constants Entries.proof_output ->
   (Constr.constr Univ.in_universe_context_set * exported_private_constant list) safe_transformer
 
-(** returns the main constant plus a certificate of its validity *)
+(** returns the main constant *)
 val add_constant :
-  side_effect:'a effect_entry -> Label.t -> global_declaration ->
-    (Constant.t * 'a) safe_transformer
+  Label.t -> global_declaration -> Constant.t safe_transformer
+
+(** Similar to add_constant but also returns a certificate *)
+val add_private_constant :
+  Label.t -> side_effect_declaration -> (Constant.t * private_constants) safe_transformer
 
 (** Adding an inductive type *)
 
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index f70b2960cf..f85b3db413 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -29,10 +29,6 @@ module NamedDecl = Context.Named.Declaration
 type 'a effect_handler =
   env -> Constr.t -> 'a -> (Constr.t * Univ.ContextSet.t * int)
 
-type _ trust =
-| Pure : unit trust
-| SideEffects : 'a effect_handler -> 'a Entries.seff_wrap trust
-
 let skip_trusted_seff sl b e =
   let rec aux sl b e acc =
     let open Context.Rel.Declaration in
@@ -64,7 +60,11 @@ let feedback_completion_typecheck =
   Option.iter (fun state_id ->
       Feedback.feedback ~id:state_id Feedback.Complete)
 
-let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
+type typing_context =
+| MonoTyCtx of Environ.env * unsafe_type_judgment * Univ.ContextSet.t * Id.Set.t * Stateid.t option
+| PolyTyCtx of Environ.env * unsafe_type_judgment * Univ.universe_level_subst * Univ.AUContext.t * Id.Set.t * Stateid.t option
+
+let infer_declaration env (dcl : constant_entry) =
   match dcl with
     | ParameterEntry (ctx,(t,uctx),nl) ->
       let env = match uctx with
@@ -112,79 +112,9 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
         cook_relevance = Sorts.Relevant;
       }
 
-  (** Definition [c] is opaque (Qed), non polymorphic and with a specified type,
-      so we delay the typing and hash consing of its body. *)
-
-  | OpaqueEntry ({ opaque_entry_type = typ;
-                       opaque_entry_universes = Monomorphic_entry univs; _ } as c) ->
-      let env = push_context_set ~strict:true univs env in
-      let { opaque_entry_body = body; opaque_entry_feedback = feedback_id; _ } = c in
-      let tyj = Typeops.infer_type env typ in
-      let proofterm =
-        Future.chain body begin fun ((body,uctx),side_eff) ->
-          (* don't redeclare universes which are declared for the type *)
-          let uctx = Univ.ContextSet.diff uctx univs in
-          let SideEffects handle = trust in
-          let (body, uctx', valid_signatures) = handle env body side_eff in
-          let uctx = Univ.ContextSet.union uctx uctx' in
-          let env = push_context_set uctx env in
-          let body,env,ectx = skip_trusted_seff valid_signatures body env in
-          let j = Typeops.infer env body in
-          let j = unzip ectx j in
-          let _ = Typeops.judge_of_cast env j DEFAULTcast tyj in
-          let c = j.uj_val in
-          feedback_completion_typecheck feedback_id;
-          c, Opaqueproof.PrivateMonomorphic uctx
-      end in
-      let def = OpaqueDef proofterm in
-      {
-        Cooking.cook_body = def;
-        cook_type = tyj.utj_val;
-        cook_universes = Monomorphic univs;
-        cook_relevance = Sorts.relevance_of_sort tyj.utj_type;
-        cook_inline = false;
-        cook_context = Some c.opaque_entry_secctx;
-      }
-
-  (** Similar case for polymorphic entries. *)
-
-  | OpaqueEntry ({ opaque_entry_type = typ;
-                       opaque_entry_universes = Polymorphic_entry (nas, uctx); _ } as c) ->
-      let { opaque_entry_body = body; opaque_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 proofterm = Future.chain body begin fun ((body, ctx), side_eff) ->
-        let SideEffects handle = trust in
-        let body, ctx', _ = handle env body side_eff in
-        let ctx = 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
-        let () = feedback_completion_typecheck feedback_id in
-        def, Opaqueproof.PrivatePolymorphic (Univ.AUContext.size auctx, private_univs)
-      end in
-      let def = OpaqueDef proofterm in
-      let typ = Vars.subst_univs_level_constr usubst tj.utj_val in
-      {
-        Cooking.cook_body = def;
-        cook_type = typ;
-        cook_universes = Polymorphic auctx;
-        cook_relevance = Sorts.relevance_of_sort tj.utj_type;
-        cook_inline = false;
-        cook_context = Some c.opaque_entry_secctx;
-      }
-
-  (** Other definitions have to be processed immediately. *)
   | DefinitionEntry c ->
       let { const_entry_type = typ; _ } = c in
       let { const_entry_body = body; const_entry_feedback = feedback_id; _ } = c in
-      let Pure = trust in
       let env, usubst, univs = match c.const_entry_universes with
       | Monomorphic_entry ctx ->
         let env = push_context_set ~strict:true ctx env in
@@ -218,25 +148,66 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
         cook_context = c.const_entry_secctx;
       }
 
+(** Definition is opaque (Qed), so we delay the typing of its body. *)
+let infer_opaque env = function
+  | ({ opaque_entry_type = typ;
+                       opaque_entry_universes = Monomorphic_entry univs; _ } as c) ->
+      let env = push_context_set ~strict:true univs env in
+      let { opaque_entry_feedback = feedback_id; _ } = c in
+      let tyj = Typeops.infer_type env typ in
+      let context = MonoTyCtx (env, tyj, univs, c.opaque_entry_secctx, feedback_id) in
+      let def = OpaqueDef () in
+      {
+        Cooking.cook_body = def;
+        cook_type = tyj.utj_val;
+        cook_universes = Monomorphic univs;
+        cook_relevance = Sorts.relevance_of_sort tyj.utj_type;
+        cook_inline = false;
+        cook_context = Some c.opaque_entry_secctx;
+      }, context
+
+  | ({ opaque_entry_type = typ;
+                       opaque_entry_universes = Polymorphic_entry (nas, uctx); _ } as c) ->
+      let { opaque_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 context = PolyTyCtx (env, tj, usubst, auctx, c.opaque_entry_secctx, feedback_id) in
+      let def = OpaqueDef () in
+      let typ = Vars.subst_univs_level_constr usubst tj.utj_val in
+      {
+        Cooking.cook_body = def;
+        cook_type = typ;
+        cook_universes = Polymorphic auctx;
+        cook_relevance = Sorts.relevance_of_sort tj.utj_type;
+        cook_inline = false;
+        cook_context = Some c.opaque_entry_secctx;
+      }, context
+
+let check_section_variables env declared_set typ body =
+  let ids_typ = global_vars_set env typ in
+  let ids_def = global_vars_set env body in
+  let inferred_set = Environ.really_needed env (Id.Set.union ids_typ ids_def) in
+  if not (Id.Set.subset inferred_set declared_set) then
+    let l = Id.Set.elements (Id.Set.diff inferred_set declared_set) in
+    let n = List.length l in
+    let declared_vars = Pp.pr_sequence Id.print (Id.Set.elements declared_set) in
+    let inferred_vars = Pp.pr_sequence Id.print (Id.Set.elements inferred_set) in
+    let missing_vars  = Pp.pr_sequence Id.print (List.rev l) in
+    user_err Pp.(prlist str
+        ["The following section "; (String.plural n "variable"); " ";
+        (String.conjugate_verb_to_be n); " used but not declared:"] ++ fnl () ++
+        missing_vars ++ str "." ++ fnl () ++ fnl () ++
+        str "You can either update your proof to not depend on " ++ missing_vars ++
+        str ", or you can update your Proof line from" ++ fnl () ++
+        str "Proof using " ++ declared_vars ++ fnl () ++
+        str "to" ++ fnl () ++
+        str "Proof using " ++ inferred_vars)
+
 let build_constant_declaration env result =
   let open Cooking in
   let typ = result.cook_type in
-  let check declared_set inferred_set =
-    if not (Id.Set.subset inferred_set declared_set) then
-      let l = Id.Set.elements (Id.Set.diff inferred_set declared_set) in
-      let n = List.length l in
-      let declared_vars = Pp.pr_sequence Id.print (Id.Set.elements declared_set) in
-      let inferred_vars = Pp.pr_sequence Id.print (Id.Set.elements inferred_set) in
-      let missing_vars  = Pp.pr_sequence Id.print (List.rev l) in
-      user_err Pp.(prlist str
-         ["The following section "; (String.plural n "variable"); " ";
-          (String.conjugate_verb_to_be n); " used but not declared:"] ++ fnl () ++
-         missing_vars ++ str "." ++ fnl () ++ fnl () ++
-         str "You can either update your proof to not depend on " ++ missing_vars ++
-         str ", or you can update your Proof line from" ++ fnl () ++
-         str "Proof using " ++ declared_vars ++ fnl () ++
-         str "to" ++ fnl () ++
-         str "Proof using " ++ inferred_vars) in
   (* 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
@@ -265,22 +236,10 @@ let build_constant_declaration env result =
         (* We use the declared set and chain a check of correctness *)
         declared,
         match def with
-        | Undef _ | Primitive _ as x -> x (* nothing to check *)
+        | Undef _ | Primitive _ | OpaqueDef _ as x -> x (* nothing to check *)
         | Def cs as x ->
-            let ids_typ = global_vars_set env typ in
-            let ids_def = global_vars_set env (Mod_subst.force_constr cs) in
-            let inferred = Environ.really_needed env (Id.Set.union ids_typ ids_def) in
-            check declared inferred;
-            x
-        | OpaqueDef lc -> (* In this case we can postpone the check *)
-          let iter k cu = Future.chain cu (fun (c, _ as p) -> k c; p) in
-          let kont c =
-            let ids_typ = global_vars_set env typ in
-            let ids_def = global_vars_set env c in
-            let inferred = Environ.really_needed env (Id.Set.union ids_typ ids_def) in
-            check declared inferred
-          in
-          OpaqueDef (iter kont lc)
+          let () = check_section_variables env declared typ (Mod_subst.force_constr cs) in
+          x
   in
   let univs = result.cook_universes in
   let hyps = List.filter (fun d -> Id.Set.mem (NamedDecl.get_id d) hyps) (Environ.named_context env) in
@@ -297,11 +256,46 @@ let build_constant_declaration env result =
     const_inline_code = result.cook_inline;
     const_typing_flags = Environ.typing_flags env }
 
+let check_delayed (type a) (handle : a effect_handler) tyenv (body : a proof_output) = match tyenv with
+| MonoTyCtx (env, tyj, univs, declared, feedback_id) ->
+  let ((body, uctx), side_eff) = body in
+  (* don't redeclare universes which are declared for the type *)
+  let uctx = Univ.ContextSet.diff uctx univs in
+  let (body, uctx', valid_signatures) = handle env body side_eff in
+  let uctx = Univ.ContextSet.union uctx uctx' in
+  let env = push_context_set uctx env in
+  let body,env,ectx = skip_trusted_seff valid_signatures body env in
+  let j = Typeops.infer env body in
+  let j = unzip ectx j in
+  let _ = Typeops.judge_of_cast env j DEFAULTcast tyj in
+  let c = j.uj_val in
+  let () = check_section_variables env declared tyj.utj_val body in
+  feedback_completion_typecheck feedback_id;
+  c, Opaqueproof.PrivateMonomorphic uctx
+| PolyTyCtx (env, tj, usubst, auctx, declared, feedback_id) ->
+  let ((body, ctx), side_eff) = body in
+  let body, ctx', _ = handle env body side_eff in
+  let ctx = 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 () = check_section_variables env declared tj.utj_val body in
+  let def = Vars.subst_univs_level_constr usubst j.uj_val in
+  let () = feedback_completion_typecheck feedback_id in
+  def, Opaqueproof.PrivatePolymorphic (Univ.AUContext.size auctx, private_univs)
+
 (*s Global and local constant declaration. *)
 
-let translate_constant mb env _kn ce =
+let translate_constant env _kn ce =
   build_constant_declaration env
-    (infer_declaration ~trust:mb env ce)
+    (infer_declaration env ce)
+
+let translate_opaque env _kn ce =
+  let def, ctx = infer_opaque env ce in
+  build_constant_declaration env def, ctx
 
 let translate_local_assum env t =
   let j = Typeops.infer env t in
@@ -336,7 +330,7 @@ let translate_local_def env _id centry =
     const_entry_universes = Monomorphic_entry Univ.ContextSet.empty;
     const_entry_inline_code = false;
   } in
-  let decl = infer_declaration ~trust:Pure env (DefinitionEntry centry) in
+  let decl = infer_declaration env (DefinitionEntry centry) in
   let typ = decl.cook_type in
   let () = match decl.cook_universes with
   | Monomorphic ctx -> assert (Univ.ContextSet.is_empty ctx)
diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli
index ef01ece185..c9f6d66e36 100644
--- a/kernel/term_typing.mli
+++ b/kernel/term_typing.mli
@@ -22,9 +22,7 @@ open Entries
 type 'a effect_handler =
   env -> Constr.t -> 'a -> (Constr.t * Univ.ContextSet.t * int)
 
-type _ trust =
-| Pure : unit trust
-| SideEffects : 'a effect_handler -> 'a Entries.seff_wrap trust
+type typing_context
 
 val translate_local_def : env -> Id.t -> section_def_entry ->
   constr * Sorts.relevance * types
@@ -32,15 +30,21 @@ val translate_local_def : env -> Id.t -> section_def_entry ->
 val translate_local_assum : env -> types -> types * Sorts.relevance
 
 val translate_constant :
-  'a trust -> env -> Constant.t -> 'a constant_entry ->
-    Opaqueproof.proofterm constant_body
+  env -> Constant.t -> constant_entry ->
+    'a constant_body
+
+val translate_opaque :
+  env -> Constant.t -> 'a opaque_entry ->
+    unit constant_body * typing_context
 
 val translate_recipe : env -> Constant.t -> Cooking.recipe -> Opaqueproof.opaque constant_body
 
+val check_delayed : 'a effect_handler -> typing_context -> 'a proof_output -> (Constr.t * Univ.ContextSet.t Opaqueproof.delayed_universes)
+
 (** Internal functions, mentioned here for debug purpose only *)
 
-val infer_declaration : trust:'a trust -> env ->
-  'a constant_entry -> Opaqueproof.proofterm Cooking.result
+val infer_declaration : env ->
+  constant_entry -> typing_context Cooking.result
 
 val build_constant_declaration :
   env -> Opaqueproof.proofterm Cooking.result -> Opaqueproof.proofterm constant_body