Simplify the private constant API.

We ungroup the rewrite scheme-defined constants, while only exporting a
function to turn the last added constant into a private constant.

2 files changed, 12 insertions, 10 deletions

diff --git a/tactics/abstract.ml b/tactics/abstract.ml
index 7a61deba0c..499152f39a 100644
--- a/tactics/abstract.ml
+++ b/tactics/abstract.ml
@@ -174,7 +174,7 @@ 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_con_of_con (Global.safe_env ()) cst 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 16829482e5..e95778a90d 100644
--- a/tactics/ind_tables.ml
+++ b/tactics/ind_tables.ml
@@ -147,9 +147,10 @@ let define_individual_scheme_base kind suff f mode idopt (mind,i as ind) =
     | 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
   declare_scheme kind [|ind,const|];
-  const, Safe_typing.concat_private
-     (Safe_typing.private_con_of_scheme ~kind (Global.safe_env()) [ind,const]) eff
+  const, Safe_typing.concat_private neff eff
 
 let define_individual_scheme kind mode names (mind,i as ind) =
   match Hashtbl.find scheme_object_table kind with
@@ -163,15 +164,16 @@ let define_mutual_scheme_base kind suff f mode names mind =
   let ids = Array.init (Array.length mib.mind_packets) (fun i ->
       try Int.List.assoc i names
       with Not_found -> add_suffix mib.mind_packets.(i).mind_typename suff) in
-  let consts = Array.map2 (fun id cl -> 
-     define mode id cl (Declareops.inductive_is_polymorphic mib) ctx) ids cl 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
+    (Safe_typing.concat_private neff effs, cst)
+  in
+  let (eff, consts) = Array.fold_left2_map_i fold eff ids cl in
   let schemes = Array.mapi (fun i cst -> ((mind,i),cst)) consts in
   declare_scheme kind schemes;
-  consts,
-  Safe_typing.concat_private
-    (Safe_typing.private_con_of_scheme
-      ~kind (Global.safe_env()) (Array.to_list schemes))
-    eff 
+  consts, eff
 
 let define_mutual_scheme kind mode names mind =
   match Hashtbl.find scheme_object_table kind with