[funind] Remove use of low-level entries in scheme generation.

This is needed to make this low-level entry structures privates;
moreover, the code seems much clearer using the higher-level API.

Some more cleanup needs to be done but this is clearly a step forward
IMHO.

6 files changed, 13 insertions, 9 deletions

diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml
index ebea5e146c..743d1d2026 100644
--- a/vernac/auto_ind_decl.ml
+++ b/vernac/auto_ind_decl.ml
@@ -710,7 +710,7 @@ let make_bl_scheme mode mind =
   let uctx = UState.make ~lbound:(Global.universes_lbound ()) (Global.universes ()) in
   let side_eff = side_effect_of_mode mode in
   let bl_goal = EConstr.of_constr bl_goal in
-  let (ans, _, _, ctx) = Declare.build_by_tactic ~poly:false ~side_eff (Global.env()) ~uctx ~typ:bl_goal
+  let (ans, _, _, _, ctx) = Declare.build_by_tactic ~poly:false ~side_eff (Global.env()) ~uctx ~typ:bl_goal
     (compute_bl_tact mode (!bl_scheme_kind_aux()) (ind, EConstr.EInstance.empty) lnamesparrec nparrec)
   in
   ([|ans|], ctx)
@@ -843,7 +843,7 @@ let make_lb_scheme mode mind =
   let uctx = UState.make ~lbound:(Global.universes_lbound ()) (Global.universes ()) in
   let side_eff = side_effect_of_mode mode in
   let lb_goal = EConstr.of_constr lb_goal in
-  let (ans, _, _, ctx) = Declare.build_by_tactic ~poly:false ~side_eff (Global.env()) ~uctx ~typ:lb_goal
+  let (ans, _, _, _, ctx) = Declare.build_by_tactic ~poly:false ~side_eff (Global.env()) ~uctx ~typ:lb_goal
     (compute_lb_tact mode (!lb_scheme_kind_aux()) ind lnamesparrec nparrec)
   in
   ([|ans|], ctx)
@@ -1014,7 +1014,7 @@ let make_eq_decidability mode mind =
   let lnonparrec,lnamesparrec =
     context_chop (nparams-nparrec) mib.mind_params_ctxt in
   let side_eff = side_effect_of_mode mode in
-  let (ans, _, _, ctx) = Declare.build_by_tactic ~poly:false ~side_eff (Global.env()) ~uctx
+  let (ans, _, _, _, ctx) = Declare.build_by_tactic ~poly:false ~side_eff (Global.env()) ~uctx
       ~typ:(EConstr.of_constr (compute_dec_goal (ind,u) lnamesparrec nparrec))
       (compute_dec_tact ind lnamesparrec nparrec)
   in
diff --git a/vernac/declare.ml b/vernac/declare.ml
index 357f58feea..95e573a671 100644
--- a/vernac/declare.ml
+++ b/vernac/declare.ml
@@ -762,7 +762,7 @@ let build_constant_by_tactic ~name ?(opaque=Transparent) ~uctx ~sign ~poly typ t
 let build_by_tactic ?(side_eff=true) env ~uctx ~poly ~typ tac =
   let name = Id.of_string ("temporary_proof"^string_of_int (next())) in
   let sign = Environ.(val_of_named_context (named_context env)) in
-  let ce, status, univs = build_constant_by_tactic ~name ~uctx ~sign ~poly typ tac in
+  let ce, status, uctx = build_constant_by_tactic ~name ~uctx ~sign ~poly typ tac in
   let cb, uctx =
     if side_eff then inline_private_constants ~uctx env ce
     else
@@ -770,7 +770,7 @@ let build_by_tactic ?(side_eff=true) env ~uctx ~poly ~typ tac =
       let (cb, ctx), _eff = Future.force ce.proof_entry_body in
       cb, UState.merge ~sideff:false Evd.univ_rigid uctx ctx
   in
-  cb, ce.proof_entry_type, status, univs
+  cb, ce.proof_entry_type, ce.proof_entry_universes, status, uctx
 
 let declare_abstract ~name ~poly ~kind ~sign ~secsign ~opaque ~solve_tac sigma concl =
   (* EJGA: flush_and_check_evars is only used in abstract, could we
diff --git a/vernac/declare.mli b/vernac/declare.mli
index e23e148ddc..a297f25868 100644
--- a/vernac/declare.mli
+++ b/vernac/declare.mli
@@ -249,7 +249,7 @@ val build_by_tactic
   -> poly:bool
   -> typ:EConstr.types
   -> unit Proofview.tactic
-  -> Constr.constr * Constr.types option * bool * UState.t
+  -> Constr.constr * Constr.types option * Entries.universes_entry * bool * UState.t
 
 (** {6 Helpers to obtain proof state when in an interactive proof } *)
 
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index 060f069419..bed593234b 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -133,7 +133,7 @@ let solve_by_tac ?loc name evi t poly uctx =
   try
     (* the status is dropped. *)
     let env = Global.env () in
-    let body, types, _, uctx =
+    let body, types, _univs, _, uctx =
       Declare.build_by_tactic env ~uctx ~poly ~typ:evi.evar_concl t in
     Inductiveops.control_only_guard env (Evd.from_ctx uctx) (EConstr.of_constr body);
     Some (body, types, uctx)
diff --git a/vernac/pfedit.ml b/vernac/pfedit.ml
index d6b9592176..1b34b6ec28 100644
--- a/vernac/pfedit.ml
+++ b/vernac/pfedit.ml
@@ -5,5 +5,9 @@ let by = Declare.by
 let refine_by_tactic = Proof.refine_by_tactic
 
 (* We don't want to export this anymore, but we do for now *)
-let build_by_tactic = Declare.build_by_tactic
+let build_by_tactic ?side_eff env ~uctx ~poly ~typ tac =
+  let b, t, _unis, safe, uctx =
+    Declare.build_by_tactic ?side_eff env ~uctx ~poly ~typ tac in
+  b, t, safe, uctx
+
 let build_constant_by_tactic = Declare.build_constant_by_tactic
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index df39c617d3..df94f69cf6 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -475,7 +475,7 @@ let program_inference_hook env sigma ev =
             Evarutil.is_ground_term sigma concl)
     then None
     else
-      let c, _, _, ctx =
+      let c, _, _, _, ctx =
         Declare.build_by_tactic ~poly:false env ~uctx:(Evd.evar_universe_context sigma) ~typ:concl tac
       in
       Some (Evd.set_universe_context sigma ctx, EConstr.of_constr c)