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

8 files changed, 32 insertions, 25 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 ->
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 75375812c0..f2e7cff8ec 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -797,7 +797,7 @@ let export_private_constants ~in_section ce senv =
   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_constant ?role ~in_section l decl senv =
   let kn = Constant.make2 senv.modpath l in
   let senv =
     let cb = 
@@ -822,7 +822,11 @@ 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 -> private_constant senv role kn
+  in
+  (kn, eff), senv
 
 (** Insertion of inductive types *)
 
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index d6c7022cf5..b9a68663d3 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
@@ -103,8 +100,8 @@ 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
 
 (** Adding an inductive type *)
 
diff --git a/library/global.ml b/library/global.ml
index 06e06a8cf2..33cdbd88ea 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -94,7 +94,7 @@ 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_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..f65ffaa2ee 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -46,7 +46,7 @@ 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_mind :
   Id.t -> Entries.mutual_inductive_entry -> MutInd.t
 
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