Fix obligations handling of universes anticipating stronger restrict

1 files changed, 54 insertions, 40 deletions

diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index 97cdd7977..17a596c42 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -824,49 +824,63 @@ let obligation_terminator name num guard hook auto pf =
   match pf with
   | Admitted _ -> apply_terminator term pf
   | Proved (opq, id, proof) ->
-    if not !shrink_obligations then apply_terminator term pf
-    else
-      let (_, (entry, uctx, _)) = Pfedit.cook_this_proof proof in
-      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), () = 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;
-      (** Declare the obligation ourselves and drop the hook *)
-      let prg = get_info (ProgMap.find name !from_prg) in
-      (** Ensure universes are substituted properly in body and type *)
-      let body = EConstr.to_constr sigma (EConstr.of_constr body) in
-      let ty = Option.map (fun x -> EConstr.to_constr sigma (EConstr.of_constr x)) ty in
-      let ctx = Evd.evar_universe_context sigma in
-      let prg = { prg with prg_ctx = ctx } in
-      let obls, rem = prg.prg_obligations in
-      let obl = obls.(num) in
-      let status =
-        match obl.obl_status, opq with
-        | (_, Evar_kinds.Expand), Vernacexpr.Opaque -> err_not_transp ()
-        | (true, _), Vernacexpr.Opaque -> err_not_transp ()
-        | (false, _), Vernacexpr.Opaque -> Evar_kinds.Define true
-        | (_, Evar_kinds.Define true), Vernacexpr.Transparent -> Evar_kinds.Define false
-        | (_, status), Vernacexpr.Transparent -> status
-      in
-      let obl = { obl with obl_status = false, status } in
-      let uctx = UState.const_univ_entry ~poly:(pi2 prg.prg_kind) ctx in
-      let (_, obl) = declare_obligation prg obl body ty uctx in
-      let obls = Array.copy obls in
-      let _ = obls.(num) <- obl in
-      try
+    let (_, (entry, uctx, _)) = Pfedit.cook_this_proof proof in
+    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), () = 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;
+    (** Declare the obligation ourselves and drop the hook *)
+    let prg = get_info (ProgMap.find name !from_prg) in
+    (** Ensure universes are substituted properly in body and type *)
+    let body = EConstr.to_constr sigma (EConstr.of_constr body) in
+    let ty = Option.map (fun x -> EConstr.to_constr sigma (EConstr.of_constr x)) ty in
+    let ctx = Evd.evar_universe_context sigma in
+    let obls, rem = prg.prg_obligations in
+    let obl = obls.(num) in
+    let status =
+      match obl.obl_status, opq with
+      | (_, Evar_kinds.Expand), Vernacexpr.Opaque -> err_not_transp ()
+      | (true, _), Vernacexpr.Opaque -> err_not_transp ()
+      | (false, _), Vernacexpr.Opaque -> Evar_kinds.Define true
+      | (_, Evar_kinds.Define true), Vernacexpr.Transparent ->
+        Evar_kinds.Define false
+      | (_, status), Vernacexpr.Transparent -> status
+    in
+    let obl = { obl with obl_status = false, status } in
+    let ctx =
+      if pi2 prg.prg_kind then ctx
+      else UState.union prg.prg_ctx ctx
+    in
+    let uctx = UState.const_univ_entry ~poly:(pi2 prg.prg_kind) ctx in
+    let (_, obl) = declare_obligation prg obl body ty uctx in
+    let obls = Array.copy obls in
+    let _ = obls.(num) <- obl in
+    let prg_ctx =
+      if pi2 (prg.prg_kind) then (* Polymorphic *)
+        (** We merge the new universes and constraints of the
+            polymorphic obligation with the existing ones *)
+        UState.union prg.prg_ctx ctx
+      else
+        (** The first obligation declares the univs of the constant,
+            each subsequent obligation declares its own additional
+            universes and constraints if any *)
+        UState.make (Global.universes ())
+    in
+    let prg = { prg with prg_ctx } in
+    try
       ignore (update_obls prg obls (pred rem));
       if pred rem > 0 then
         begin
-	  let deps = dependencies obls num in
-	  if not (Int.Set.is_empty deps) then
-	    ignore (auto (Some name) None deps)
-	end
-      with e when CErrors.noncritical e ->
-        let e = CErrors.push e in
-        pperror (CErrors.iprint (ExplainErr.process_vernac_interp_error e))
+          let deps = dependencies obls num in
+          if not (Int.Set.is_empty deps) then
+            ignore (auto (Some name) None deps)
+        end
+    with e when CErrors.noncritical e ->
+      let e = CErrors.push e in
+      pperror (CErrors.iprint (ExplainErr.process_vernac_interp_error e))
 
 let obligation_hook prg obl num auto ctx' _ gr =
   let obls, rem = prg.prg_obligations in