[obligations] `declare_obligation` now takes an `UState.t`

This removes a use of internal obligation data `prg_poly` and a couple
of duplicate lines.

3 files changed, 19 insertions, 20 deletions

diff --git a/vernac/declare.ml b/vernac/declare.ml
index 333b186b22..c77d4909da 100644
--- a/vernac/declare.ml
+++ b/vernac/declare.ml
@@ -1210,19 +1210,20 @@ let get_hide_obligations =
     ~key:["Hide"; "Obligations"]
     ~value:false
 
-let declare_obligation prg obl body ty uctx =
+let declare_obligation prg obl ~uctx ~types ~body =
+  let univs = UState.univ_entry ~poly:prg.prg_poly uctx in
   let body = prg.prg_reduce body in
-  let ty = Option.map prg.prg_reduce ty in
+  let types = Option.map prg.prg_reduce types in
   match obl.obl_status with
   | _, Evar_kinds.Expand -> (false, {obl with obl_body = Some (TermObl body)})
   | force, Evar_kinds.Define opaque ->
     let opaque = (not force) && opaque in
     let poly = prg.prg_poly in
     let ctx, body, ty, args =
-      if not poly then shrink_body body ty
-      else ([], body, ty, [||])
+      if not poly then shrink_body body types
+      else ([], body, types, [||])
     in
-    let ce = definition_entry ?types:ty ~opaque ~univs:uctx body in
+    let ce = definition_entry ?types:ty ~opaque ~univs body in
     (* ppedrot: seems legit to have obligations as local *)
     let constant =
       declare_constant ~name:obl.obl_name
@@ -1234,7 +1235,7 @@ let declare_obligation prg obl body ty uctx =
       add_hint (Locality.make_section_locality None) prg constant;
     definition_message obl.obl_name;
     let body =
-      match uctx with
+      match univs with
       | Entries.Polymorphic_entry (_, uctx) ->
         Some (DefinedObl (constant, Univ.UContext.instance uctx))
       | Entries.Monomorphic_entry _ ->
@@ -1621,8 +1622,7 @@ let obligation_terminator entries uctx {name; num; auto} =
     in
     let obl = {obl with obl_status = (false, status)} in
     let uctx = if prg.prg_poly then uctx else UState.union prg.prg_ctx uctx in
-    let univs = UState.univ_entry ~poly:prg.prg_poly uctx in
-    let defined, obl = declare_obligation prg obl body ty univs in
+    let defined, obl = declare_obligation prg obl ~body ~types:ty ~uctx in
     let prg_ctx =
       if prg.prg_poly then
         (* Polymorphic *)
diff --git a/vernac/declare.mli b/vernac/declare.mli
index 275a70fd7b..647896e2f5 100644
--- a/vernac/declare.mli
+++ b/vernac/declare.mli
@@ -446,13 +446,14 @@ module ProgramDecl : sig
   val set_uctx : uctx:UState.t -> t -> t
 end
 
-(** [declare_obligation] Save an obligation *)
+(** [declare_obligation prg obl ~uctx ~types ~body] Save an obligation
+   [obl] for program definition [prg] *)
 val declare_obligation :
      ProgramDecl.t
   -> Obligation.t
-  -> Constr.types
-  -> Constr.types option
-  -> Entries.universes_entry
+  -> uctx:UState.t
+  -> types:Constr.types option
+  -> body:Constr.types
   -> bool * Obligation.t
 
 module State : sig
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index bbc20d5e30..62d1065e75 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -53,7 +53,6 @@ module Error = struct
 
 end
 
-let assumption_message = Declare.assumption_message
 let default_tactic = ref (Proofview.tclUNIT ())
 
 let evar_of_obligation o = Evd.make_evar (Global.named_context_val ()) (EConstr.of_constr o.obl_type)
@@ -183,16 +182,15 @@ and solve_obligation_by_tac prg obls i tac =
         match solve_by_tac ?loc:(fst obl.obl_location) obl.obl_name (evar_of_obligation obl) tac
                 prg.prg_poly (Evd.evar_universe_context evd) with
         | None -> None
-        | Some (t, ty, ctx) ->
-          let prg = ProgramDecl.set_uctx ~uctx:ctx prg in
+        | Some (t, ty, uctx) ->
+          let prg = ProgramDecl.set_uctx ~uctx prg in
           (* Why is uctx not used above? *)
-          let uctx = UState.univ_entry ~poly:prg.prg_poly ctx in
-          let def, obl' = declare_obligation prg obl t ty uctx in
+          let def, obl' = declare_obligation prg obl ~body:t ~types:ty ~uctx in
           obls.(i) <- obl';
           if def && not prg.prg_poly then (
             (* Declare the term constraints with the first obligation only *)
-            let uctx = UState.from_env (Global.env ()) in
-            let uctx = UState.merge_subst uctx (UState.subst ctx) in
+            let uctx_global = UState.from_env (Global.env ()) in
+            let uctx = UState.merge_subst uctx_global (UState.subst uctx) in
             Some (ProgramDecl.set_uctx ~uctx prg))
           else Some prg
       else None
@@ -372,7 +370,7 @@ let admit_prog prg =
             let kn = Declare.declare_constant ~name:x.obl_name ~local:Declare.ImportNeedQualified
               (Declare.ParameterEntry (None, (x.obl_type, ctx), None)) ~kind:Decls.(IsAssumption Conjectural)
             in
-              assumption_message x.obl_name;
+              Declare.assumption_message x.obl_name;
               obls.(i) <- Obligation.set_body ~body:(DefinedObl (kn, Univ.Instance.empty)) x
         | Some _ -> ())
       obls;