1 files changed, 18 insertions, 28 deletions

diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index c09cc1977..a4fe49020 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -285,7 +285,7 @@ type obligation =
   { obl_name : Id.t;
     obl_type : types;
     obl_location : Evar_kinds.t Loc.located;
-    obl_body : constant obligation_body option;
+    obl_body : pconstant obligation_body option;
     obl_status : bool * Evar_kinds.obligation_definition_status;
     obl_deps : Int.Set.t;
     obl_tac : unit Proofview.tactic option;
@@ -350,7 +350,7 @@ let get_shrink_obligations () = !shrink_obligations
 
 let _ =
   declare_bool_option
-    { optdepr  = true;
+    { optdepr  = true; (* remove in 8.8 *)
       optname  = "Shrinking of Program obligations";
       optkey   = ["Shrink";"Obligations"];
       optread  = get_shrink_obligations;
@@ -358,18 +358,8 @@ let _ =
 
 let evar_of_obligation o = make_evar (Global.named_context_val ()) o.obl_type
 
-let get_body obl =
-  match obl.obl_body with
-  | None -> None
-  | Some (DefinedObl c) ->
-    let u = Environ.constant_instance (Global.env ()) c in
-    let pc = (c, u) in
-      Some (DefinedObl pc)
-  | Some (TermObl c) ->
-      Some (TermObl c)
-
 let get_obligation_body expand obl =
-  match get_body obl with
+  match obl.obl_body with
   | None -> None
   | Some c ->
      if expand && snd obl.obl_status == Evar_kinds.Expand then
@@ -646,12 +636,12 @@ let declare_obligation prg obl body ty uctx =
 	  shrink_body body ty else [], body, ty, [||]
       in
       let body = ((body,Univ.ContextSet.empty),Safe_typing.empty_private_constants) in
+      let univs = if poly then Polymorphic_const_entry uctx else Monomorphic_const_entry uctx in
       let ce =
         { const_entry_body = Future.from_val ~fix_exn:(fun x -> x) body;
           const_entry_secctx = None;
 	  const_entry_type = ty;
-	  const_entry_polymorphic = poly;
-	  const_entry_universes = uctx;
+	  const_entry_universes = univs;
 	  const_entry_opaque = opaque;
           const_entry_inline_code = false;
           const_entry_feedback = None;
@@ -664,7 +654,7 @@ let declare_obligation prg obl body ty uctx =
 	definition_message obl.obl_name;
 	true, { obl with obl_body =
 	    if poly then
-	      Some (DefinedObl constant)
+	      Some (DefinedObl (constant, Univ.UContext.instance uctx))
 	    else
 	      Some (TermObl (it_mkLambda_or_LetIn_or_clean (mkApp (mkConst constant, args)) ctx)) }
 
@@ -828,8 +818,7 @@ let solve_by_tac name evi t poly ctx =
     id ~goal_kind:(goal_kind poly) ctx evi.evar_hyps concl (Tacticals.New.tclCOMPLETE t) in
   let env = Global.env () in
   let entry = Safe_typing.inline_private_constants_in_definition_entry env entry in
-  let body, eff = Future.force entry.const_entry_body in
-  assert(Safe_typing.empty_private_constants = eff);
+  let body, () = Future.force entry.const_entry_body in
   let ctx' = Evd.merge_context_set ~sideff:true Evd.univ_rigid (Evd.from_ctx ctx') (snd body) in
   Inductiveops.control_only_guard (Global.env ()) (fst body);
   (fst body), entry.const_entry_type, Evd.evar_universe_context ctx'
@@ -846,8 +835,7 @@ let obligation_terminator name num guard hook auto pf =
       let env = Global.env () in
       let entry = Safe_typing.inline_private_constants_in_definition_entry env entry in
       let ty = entry.Entries.const_entry_type in
-      let (body, cstr), eff = Future.force entry.Entries.const_entry_body in
-      assert(Safe_typing.empty_private_constants = eff);
+      let (body, cstr), () = Future.force entry.Entries.const_entry_body in
       let sigma = Evd.from_ctx (fst uctx) in
       let sigma = Evd.merge_context_set ~sideff:true Evd.univ_rigid sigma cstr in
       Inductiveops.control_only_guard (Global.env ()) body;
@@ -892,20 +880,22 @@ let obligation_hook prg obl num auto ctx' _ gr =
        if not transparent then err_not_transp ()
     | _ -> ()
 in
-  let obl = { obl with obl_body = Some (DefinedObl cst) } in
-  let () = if transparent then add_hint true prg cst in
-  let obls = Array.copy obls in
-  let _ = obls.(num) <- obl in
   let ctx' = match ctx' with None -> prg.prg_ctx | Some ctx' -> ctx' in
-  let ctx' =
+  let inst, ctx' =
     if not (pi2 prg.prg_kind) (* Not polymorphic *) then
       (* The universe context was declared globally, we continue
          from the new global environment. *)
       let evd = Evd.from_env (Global.env ()) in
       let ctx' = Evd.merge_universe_subst evd (Evd.universe_subst (Evd.from_ctx ctx')) in
-        Evd.evar_universe_context ctx'
-    else ctx'
+      Univ.Instance.empty, Evd.evar_universe_context ctx'
+    else
+      let (_, uctx) = UState.universe_context ctx' in
+      Univ.UContext.instance uctx, ctx'
   in
+  let obl = { obl with obl_body = Some (DefinedObl (cst, inst)) } in
+  let () = if transparent then add_hint true prg cst in
+  let obls = Array.copy obls in
+  let _ = obls.(num) <- obl in
   let prg = { prg with prg_ctx = ctx' } in
   let () =
     try ignore (update_obls prg obls (pred rem))
@@ -1132,7 +1122,7 @@ let admit_prog prg =
               (ParameterEntry (None,false,(x.obl_type,ctx),None), IsAssumption Conjectural)
             in
               assumption_message x.obl_name;
-              obls.(i) <- { x with obl_body = Some (DefinedObl kn) }
+              obls.(i) <- { x with obl_body = Some (DefinedObl (kn, Univ.Instance.empty)) }
         | Some _ -> ())
       obls;
     ignore(update_obls prg obls 0)