Merge PR #10174: Further cleanup of the side-effect machinery

Reviewed-by: SkySkimmer
Reviewed-by: gares
Reviewed-by: maximedenes

29 files changed, 206 insertions, 212 deletions

diff --git a/interp/declare.ml b/interp/declare.ml
index 76b4bab2ce..7ee7ecb5e8 100644
--- a/interp/declare.ml
+++ b/interp/declare.ml
@@ -36,9 +36,8 @@ type internal_flag =
 (** Declaration of constants and parameters *)
 
 type constant_obj = {
-  cst_decl : global_declaration option;
-  (** [None] when the declaration is a side-effect and has already been defined
-      in the global environment. *)
+  cst_decl : Cooking.recipe option;
+  (** Non-empty only when rebuilding a constant after a section *)
   cst_kind : logical_kind;
   cst_locl : bool;
 }
@@ -65,21 +64,21 @@ let open_constant i ((sp,kn), obj) =
 let exists_name id =
   variable_exists id || Global.exists_objlabel (Label.of_id id)
 
-let check_exists sp =
-  let id = basename sp in
+let check_exists id =
   if exists_name id then alreadydeclared (Id.print id ++ str " already exists")
 
 let cache_constant ((sp,kn), obj) =
+  (* Invariant: the constant must exist in the logical environment, except when
+     redefining it when exiting a section. See [discharge_constant]. *)
   let id = basename sp in
   let kn' =
     match obj.cst_decl with
     | None ->
       if Global.exists_objlabel (Label.of_id (basename sp))
       then Constant.make1 kn
-      else CErrors.anomaly Pp.(str"Ex seff not found: " ++ Id.print(basename sp) ++ str".")
-    | Some decl ->
-      let () = check_exists sp in
-      Global.add_constant ~in_section:(Lib.sections_are_opened ()) id decl
+      else CErrors.anomaly Pp.(str"Missing constant " ++ Id.print(basename sp) ++ str".")
+    | Some r ->
+      Global.add_recipe ~in_section:(Lib.sections_are_opened ()) id r
   in
   assert (Constant.equal kn' (Constant.make1 kn));
   Nametab.push (Nametab.Until 1) sp (ConstRef (Constant.make1 kn));
@@ -93,7 +92,9 @@ let discharge_constant ((sp, kn), obj) =
   let modlist = replacement_context () in
   let { abstr_ctx = hyps; abstr_subst = subst; abstr_uctx = uctx } = section_segment_of_constant con in
   let abstract = (named_of_variable_context hyps, subst, uctx) in
-  let new_decl = GlobalRecipe{ from; info = { Opaqueproof.modlist; abstract}} in
+  let new_decl = { from; info = { Opaqueproof.modlist; abstract } } in
+  (* This is a hack: when leaving a section, we lose the constant definition, so
+     we have to store it in the libobject to be able to retrieve it after. *)
   Some { obj with cst_decl = Some new_decl; }
 
 (* Hack to reduce the size of .vo: we keep only what load/open needs *)
@@ -121,27 +122,22 @@ let update_tables c =
   declare_constant_implicits c;
   Notation.declare_ref_arguments_scope Evd.empty (ConstRef c)
 
-let register_side_effect (c, role) =
+let register_constant kn kind local =
   let o = inConstant {
     cst_decl = None;
-    cst_kind = IsProof Theorem;
-    cst_locl = false;
+    cst_kind = kind;
+    cst_locl = local;
   } in
-  let id = Label.to_id (Constant.label c) in
-  ignore(add_leaf id o);
-  update_tables c;
+  let id = Label.to_id (Constant.label kn) in
+  let _ = add_leaf id o in
+  update_tables kn
+
+let register_side_effect (c, role) =
+  let () = register_constant c (IsProof Theorem) false in
   match role with
   | Subproof -> ()
   | Schema (ind, kind) -> !declare_scheme kind [|ind,c|]
 
-let declare_constant_common id cst =
-  let o = inConstant cst in
-  let _, kn as oname = add_leaf id o in
-  pull_to_head oname;
-  let c = Global.constant_of_delta_kn kn in
-  update_tables c;
-  c
-
 let default_univ_entry = Monomorphic_entry Univ.ContextSet.empty
 let definition_entry ?fix_exn ?(opaque=false) ?(inline=false) ?types
     ?(univs=default_univ_entry) ?(eff=Safe_typing.empty_private_constants) body =
@@ -153,7 +149,8 @@ let definition_entry ?fix_exn ?(opaque=false) ?(inline=false) ?types
     const_entry_feedback = None;
     const_entry_inline_code = inline}
 
-let declare_constant ?(internal = UserIndividualRequest) ?(local = false) id ?(export_seff=false) (cd, kind) =
+let define_constant ?role ?(export_seff=false) id cd =
+  (* Logically define the constant and its subproofs, no libobject tampering *)
   let is_poly de = match de.const_entry_universes with
   | Monomorphic_entry _ -> false
   | Polymorphic_entry _ -> true
@@ -165,20 +162,27 @@ let declare_constant ?(internal = UserIndividualRequest) ?(local = false) id ?(e
         export_seff ||
         not de.const_entry_opaque ||
         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. *)
+      (* This globally defines the side-effects in the environment. *)
       let de, export = Global.export_private_constants ~in_section de in
       export, ConstantEntry (PureEntry, DefinitionEntry de)
     | _ -> [], ConstantEntry (EffectEntry, cd)
   in
+  let kn, eff = Global.add_constant ?role ~in_section id decl in
+  kn, eff, export
+
+let declare_constant ?(internal = UserIndividualRequest) ?(local = false) id ?(export_seff=false) (cd, kind) =
+  let () = check_exists id in
+  let kn, _eff, export = define_constant ~export_seff id cd in
+  (* Register the libobjects attached to the constants and its subproofs *)
   let () = List.iter register_side_effect export in
-  let cst = {
-    cst_decl = Some decl;
-    cst_kind = kind;
-    cst_locl = local;
-  } in
-  declare_constant_common id cst
+  let () = register_constant kn kind local in
+  kn
+
+let declare_private_constant ~role ?(internal=UserIndividualRequest) ?(local = false) id (cd, kind) =
+  let kn, eff, export = define_constant ~role id cd in
+  let () = assert (List.is_empty export) in
+  let () = register_constant kn kind local in
+  kn, eff
 
 let declare_definition ?(internal=UserIndividualRequest)
   ?(opaque=false) ?(kind=Decl_kinds.Definition) ?(local = false)
@@ -297,7 +301,7 @@ let open_inductive i ((sp,kn),mie) =
 
 let cache_inductive ((sp,kn),mie) =
   let names = inductive_names sp kn mie in
-  List.iter check_exists (List.map fst names);
+  List.iter check_exists (List.map (fun p -> basename (fst p)) names);
   let id = basename sp in
   let kn' = Global.add_mind id mie in
   assert (MutInd.equal kn' (MutInd.make1 kn));
diff --git a/interp/declare.mli b/interp/declare.mli
index 8f1e73c88c..2ffde31fc0 100644
--- a/interp/declare.mli
+++ b/interp/declare.mli
@@ -55,6 +55,9 @@ val definition_entry : ?fix_exn:Future.fix_exn ->
 val declare_constant :
  ?internal:internal_flag -> ?local:bool -> Id.t -> ?export_seff:bool -> constant_declaration -> Constant.t
 
+val declare_private_constant :
+  role:side_effect_role -> ?internal:internal_flag -> ?local:bool -> Id.t -> constant_declaration -> Constant.t * Safe_typing.private_constants
+
 val declare_definition : 
   ?internal:internal_flag -> ?opaque:bool -> ?kind:definition_object_kind ->
   ?local:bool -> Id.t -> ?types:constr ->
diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml
index 412637c4b6..95f88c0306 100644
--- a/kernel/cClosure.ml
+++ b/kernel/cClosure.ml
@@ -389,7 +389,7 @@ type clos_infos = {
   i_flags : reds;
   i_cache : infos_cache }
 
-type clos_tab = fconstr constant_def KeyTable.t
+type clos_tab = (fconstr, Empty.t) constant_def KeyTable.t
 
 let info_flags info = info.i_flags
 let info_env info = info.i_cache.i_env
diff --git a/kernel/cClosure.mli b/kernel/cClosure.mli
index b1b69dded8..1a790eaed6 100644
--- a/kernel/cClosure.mli
+++ b/kernel/cClosure.mli
@@ -215,7 +215,7 @@ val eta_expand_ind_stack : env -> inductive -> fconstr -> stack ->
 (** Conversion auxiliary functions to do step by step normalisation *)
 
 (** [unfold_reference] unfolds references in a [fconstr] *)
-val unfold_reference : clos_infos -> clos_tab -> table_key -> fconstr constant_def
+val unfold_reference : clos_infos -> clos_tab -> table_key -> (fconstr, Util.Empty.t) constant_def
 
 (***********************************************************************
   i This is for lazy debug *)
diff --git a/kernel/cbytegen.mli b/kernel/cbytegen.mli
index 6a9550342c..bdaf5fe422 100644
--- a/kernel/cbytegen.mli
+++ b/kernel/cbytegen.mli
@@ -20,7 +20,7 @@ val compile : fail_on_error:bool ->
 (** init, fun, fv *)
 
 val compile_constant_body : fail_on_error:bool ->
-  env -> universes -> Constr.t Mod_subst.substituted constant_def ->
+  env -> universes -> (Constr.t Mod_subst.substituted, 'opaque) constant_def ->
   body_code option
 
 (** Shortcut of the previous function used during module strengthening *)
diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index 9b974c4ecc..9b6e37251f 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -152,11 +152,11 @@ let abstract_constant_body c (hyps, subst) =
   let c = Vars.subst_vars subst c in
   it_mkLambda_or_LetIn c hyps
 
-type recipe = { from : constant_body; info : Opaqueproof.cooking_info }
+type recipe = { from : Opaqueproof.opaque constant_body; info : Opaqueproof.cooking_info }
 type inline = bool
 
-type result = {
-  cook_body : constr Mod_subst.substituted constant_def;
+type 'opaque result = {
+  cook_body : (constr Mod_subst.substituted, 'opaque) constant_def;
   cook_type : types;
   cook_universes : universes;
   cook_private_univs : Univ.ContextSet.t option;
diff --git a/kernel/cooking.mli b/kernel/cooking.mli
index b0f143c47d..b022e2ac09 100644
--- a/kernel/cooking.mli
+++ b/kernel/cooking.mli
@@ -13,12 +13,12 @@ open Declarations
 
 (** {6 Cooking the constants. } *)
 
-type recipe = { from : constant_body; info : Opaqueproof.cooking_info }
+type recipe = { from : Opaqueproof.opaque constant_body; info : Opaqueproof.cooking_info }
 
 type inline = bool
 
-type result = {
-  cook_body : constr Mod_subst.substituted constant_def;
+type 'opaque result = {
+  cook_body : (constr Mod_subst.substituted, 'opaque) constant_def;
   cook_type : types;
   cook_universes : universes;
   cook_private_univs : Univ.ContextSet.t option;
@@ -27,7 +27,7 @@ type result = {
   cook_context : Constr.named_context option;
 }
 
-val cook_constant : hcons:bool -> recipe -> result
+val cook_constant : hcons:bool -> recipe -> Opaqueproof.opaque result
 val cook_constr : Opaqueproof.cooking_info -> constr -> constr
 
 (** {6 Utility functions used in module [Discharge]. } *)
diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index 5551742c02..36ee952099 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -47,10 +47,10 @@ type inline = int option
     transparent body, or an opaque one *)
 
 (* Global declarations (i.e. constants) can be either: *)
-type 'a constant_def =
+type ('a, 'opaque) constant_def =
   | Undef of inline                       (** a global assumption *)
   | Def of 'a                             (** or a transparent global definition *)
-  | OpaqueDef of Opaqueproof.opaque       (** or an opaque global definition *)
+  | OpaqueDef of 'opaque                  (** or an opaque global definition *)
   | Primitive of CPrimitives.t            (** or a primitive operation *)
 
 type universes =
@@ -87,9 +87,9 @@ type typing_flags = {
 
 (* some contraints are in constant_constraints, some other may be in
  * the OpaqueDef *)
-type constant_body = {
+type 'opaque constant_body = {
     const_hyps : Constr.named_context; (** New: younger hyp at top *)
-    const_body : Constr.t Mod_subst.substituted constant_def;
+    const_body : (Constr.t Mod_subst.substituted, 'opaque) constant_def;
     const_type : types;
     const_relevance : Sorts.relevance;
     const_body_code : Cemitcodes.to_patch_substituted option;
@@ -246,7 +246,7 @@ type module_alg_expr =
 (** A component of a module structure *)
 
 type structure_field_body =
-  | SFBconst of constant_body
+  | SFBconst of Opaqueproof.opaque constant_body
   | SFBmind of mutual_inductive_body
   | SFBmodule of module_body
   | SFBmodtype of module_type_body
diff --git a/kernel/declareops.mli b/kernel/declareops.mli
index 54a853fc81..fb02c6a029 100644
--- a/kernel/declareops.mli
+++ b/kernel/declareops.mli
@@ -26,21 +26,21 @@ val map_decl_arity : ('a -> 'c) -> ('b -> 'd) ->
 
 (** {6 Constants} *)
 
-val subst_const_body : substitution -> constant_body -> constant_body
+val subst_const_body : substitution -> Opaqueproof.opaque constant_body -> Opaqueproof.opaque constant_body
 
 (** Is there a actual body in const_body ? *)
 
-val constant_has_body : constant_body -> bool
+val constant_has_body : 'a constant_body -> bool
 
-val constant_polymorphic_context : constant_body -> AUContext.t
+val constant_polymorphic_context : 'a constant_body -> AUContext.t
 
 (** Is the constant polymorphic? *)
-val constant_is_polymorphic : constant_body -> bool
+val constant_is_polymorphic : 'a constant_body -> bool
 
 (** Return the universe context, in case the definition is polymorphic, otherwise
     the context is empty. *)
 
-val is_opaque : constant_body -> bool
+val is_opaque : 'a constant_body -> bool
 
 (** {6 Inductive types} *)
 
@@ -83,7 +83,7 @@ val safe_flags : Conv_oracle.oracle -> typing_flags
     of the structure, but simply hash-cons all inner constr
     and other known elements *)
 
-val hcons_const_body : constant_body -> constant_body
+val hcons_const_body : 'a constant_body -> 'a constant_body
 val hcons_mind : mutual_inductive_body -> mutual_inductive_body
 val hcons_module_body : module_body -> module_body
 val hcons_module_type : module_type_body -> module_type_body
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 617519a038..05f342a82a 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -46,7 +46,7 @@ type link_info =
   | LinkedInteractive of string
   | NotLinked
 
-type constant_key = constant_body * (link_info ref * key)
+type constant_key = Opaqueproof.opaque constant_body * (link_info ref * key)
 
 type mind_key = mutual_inductive_body * link_info ref
 
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 4e6dbbe206..f6cd41861e 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -42,7 +42,7 @@ type link_info =
 
 type key = int CEphemeron.key option ref
 
-type constant_key = constant_body * (link_info ref * key)
+type constant_key = Opaqueproof.opaque constant_body * (link_info ref * key)
 
 type mind_key = mutual_inductive_body * link_info ref
 
@@ -174,19 +174,19 @@ val reset_with_named_context : named_context_val -> env -> env
 val pop_rel_context : int -> env -> env
 
 (** Useful for printing *)
-val fold_constants : (Constant.t -> constant_body -> 'a -> 'a) -> env -> 'a -> 'a
+val fold_constants : (Constant.t -> Opaqueproof.opaque constant_body -> 'a -> 'a) -> env -> 'a -> 'a
 
 (** {5 Global constants }
   {6 Add entries to global environment } *)
 
-val add_constant : Constant.t -> constant_body -> env -> env
-val add_constant_key : Constant.t -> constant_body -> link_info ->
+val add_constant : Constant.t -> Opaqueproof.opaque constant_body -> env -> env
+val add_constant_key : Constant.t -> Opaqueproof.opaque constant_body -> link_info ->
   env -> env
 val lookup_constant_key :  Constant.t -> env -> constant_key
 
 (** Looks up in the context of global constant names 
    raises [Not_found] if the required path is not found *)
-val lookup_constant    : Constant.t -> env -> constant_body
+val lookup_constant    : Constant.t -> env -> Opaqueproof.opaque constant_body
 val evaluable_constant : Constant.t -> env -> bool
 
 (** New-style polymorphism *)
@@ -219,7 +219,7 @@ val constant_context : env -> Constant.t -> Univ.AUContext.t
     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 -> constant_body -> (Constr.constr * Univ.AUContext.t) option
+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 
diff --git a/kernel/nativecode.mli b/kernel/nativecode.mli
index 96efa7faa5..b5c03b6ca3 100644
--- a/kernel/nativecode.mli
+++ b/kernel/nativecode.mli
@@ -65,7 +65,7 @@ val empty_updates : code_location_updates
 val register_native_file : string -> unit
 
 val compile_constant_field : env -> string -> Constant.t ->
-  global list -> constant_body -> global list
+  global list -> 'a constant_body -> global list
 
 val compile_mind_field : ModPath.t -> Label.t ->
   global list -> mutual_inductive_body -> global list
diff --git a/kernel/opaqueproof.ml b/kernel/opaqueproof.ml
index 57059300b8..18c1bcc0f8 100644
--- a/kernel/opaqueproof.ml
+++ b/kernel/opaqueproof.ml
@@ -77,11 +77,6 @@ let subst_opaque sub = function
   | Indirect (s,dp,i) -> Indirect (sub::s,dp,i)
   | Direct _ -> CErrors.anomaly (Pp.str "Substituting a Direct opaque.")
 
-let iter_direct_opaque f = function
-  | Indirect _ -> CErrors.anomaly (Pp.str "Not a direct opaque.")
-  | Direct (d,cu) ->
-      Direct (d,Future.chain cu (fun (c, u) -> f c; c, u))
-
 let discharge_direct_opaque ~cook_constr ci = function
   | Indirect _ -> CErrors.anomaly (Pp.str "Not a direct opaque.")
   | Direct (d,cu) ->
diff --git a/kernel/opaqueproof.mli b/kernel/opaqueproof.mli
index d47c0bbb3c..4e8956af06 100644
--- a/kernel/opaqueproof.mli
+++ b/kernel/opaqueproof.mli
@@ -43,7 +43,6 @@ val get_constraints :
   opaquetab -> opaque -> Univ.ContextSet.t Future.computation option
 
 val subst_opaque : substitution -> opaque -> opaque
-val iter_direct_opaque : (constr -> unit) -> opaque -> opaque
 
 type work_list = (Univ.Instance.t * Id.t array) Cmap.t * 
   (Univ.Instance.t * Id.t array) Mindmap.t
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 75375812c0..a5d8a480ee 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -228,27 +228,10 @@ let check_engagement env expected_impredicative_set =
 
 (** {6 Stm machinery } *)
 
-type seff_env =
-  [ `Nothing
-  (* The proof term and its universes.
-     Same as the constant_body's but not in an ephemeron *)
-  | `Opaque of Constr.t * Univ.ContextSet.t ]
-
-let get_opaque_body env cbo =
-  match cbo.const_body with
-  | Undef _ -> assert false
-  | Primitive _ -> assert false
-  | Def _ -> `Nothing
-  | OpaqueDef opaque ->
-      `Opaque
-        (Opaqueproof.force_proof (Environ.opaque_tables env) opaque,
-         Opaqueproof.force_constraints (Environ.opaque_tables env) opaque)
-
 type side_effect = {
   from_env : Declarations.structure_body CEphemeron.key;
   seff_constant : Constant.t;
-  seff_body : Declarations.constant_body;
-  seff_env : seff_env;
+  seff_body : (Constr.t * Univ.ContextSet.t) Declarations.constant_body;
   seff_role : Entries.side_effect_role;
 }
 
@@ -288,39 +271,38 @@ type private_constants = SideEffects.t
 let side_effects_of_private_constants l =
   List.rev (SideEffects.repr l)
 
+(* Only used to push in an Environ.env. *)
+let lift_constant c =
+  let body = match c.const_body with
+  | OpaqueDef _ -> Undef None
+  | Def _ | Undef _ | Primitive _ as body -> body
+  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 =
     try ignore(Environ.lookup_constant eff.seff_constant env); env
-    with Not_found -> Environ.add_constant eff.seff_constant eff.seff_body env
+    with Not_found -> Environ.add_constant eff.seff_constant (lift_constant eff.seff_body) env
   in
   List.fold_left add_if_undefined env eff
 
 let empty_private_constants = SideEffects.empty
 let concat_private = SideEffects.concat
 
-let private_constant env role cst =
-  (** The constant must be the last entry of the safe environment *)
-  let () = match env.revstruct with
-  | (lbl, SFBconst _) :: _ -> assert (Label.equal lbl (Constant.label cst))
-  | _ -> assert false
-  in
-  let from_env = CEphemeron.create env.revstruct in
-  let cbo = Environ.lookup_constant cst env.env in
-  let eff = {
-    from_env = from_env;
-    seff_constant = cst;
-    seff_body = cbo;
-    seff_env = get_opaque_body env.env cbo;
-    seff_role = role;
-  } in
-  SideEffects.add eff empty_private_constants
-
 let universes_of_private eff =
   let fold acc eff =
-    let acc = match eff.seff_env with
-    | `Nothing -> acc
-    | `Opaque (_, ctx) -> ctx :: acc
+    let acc = match eff.seff_body.const_body with
+    | Def _ -> acc
+    | OpaqueDef (_, ctx) -> ctx :: acc
+    | Primitive _ | Undef _ -> assert false
     in
     match eff.seff_body.const_universes with
     | Monomorphic ctx -> ctx :: acc
@@ -565,7 +547,6 @@ type 'a effect_entry =
 
 type global_declaration =
   | ConstantEntry : 'a effect_entry * 'a Entries.constant_entry -> global_declaration
-  | GlobalRecipe of Cooking.recipe
 
 type exported_private_constant = 
   Constant.t * Entries.side_effect_role
@@ -598,7 +579,7 @@ let inline_side_effects env body side_eff =
   let open Constr in
   (** First step: remove the constants that are still in the environment *)
   let filter e =
-    let cb = (e.seff_constant, e.seff_body, e.seff_env) in
+    let cb = (e.seff_constant, e.seff_body) in
     try ignore (Environ.lookup_constant e.seff_constant env); None
     with Not_found -> Some (cb, e.from_env)
   in
@@ -612,10 +593,10 @@ let inline_side_effects env body side_eff =
   else
     (** Second step: compute the lifts and substitutions to apply *)
     let cname c r = Context.make_annot (Name (Label.to_id (Constant.label c))) r in
-    let fold (subst, var, ctx, args) (c, cb, b) =
-      let (b, opaque) = match cb.const_body, b with
-      | Def b, _ -> (Mod_subst.force_constr b, false)
-      | OpaqueDef _, `Opaque (b,_) -> (b, true)
+    let fold (subst, var, ctx, args) (c, cb) =
+      let (b, opaque) = match cb.const_body with
+      | Def b -> (Mod_subst.force_constr b, false)
+      | OpaqueDef (b, _) -> (b, true)
       | _ -> assert false
       in
       match cb.const_universes with
@@ -701,7 +682,8 @@ let check_signatures curmb sl =
   | Some (n, _) -> n
 
 
-let constant_entry_of_side_effect cb u =
+let constant_entry_of_side_effect eff =
+  let cb = eff.seff_body in
   let open Entries in
   let univs =
     match cb.const_universes with
@@ -711,9 +693,9 @@ let constant_entry_of_side_effect cb u =
       Polymorphic_entry (Univ.AUContext.names auctx, Univ.AUContext.repr auctx)
   in
   let pt =
-    match cb.const_body, u with
-    | OpaqueDef _, `Opaque (b, c) -> b, c
-    | Def b, `Nothing -> Mod_subst.force_constr b, Univ.ContextSet.empty
+    match cb.const_body with
+    | OpaqueDef (b, c) -> b, c
+    | Def b -> Mod_subst.force_constr b, Univ.ContextSet.empty
     | _ -> assert false in
   DefinitionEntry {
     const_entry_body = Future.from_val (pt, ());
@@ -724,18 +706,6 @@ let constant_entry_of_side_effect cb u =
     const_entry_opaque = Declareops.is_opaque cb;
     const_entry_inline_code = cb.const_inline_code }
 
-let turn_direct orig =
-  let cb = orig.seff_body in
-  if Declareops.is_opaque cb then
-    let p = match orig.seff_env with
-    | `Opaque (b, c) -> (b, c)
-    | _ -> assert false
-    in
-    let const_body = OpaqueDef (Opaqueproof.create (Future.from_val p)) in
-    let cb = { cb with const_body } in
-    { orig with seff_body = cb }
-  else orig
-
 let export_eff eff =
   (eff.seff_constant, eff.seff_body, eff.seff_role)
 
@@ -756,13 +726,14 @@ let export_side_effects mb env c =
       let trusted = check_signatures mb signatures in
       let push_seff env eff =
         let { seff_constant = kn; seff_body = cb ; _ } = eff in
-        let env = Environ.add_constant kn cb env in
+        let env = Environ.add_constant kn (lift_constant cb) env in
         match cb.const_universes with
         | Polymorphic _ -> env
         | Monomorphic ctx ->
-          let ctx = match eff.seff_env with
-          | `Nothing -> ctx
-          | `Opaque(_, ctx') -> Univ.ContextSet.union ctx' ctx
+          let ctx = match eff.seff_body.const_body with
+          | Def _ -> ctx
+          | OpaqueDef (_, ctx') -> Univ.ContextSet.union ctx' ctx
+          | Undef _ | Primitive _ -> assert false
           in
           Environ.push_context_set ~strict:true ctx env
       in
@@ -771,35 +742,39 @@ let export_side_effects mb env c =
         | [] -> List.rev acc, ce
         | eff :: rest ->
           if Int.equal sl 0 then
-           let env, cb =
-              let { seff_constant = kn; seff_body = ocb; seff_env = u ; _ } = eff in
-               let ce = constant_entry_of_side_effect ocb u in
+            let env, cb =
+              let kn = eff.seff_constant in
+               let ce = constant_entry_of_side_effect eff in
                let cb = Term_typing.translate_constant Term_typing.Pure env kn ce in
-               let eff = { eff with
-                seff_body = cb;
-                seff_env = `Nothing;
-               } in
+               let cb = map_constant Future.force cb in
+               let eff = { eff with seff_body = cb } in
                (push_seff env eff, export_eff eff)
             in
             translate_seff 0 rest (cb :: acc) env
           else
-           let cb = turn_direct eff in
-           let env = push_seff env cb in
-           let ecb = export_eff cb in
+           let env = push_seff env eff in
+           let ecb = export_eff eff in
            translate_seff (sl - 1) rest (ecb :: acc) env
      in
        translate_seff trusted seff [] env
 
 let export_private_constants ~in_section ce senv =
   let exported, ce = export_side_effects senv.revstruct senv.env ce in
-  let bodies = List.map (fun (kn, cb, _) -> (kn, cb)) exported in
+  let map (kn, cb, _) = (kn, map_constant (fun p -> Opaqueproof.create (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
   (ce, exported), senv
 
-let add_constant ~in_section l decl 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 senv = add_constant_aux ~in_section senv (kn, cb) in
+  kn, senv
+
+let add_constant ?role ~in_section l decl senv =
   let kn = Constant.make2 senv.modpath l in
-  let senv =
     let cb = 
       match decl with
       | ConstantEntry (EffectEntry, ce) ->
@@ -811,9 +786,9 @@ let add_constant ~in_section l decl senv =
         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
-      | GlobalRecipe r ->
-        let cb = Term_typing.translate_recipe ~hcons:(not in_section) senv.env kn r in
-        if in_section then cb else Declareops.hcons_const_body cb in
+    in
+  let senv =
+    let cb = map_constant Opaqueproof.create cb in
     add_constant_aux ~in_section senv (kn, cb) in
   let senv =
     match decl with
@@ -822,7 +797,20 @@ let add_constant ~in_section l decl senv =
       add_retroknowledge (Retroknowledge.Register_type(t,kn)) senv
     | _ -> senv
   in
-  kn, senv
+  let eff = match role with
+  | None -> empty_private_constants
+  | Some role ->
+    let cb = map_constant Future.force cb in
+    let from_env = CEphemeron.create senv.revstruct in
+    let eff = {
+      from_env = from_env;
+      seff_constant = kn;
+      seff_body = cb;
+      seff_role = role;
+    } in
+    SideEffects.add eff empty_private_constants
+  in
+  (kn, eff), senv
 
 (** Insertion of inductive types *)
 
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index d6c7022cf5..36ca3d8c47 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -48,9 +48,6 @@ val concat_private : private_constants -> private_constants -> private_constants
 (** [concat_private e1 e2] adds the constants of [e1] to [e2], i.e. constants in
     [e1] must be more recent than those of [e2]. *)
 
-val private_constant : safe_environment -> Entries.side_effect_role -> Constant.t -> private_constants
-(** Constant must be the last definition of the safe_environment. *)
-
 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
@@ -91,7 +88,6 @@ type 'a effect_entry =
 
 type global_declaration =
   | ConstantEntry : 'a effect_entry * 'a Entries.constant_entry -> global_declaration
-  | GlobalRecipe of Cooking.recipe
 
 type exported_private_constant = 
   Constant.t * Entries.side_effect_role
@@ -103,8 +99,11 @@ val export_private_constants : in_section:bool ->
 (** returns the main constant plus a list of auxiliary constants (empty
     unless one requires the side effects to be exported) *)
 val add_constant :
-  in_section:bool -> Label.t -> global_declaration ->
-    Constant.t safe_transformer
+  ?role:Entries.side_effect_role -> in_section:bool -> Label.t -> global_declaration ->
+    (Constant.t * private_constants) safe_transformer
+
+val add_recipe :
+  in_section:bool -> Label.t -> Cooking.recipe -> Constant.t safe_transformer
 
 (** Adding an inductive type *)
 
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index 1857ea3329..24845ce459 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -31,7 +31,7 @@ open Mod_subst
    an inductive type. It can also be useful to allow reorderings in
    inductive types *)
 type namedobject =
-  | Constant of constant_body
+  | Constant of Opaqueproof.opaque constant_body
   | IndType of inductive * mutual_inductive_body
   | IndConstr of constructor * mutual_inductive_body
 
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index faa4411e92..74c6189a65 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -154,7 +154,7 @@ the polymorphic case
           let c = Constr.hcons j.uj_val in
           feedback_completion_typecheck feedback_id;
           c, uctx) in
-      let def = OpaqueDef (Opaqueproof.create proofterm) in
+      let def = OpaqueDef proofterm in
       {
         Cooking.cook_body = def;
         cook_type = tyj.utj_val;
@@ -207,7 +207,7 @@ the polymorphic case
       in
       let def = Constr.hcons (Vars.subst_univs_level_constr usubst j.uj_val) in
       let def = 
-	if opaque then OpaqueDef (Opaqueproof.create (Future.from_val (def, Univ.ContextSet.empty)))
+        if opaque then OpaqueDef (Future.from_val (def, Univ.ContextSet.empty))
 	else Def (Mod_subst.from_val def) 
       in
 	feedback_completion_typecheck feedback_id;
@@ -232,7 +232,7 @@ let record_aux env s_ty s_bo =
         (keep_hyps env s_bo)) in
   Aux_file.record_in_aux "context_used" v
 
-let build_constant_declaration _kn env result =
+let build_constant_declaration env result =
   let open Cooking in
   let typ = result.cook_type in
   let check declared inferred =
@@ -271,11 +271,8 @@ let build_constant_declaration _kn env result =
         | Undef _ | Primitive _ -> Id.Set.empty
         | Def cs -> global_vars_set env (Mod_subst.force_constr cs)
         | OpaqueDef lc ->
-            let vars =
-              global_vars_set env
-                (Opaqueproof.force_proof (opaque_tables env) lc) in
-            (* we force so that cst are added to the env immediately after *)
-            ignore(Opaqueproof.force_constraints (opaque_tables env) lc);
+            let (lc, _) = Future.force lc in
+            let vars = global_vars_set env lc in
             if !Flags.record_aux_file then record_aux env ids_typ vars;
             vars
         in
@@ -296,11 +293,15 @@ let build_constant_declaration _kn env result =
             check declared inferred;
             x
         | OpaqueDef lc -> (* In this case we can postpone the check *)
-            OpaqueDef (Opaqueproof.iter_direct_opaque (fun c ->
-              let ids_typ = global_vars_set env typ in
-              let ids_def = global_vars_set env c in
-              let inferred = keep_hyps env (Id.Set.union ids_typ ids_def) in
-              check declared inferred) lc) in
+          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 = keep_hyps env (Id.Set.union ids_typ ids_def) in
+            check declared inferred
+          in
+          OpaqueDef (iter kont lc)
+  in
   let univs = result.cook_universes in
   let tps = 
     let res = Cbytegen.compile_constant_body ~fail_on_error:false env univs def in
@@ -318,8 +319,8 @@ let build_constant_declaration _kn env result =
 
 (*s Global and local constant declaration. *)
 
-let translate_constant mb env kn ce =
-  build_constant_declaration kn env
+let translate_constant mb env _kn ce =
+  build_constant_declaration env
     (infer_declaration ~trust:mb env ce)
 
 let translate_local_assum env t =
@@ -327,8 +328,21 @@ 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 =
-  build_constant_declaration kn env (Cooking.cook_constant ~hcons r)
+let translate_recipe ~hcons env _kn r =
+  let open Cooking in
+  let result = Cooking.cook_constant ~hcons 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
+  { const_hyps = Option.get result.cook_context;
+    const_body = result.cook_body;
+    const_type = result.cook_type;
+    const_body_code = tps;
+    const_universes = univs;
+    const_private_poly_univs = result.cook_private_univs;
+    const_relevance = result.cook_relevance;
+    const_inline_code = result.cook_inline;
+    const_typing_flags = Environ.typing_flags env }
 
 let translate_local_def env _id centry =
   let open Cooking in
@@ -351,8 +365,7 @@ let translate_local_def env _id centry =
     | Def _ -> ()
     | OpaqueDef lc ->
        let ids_typ = global_vars_set env typ in
-       let ids_def = global_vars_set env
-         (Opaqueproof.force_proof (opaque_tables env) lc) in
+       let ids_def = global_vars_set env (fst (Future.force lc)) in
        record_aux env ids_typ ids_def
   end;
   let () = match decl.cook_universes with
@@ -362,8 +375,7 @@ let translate_local_def env _id centry =
   let c = match decl.cook_body with
   | Def c -> Mod_subst.force_constr c
   | OpaqueDef o ->
-    let p = Opaqueproof.force_proof (Environ.opaque_tables env) o in
-    let cst = Opaqueproof.force_constraints (Environ.opaque_tables env) o in
+    let (p, cst) = Future.force o in
     (** Let definitions are ensured to have no extra constraints coming from
         the body by virtue of the typing of [Entries.section_def_entry]. *)
     let () = assert (Univ.ContextSet.is_empty cst) in
diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli
index 1fa5eca2e3..592a97e132 100644
--- a/kernel/term_typing.mli
+++ b/kernel/term_typing.mli
@@ -33,14 +33,14 @@ val translate_local_assum : env -> types -> types * Sorts.relevance
 
 val translate_constant :
   'a trust -> env -> Constant.t -> 'a constant_entry ->
-    constant_body
+    Opaqueproof.proofterm constant_body
 
-val translate_recipe : hcons:bool -> env -> Constant.t -> Cooking.recipe -> constant_body
+val translate_recipe : hcons:bool -> env -> Constant.t -> Cooking.recipe -> Opaqueproof.opaque constant_body
 
 (** Internal functions, mentioned here for debug purpose only *)
 
 val infer_declaration : trust:'a trust -> env ->
-  'a constant_entry -> Cooking.result
+  'a constant_entry -> Opaqueproof.proofterm Cooking.result
 
 val build_constant_declaration :
-  Constant.t -> env -> Cooking.result -> constant_body
+  env -> Opaqueproof.proofterm Cooking.result -> Opaqueproof.proofterm constant_body
diff --git a/library/global.ml b/library/global.ml
index 06e06a8cf2..58e2380440 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -94,7 +94,8 @@ let make_sprop_cumulative () = globalize0 Safe_typing.make_sprop_cumulative
 let set_allow_sprop b = globalize0 (Safe_typing.set_allow_sprop b)
 let sprop_allowed () = Environ.sprop_allowed (env())
 let export_private_constants ~in_section cd = globalize (Safe_typing.export_private_constants ~in_section cd)
-let add_constant ~in_section id d = globalize (Safe_typing.add_constant ~in_section (i2l id) d)
+let add_constant ?role ~in_section id d = globalize (Safe_typing.add_constant ?role ~in_section (i2l id) d)
+let add_recipe ~in_section id d = globalize (Safe_typing.add_recipe ~in_section (i2l id) d)
 let add_mind id mie = globalize (Safe_typing.add_mind (i2l id) mie)
 let add_modtype id me inl = globalize (Safe_typing.add_modtype (i2l id) me inl)
 let add_module id me inl = globalize (Safe_typing.add_module (i2l id) me inl)
diff --git a/library/global.mli b/library/global.mli
index a60de48897..984d8c666c 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -46,7 +46,8 @@ val export_private_constants : in_section:bool ->
   unit Entries.definition_entry * Safe_typing.exported_private_constant list
 
 val add_constant :
-  in_section:bool -> Id.t -> Safe_typing.global_declaration -> Constant.t
+  ?role:Entries.side_effect_role -> in_section:bool -> Id.t -> Safe_typing.global_declaration -> Constant.t * Safe_typing.private_constants
+val add_recipe : in_section:bool -> Id.t -> Cooking.recipe -> Constant.t
 val add_mind :
   Id.t -> Entries.mutual_inductive_entry -> MutInd.t
 
@@ -84,7 +85,7 @@ val add_module_parameter :
 (** {6 Queries in the global environment } *)
 
 val lookup_named     : variable -> Constr.named_declaration
-val lookup_constant  : Constant.t -> Declarations.constant_body
+val lookup_constant  : Constant.t -> Opaqueproof.opaque Declarations.constant_body
 val lookup_inductive : inductive ->
   Declarations.mutual_inductive_body * Declarations.one_inductive_body
 val lookup_pinductive : Constr.pinductive -> 
@@ -105,7 +106,7 @@ val body_of_constant : Constant.t -> (Constr.constr * Univ.AUContext.t) option
     polymorphic constants, the term contains De Bruijn universe variables that
     need to be instantiated. *)
 
-val body_of_constant_body : Declarations.constant_body -> (Constr.constr * Univ.AUContext.t) option
+val body_of_constant_body : Opaqueproof.opaque Declarations.constant_body -> (Constr.constr * Univ.AUContext.t) option
 (** Same as {!body_of_constant} but on {!Declarations.constant_body}. *)
 
 (** {6 Compiled libraries } *)
diff --git a/library/lib.ml b/library/lib.ml
index a046360822..4be288ed20 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -211,9 +211,6 @@ let split_lib_at_opening sp =
 let add_entry sp node =
   lib_state := { !lib_state with lib_stk = (sp,node) :: !lib_state.lib_stk }
 
-let pull_to_head oname =
-  lib_state := { !lib_state with lib_stk = (oname,List.assoc oname !lib_state.lib_stk) :: List.remove_assoc oname !lib_state.lib_stk }
-
 let anonymous_id =
   let n = ref 0 in
   fun () -> incr n; Names.Id.of_string ("_" ^ (string_of_int !n))
diff --git a/library/lib.mli b/library/lib.mli
index 30569197bc..5da76961a6 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -57,7 +57,6 @@ val segment_of_objects :
 
 val add_leaf : Id.t -> Libobject.obj -> Libobject.object_name
 val add_anonymous_leaf : ?cache_first:bool -> Libobject.obj -> unit
-val pull_to_head : Libobject.object_name -> unit
 
 (** this operation adds all objects with the same name and calls [load_object]
    for each of them *)
diff --git a/plugins/extraction/extraction.mli b/plugins/extraction/extraction.mli
index d27c79cb62..bf98f8cd70 100644
--- a/plugins/extraction/extraction.mli
+++ b/plugins/extraction/extraction.mli
@@ -16,9 +16,9 @@ open Environ
 open Evd
 open Miniml
 
-val extract_constant : env -> Constant.t -> constant_body -> ml_decl
+val extract_constant : env -> Constant.t -> Opaqueproof.opaque constant_body -> ml_decl
 
-val extract_constant_spec : env -> Constant.t -> constant_body -> ml_spec
+val extract_constant_spec : env -> Constant.t -> 'a constant_body -> ml_spec
 
 (** For extracting "module ... with ..." declaration *)
 
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index 399a77c596..4e229a94b6 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -109,7 +109,7 @@ let labels_of_ref r =
 
 (*s Constants tables. *)
 
-let typedefs = ref (Cmap_env.empty : (constant_body * ml_type) Cmap_env.t)
+let typedefs = ref (Cmap_env.empty : (Opaqueproof.opaque constant_body * ml_type) Cmap_env.t)
 let init_typedefs () = typedefs := Cmap_env.empty
 let add_typedef kn cb t =
   typedefs := Cmap_env.add kn (cb,t) !typedefs
@@ -120,7 +120,7 @@ let lookup_typedef kn cb =
   with Not_found -> None
 
 let cst_types =
-  ref (Cmap_env.empty : (constant_body * ml_schema) Cmap_env.t)
+  ref (Cmap_env.empty : (Opaqueproof.opaque constant_body * ml_schema) Cmap_env.t)
 let init_cst_types () = cst_types := Cmap_env.empty
 let add_cst_type kn cb s = cst_types := Cmap_env.add kn (cb,s) !cst_types
 let lookup_cst_type kn cb =
diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli
index acc1bfee8a..7e53964642 100644
--- a/plugins/extraction/table.mli
+++ b/plugins/extraction/table.mli
@@ -72,11 +72,11 @@ val labels_of_ref : GlobRef.t -> ModPath.t * Label.t list
    [mutual_inductive_body] as checksum. In both case, we should ideally
    also check the env *)
 
-val add_typedef : Constant.t -> constant_body -> ml_type -> unit
-val lookup_typedef : Constant.t -> constant_body -> ml_type option
+val add_typedef : Constant.t -> Opaqueproof.opaque constant_body -> ml_type -> unit
+val lookup_typedef : Constant.t -> Opaqueproof.opaque constant_body -> ml_type option
 
-val add_cst_type : Constant.t -> constant_body -> ml_schema -> unit
-val lookup_cst_type : Constant.t -> constant_body -> ml_schema option
+val add_cst_type : Constant.t -> Opaqueproof.opaque constant_body -> ml_schema -> unit
+val lookup_cst_type : Constant.t -> Opaqueproof.opaque constant_body -> ml_schema option
 
 val add_ind : MutInd.t -> mutual_inductive_body -> ml_ind -> unit
 val lookup_ind : MutInd.t -> mutual_inductive_body -> ml_ind option
diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml
index c9f18d89be..5ea9b79336 100644
--- a/pretyping/cbv.ml
+++ b/pretyping/cbv.ml
@@ -145,7 +145,7 @@ let mkSTACK = function
 
 type cbv_infos = {
   env : Environ.env;
-  tab : cbv_value Declarations.constant_def KeyTable.t;
+  tab : (cbv_value, Empty.t) Declarations.constant_def KeyTable.t;
   reds : RedFlags.reds;
   sigma : Evd.evar_map
 }
diff --git a/tactics/abstract.ml b/tactics/abstract.ml
index 499152f39a..6dd9a976f9 100644
--- a/tactics/abstract.ml
+++ b/tactics/abstract.ml
@@ -158,9 +158,9 @@ let cache_term_by_tactic_then ~opaque ~name_op ?(goal_type=None) tac tacK =
     (* do not compute the implicit arguments, it may be costly *)
     let () = Impargs.make_implicit_args false in
     (* ppedrot: seems legit to have abstracted subproofs as local*)
-    Declare.declare_constant ~internal:Declare.InternalTacticRequest ~local:true id decl
+    Declare.declare_private_constant ~role:Entries.Subproof ~internal:Declare.InternalTacticRequest ~local:true id decl
   in
-  let cst = Impargs.with_implicit_protection cst () in
+  let cst, eff = Impargs.with_implicit_protection cst () in
   let inst = match const.Entries.const_entry_universes with
   | Entries.Monomorphic_entry _ -> EInstance.empty
   | Entries.Polymorphic_entry (_, ctx) ->
@@ -174,7 +174,6 @@ let cache_term_by_tactic_then ~opaque ~name_op ?(goal_type=None) tac tacK =
   let lem = mkConstU (cst, inst) in
   let evd = Evd.set_universe_context evd ectx in
   let open Safe_typing in
-  let eff = private_constant (Global.safe_env ()) Entries.Subproof cst in
   let effs = concat_private eff
     Entries.(snd (Future.force const.const_entry_body)) in
   let solve =
diff --git a/tactics/ind_tables.ml b/tactics/ind_tables.ml
index e95778a90d..b9485b8823 100644
--- a/tactics/ind_tables.ml
+++ b/tactics/ind_tables.ml
@@ -116,8 +116,7 @@ let compute_name internal id =
   | InternalTacticRequest ->
       Namegen.next_ident_away_from (add_prefix "internal_" id) is_visible_name
 
-let define internal id c poly univs =
-  let fd = declare_constant ~internal in
+let define internal role id c poly univs =
   let id = compute_name internal id in
   let ctx = UState.minimize univs in
   let c = UnivSubst.nf_evars_and_universes_opt_subst (fun _ -> None) (UState.subst ctx) c in
@@ -133,12 +132,12 @@ let define internal id c poly univs =
     const_entry_inline_code = false;
     const_entry_feedback = None;
   } in
-  let kn = fd id (DefinitionEntry entry, Decl_kinds.IsDefinition Scheme) in
+  let kn, eff = declare_private_constant ~role ~internal id (DefinitionEntry entry, Decl_kinds.IsDefinition Scheme) in
   let () = match internal with
     | InternalTacticRequest -> ()
     | _-> definition_message id
   in
-  kn
+  kn, eff
 
 let define_individual_scheme_base kind suff f mode idopt (mind,i as ind) =
   let (c, ctx), eff = f mode ind in
@@ -146,9 +145,8 @@ let define_individual_scheme_base kind suff f mode idopt (mind,i as ind) =
   let id = match idopt with
     | Some id -> id
     | None -> add_suffix mib.mind_packets.(i).mind_typename suff in
-  let const = define mode id c (Declareops.inductive_is_polymorphic mib) ctx in
   let role = Entries.Schema (ind, kind) in
-  let neff = Safe_typing.private_constant (Global.safe_env ()) role const in
+  let const, neff = define mode role id c (Declareops.inductive_is_polymorphic mib) ctx in
   declare_scheme kind [|ind,const|];
   const, Safe_typing.concat_private neff eff
 
@@ -165,9 +163,8 @@ let define_mutual_scheme_base kind suff f mode names mind =
       try Int.List.assoc i names
       with Not_found -> add_suffix mib.mind_packets.(i).mind_typename suff) in
   let fold i effs id cl =
-    let cst = define mode id cl (Declareops.inductive_is_polymorphic mib) ctx in
     let role = Entries.Schema ((mind, i), kind)in
-    let neff = Safe_typing.private_constant (Global.safe_env ()) role cst in
+    let cst, neff = define mode role id cl (Declareops.inductive_is_polymorphic mib) ctx in
     (Safe_typing.concat_private neff effs, cst)
   in
   let (eff, consts) = Array.fold_left2_map_i fold eff ids cl in