Merge the definition of constants and private constants in the API.

2 files changed, 15 insertions, 5 deletions

diff --git a/interp/declare.ml b/interp/declare.ml
index 9640ea26a6..29da49f29d 100644
--- a/interp/declare.ml
+++ b/interp/declare.ml
@@ -78,7 +78,8 @@ let cache_constant ((sp,kn), obj) =
       then Constant.make1 kn
       else CErrors.anomaly Pp.(str"Missing constant " ++ Id.print(basename sp) ++ str".")
     | Some r ->
-      Global.add_constant ~in_section:(Lib.sections_are_opened ()) id (GlobalRecipe r)
+      let kn, _ = Global.add_constant ~in_section:(Lib.sections_are_opened ()) id (GlobalRecipe r) in
+      kn
   in
   assert (Constant.equal kn' (Constant.make1 kn));
   Nametab.push (Nametab.Until 1) sp (ConstRef (Constant.make1 kn));
@@ -149,7 +150,7 @@ let definition_entry ?fix_exn ?(opaque=false) ?(inline=false) ?types
     const_entry_feedback = None;
     const_entry_inline_code = inline}
 
-let define_constant ?(export_seff=false) id cd =
+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
@@ -167,17 +168,23 @@ let define_constant ?(export_seff=false) id cd =
       export, ConstantEntry (PureEntry, DefinitionEntry de)
     | _ -> [], ConstantEntry (EffectEntry, cd)
   in
-  let kn = Global.add_constant ~in_section id decl in
-  kn, export
+  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, export = define_constant ~export_seff id cd 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 () = 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)
   id ?types (body,univs) =
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 ->