5 files changed, 21 insertions, 33 deletions
diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml
index 5323c9f1c6..bb640a83f6 100644
--- a/vernac/auto_ind_decl.ml
+++ b/vernac/auto_ind_decl.ml
@@ -385,7 +385,7 @@ let build_beq_scheme mode kn =
           Vars.substl subst cores.(i)
         in
         create_input fix),
-       UState.make ~lbound:(Global.universes_lbound ()) (Global.universes ()))
+       UState.from_env (Global.env ()))
 
 let beq_scheme_kind =
   declare_mutual_scheme_object "_beq"
@@ -707,7 +707,7 @@ let make_bl_scheme mode mind =
   let lnonparrec,lnamesparrec = (* TODO subst *)
     context_chop (nparams-nparrec) mib.mind_params_ctxt in
   let bl_goal = compute_bl_goal ind lnamesparrec nparrec in
-  let uctx = UState.make ~lbound:(Global.universes_lbound ()) (Global.universes ()) in
+  let uctx = UState.from_env (Global.env ()) 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
@@ -840,7 +840,7 @@ let make_lb_scheme mode mind =
   let lnonparrec,lnamesparrec =
     context_chop (nparams-nparrec) mib.mind_params_ctxt in
   let lb_goal = compute_lb_goal ind lnamesparrec nparrec in
-  let uctx = UState.make ~lbound:(Global.universes_lbound ()) (Global.universes ()) in
+  let uctx = UState.from_env (Global.env ()) 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
@@ -1010,7 +1010,7 @@ let make_eq_decidability mode mind =
   let nparams = mib.mind_nparams in
   let nparrec = mib.mind_nparams_rec in
   let u = Univ.Instance.empty in
-  let uctx = UState.make ~lbound:(Global.universes_lbound ()) (Global.universes ()) in
+  let uctx = UState.from_env (Global.env ()) in
   let lnonparrec,lnamesparrec =
     context_chop (nparams-nparrec) mib.mind_params_ctxt in
   let side_eff = side_effect_of_mode mode in
diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml
index eac8f92e2e..d56917271c 100644
--- a/vernac/comDefinition.ml
+++ b/vernac/comDefinition.ml
@@ -126,7 +126,7 @@ let do_definition_program ?hook ~name ~scope ~poly ~kind udecl bl red_option c c
   let (body, types), evd, udecl, impargs =
     interp_definition ~program_mode udecl bl ~poly red_option c ctypopt
   in
-  let term, ty, uctx, obls = Declare.prepare_obligation ~name ~poly ~body ~types ~udecl evd in
+  let term, ty, uctx, obls = Declare.prepare_obligation ~name ~body ~types evd in
   let _ : Declare.Obls.progress =
     Obligations.add_definition
       ~name ~term ty ~uctx ~udecl ~impargs ~scope ~poly ~kind ?hook obls
diff --git a/vernac/declare.ml b/vernac/declare.ml
index c291890dce..333b186b22 100644
--- a/vernac/declare.ml
+++ b/vernac/declare.ml
@@ -1007,25 +1007,20 @@ let declare_definition ~name ~scope ~kind ~opaque ~impargs ~udecl ?hook
   let entry, uctx = prepare_definition ?fix_exn ~opaque ~poly ~udecl ~types ~body ?inline sigma in
   declare_entry ~name ~scope ~kind ~impargs ?obls ?hook ~uctx entry
 
-let prepare_obligation ?opaque ?inline ~name ~poly ~udecl ~types ~body sigma =
+let prepare_obligation ~name ~types ~body sigma =
+  let env = Global.env () in
+  let types = match types with
+    | Some t -> t
+    | None -> Retyping.get_type_of env sigma body
+  in
   let sigma, (body, types) = Evarutil.finalize ~abort_on_undefined_evars:false
-      sigma (fun nf -> nf body, Option.map nf types)
+      sigma (fun nf -> nf body, nf types)
   in
-  let univs = Evd.check_univ_decl ~poly sigma udecl in
-  let ce = definition_entry ?opaque ?inline ?types ~univs body in
-  let env = Global.env () in
-  let (c,ctx), sideff = Future.force ce.proof_entry_body in
-  assert(Safe_typing.is_empty_private_constants sideff.Evd.seff_private);
-  assert(Univ.ContextSet.is_empty ctx);
   RetrieveObl.check_evars env sigma;
-  let c = EConstr.of_constr c in
-  let typ = match ce.proof_entry_type with
-    | Some t -> EConstr.of_constr t
-    | None -> Retyping.get_type_of env sigma c
-  in
-  let obls, _, c, cty = RetrieveObl.retrieve_obligations env name sigma 0 c typ in
+  let body, types = EConstr.(of_constr body, of_constr types) in
+  let obls, _, body, cty = RetrieveObl.retrieve_obligations env name sigma 0 body types in
   let uctx = Evd.evar_universe_context sigma in
-  c, cty, uctx, obls
+  body, cty, uctx, obls
 
 let prepare_parameter ~poly ~udecl ~types sigma =
   let env = Global.env () in
@@ -1641,7 +1636,7 @@ let obligation_terminator entries uctx {name; num; auto} =
            universes and constraints if any *)
         defined
       then
-        UState.make ~lbound:(Global.universes_lbound ()) (Global.universes ())
+        UState.from_env (Global.env ())
       else uctx
     in
     update_program_decl_on_defined prg obls num obl ~uctx:prg_ctx rem ~auto
@@ -1673,9 +1668,7 @@ let obligation_admitted_terminator {name; num; auto} ctx' dref =
     if not prg.prg_poly (* Not polymorphic *) then
       (* The universe context was declared globally, we continue
          from the new global environment. *)
-      let ctx =
-        UState.make ~lbound:(Global.universes_lbound ()) (Global.universes ())
-      in
+      let ctx = UState.from_env (Global.env ()) in
       let ctx' = UState.merge_subst ctx (UState.subst ctx') in
       (Univ.Instance.empty, ctx')
     else
diff --git a/vernac/declare.mli b/vernac/declare.mli
index 82b0cff8d9..62bc6a34bf 100644
--- a/vernac/declare.mli
+++ b/vernac/declare.mli
@@ -367,11 +367,7 @@ val declare_mutually_recursive
 
 (** Prepare API, to be removed once we provide the corresponding 1-step API *)
 val prepare_obligation
-  :  ?opaque:bool
-  -> ?inline:bool
-  -> name:Id.t
-  -> poly:bool
-  -> udecl:UState.universe_decl
+  :  name:Id.t
   -> types:EConstr.t option
   -> body:EConstr.t
   -> Evd.evar_map
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index 5fdee9f2d4..bbc20d5e30 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -191,10 +191,9 @@ and solve_obligation_by_tac prg obls i tac =
           obls.(i) <- obl';
           if def && not prg.prg_poly then (
             (* Declare the term constraints with the first obligation only *)
-            let evd = Evd.from_env (Global.env ()) in
-            let evd = Evd.merge_universe_subst evd (UState.subst ctx) in
-            let ctx' = Evd.evar_universe_context evd in
-            Some (ProgramDecl.set_uctx ~uctx:ctx' prg))
+            let uctx = UState.from_env (Global.env ()) in
+            let uctx = UState.merge_subst uctx (UState.subst ctx) in
+            Some (ProgramDecl.set_uctx ~uctx prg))
           else Some prg
       else None