Merge PR #12371: [obligations] Minor refactoring

Reviewed-by: SkySkimmer

3 files changed, 41 insertions, 44 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 62bc6a34bf..647896e2f5 100644
--- a/vernac/declare.mli
+++ b/vernac/declare.mli
@@ -439,26 +439,21 @@ module ProgramDecl : sig
     -> Names.Id.t list
     -> fixpoint_kind option
     -> Vernacexpr.decl_notation list
-    -> ( Names.Id.t
-       * Constr.types
-       * Evar_kinds.t Loc.located
-       * (bool * Evar_kinds.obligation_definition_status)
-       * Int.Set.t
-       * unit Proofview.tactic option )
-       array
+    -> RetrieveObl.obligation_info
     -> (Constr.constr -> Constr.constr)
     -> t
 
   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
@@ -517,7 +512,6 @@ val obl_substitution :
   -> (Id.t * (Constr.types * Constr.types)) list
 
 val dependencies : Obligation.t array -> int -> Int.Set.t
-val err_not_transp : unit -> unit
 
 (* This is a hack to make it possible for Obligations to craft a Qed
  * behind the scenes.  The fix_exn the Stm attaches to the Future proof
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index bbc20d5e30..a8eac8fd2d 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
@@ -253,27 +251,32 @@ and auto_solve_obligations n ?oblset tac : progress =
 
 open Pp
 
+let show_single_obligation i n obls x =
+  let x = subst_deps_obl obls x in
+  let env = Global.env () in
+  let sigma = Evd.from_env env in
+  let msg =
+    str "Obligation" ++ spc ()
+    ++ int (succ i)
+    ++ spc () ++ str "of" ++ spc () ++ Id.print n ++ str ":" ++ spc ()
+    ++ hov 1 (Printer.pr_constr_env env sigma x.obl_type
+              ++ str "." ++ fnl ()) in
+  Feedback.msg_info msg
+
 let show_obligations_of_prg ?(msg = true) prg =
   let n = prg.prg_name in
   let {obls; remaining} = prg.prg_obligations in
   let showed = ref 5 in
     if msg then Feedback.msg_info (int remaining ++ str " obligation(s) remaining: ");
-    Array.iteri (fun i x ->
-                   match x.obl_body with
-                   | None ->
-                       if !showed > 0 then (
-                         decr showed;
-                         let x = subst_deps_obl obls x in
-                         let env = Global.env () in
-                         let sigma = Evd.from_env env in
-                         Feedback.msg_info
-                           ( str "Obligation" ++ spc ()
-                           ++ int (succ i)
-                           ++ spc () ++ str "of" ++ spc () ++ Id.print n ++ str ":" ++ spc ()
-                           ++ hov 1
-                                ( Printer.pr_constr_env env sigma x.obl_type
-                                ++ str "." ++ fnl () ) ) )
-                   | Some _ -> ())
+    Array.iteri
+      (fun i x ->
+         match x.obl_body with
+         | None ->
+           if !showed > 0 then begin
+             decr showed;
+             show_single_obligation i n obls x
+           end
+         | Some _ -> ())
       obls
 
 let show_obligations ?(msg = true) n =
@@ -372,7 +375,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;