[obligation] Switch to new declare info API.

5 files changed, 23 insertions, 33 deletions

diff --git a/vernac/classes.ml b/vernac/classes.ml
index 94040a9cef..04321ed844 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -347,8 +347,10 @@ let declare_instance_program env sigma ~global ~poly name pri impargs udecl term
   let uctx = Evd.evar_universe_context sigma in
   let scope, kind = Locality.Global Locality.ImportDefaultBehavior,
                     Decls.IsDefinition Decls.Instance in
+  let cinfo = Declare.CInfo.make ~name ~typ ~impargs () in
+  let info = Declare.Info.make  ~udecl ~scope ~poly ~kind ~hook () in
   let _ : Declare.progress =
-    Obligations.add_definition ~name ~term ~udecl ~scope ~poly ~kind ~hook ~impargs ~uctx typ obls
+    Obligations.add_definition ~cinfo ~info ~term ~uctx obls
   in ()
 
 let declare_instance_open sigma ?hook ~tac ~global ~poly id pri impargs udecl ids term termtype =
diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml
index d5ab9f03be..537f713e82 100644
--- a/vernac/comDefinition.ml
+++ b/vernac/comDefinition.ml
@@ -127,8 +127,10 @@ 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 ~body ~types evd in
+  let term, typ, uctx, obls = Declare.prepare_obligation ~name ~body ~types evd in
   let _ : Declare.progress =
+    let cinfo = Declare.CInfo.make ~name ~typ ~impargs () in
+    let info = Declare.Info.make ~udecl ~scope ~poly ~kind ?hook () in
     Obligations.add_definition
-      ~name ~term ty ~uctx ~udecl ~impargs ~scope ~poly ~kind ?hook obls
+      ~cinfo ~info ~term ~uctx obls
   in ()
diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml
index 87aa5d9b2d..381b6cb9fa 100644
--- a/vernac/comProgramFixpoint.ml
+++ b/vernac/comProgramFixpoint.ml
@@ -260,8 +260,10 @@ let build_wellfounded (recname,pl,bl,arityc,body) poly r measure notation =
     RetrieveObl.retrieve_obligations env recname sigma 0 def typ
   in
   let uctx = Evd.evar_universe_context sigma in
-  ignore(Obligations.add_definition ~name:recname ~term:evars_def ~udecl
-           ~poly evars_typ ~uctx evars ~hook)
+  let cinfo = Declare.CInfo.make ~name:recname ~typ:evars_typ () in
+  let info = Declare.Info.make ~udecl ~poly ~hook () in
+  let _ : Declare.progress = Obligations.add_definition ~cinfo ~info ~term:evars_def ~uctx evars in
+  ()
 
 let out_def = function
   | Some def -> def
@@ -319,7 +321,8 @@ let do_program_recursive ~scope ~poly fixkind fixl =
   | Declare.Obls.IsCoFixpoint -> Decls.(IsDefinition CoFixpoint)
   in
   let ntns = List.map_append (fun { Vernacexpr.notations } -> notations ) fixl in
-  Obligations.add_mutual_definitions defs ~poly ~scope ~kind ~udecl ~uctx ntns fixkind
+  let info = Declare.Info.make ~poly ~scope ~kind ~udecl () in
+  Obligations.add_mutual_definitions defs ~info ~uctx ~ntns fixkind
 
 let do_fixpoint ~scope ~poly l =
   let g = List.map (fun { Vernacexpr.rec_order } -> rec_order) l in
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index 0cce9581a2..6e84d599c5 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -302,16 +302,12 @@ let msg_generating_obl name obls =
        info ++ str ", generating " ++ int len ++
        str (String.plural len " obligation"))
 
-let add_definition ~name ?term t ~uctx ?(udecl = UState.default_univ_decl)
-    ?(impargs = []) ~poly
-    ?(scope = Locality.Global Locality.ImportDefaultBehavior)
-    ?(kind = Decls.(IsDefinition Definition)) ?tactic ?(reduce = reduce) ?hook
-    ?(opaque = false) obls =
+let add_definition ~cinfo ~info ?term ~uctx
+    ?tactic ?(reduce = reduce) ?(opaque = false) obls =
   let prg =
-    let info = Declare.Info.make ~poly ~udecl ~scope ~kind ?hook () in
-    let cinfo = Declare.CInfo.make ~name ~typ:t ~impargs () in
     ProgramDecl.make ~info ~cinfo ~body:term ~opaque ~uctx ~reduce ~ntns:[] ~deps:[] ~fixpoint_kind:None obls
   in
+  let name = Declare.CInfo.get_name cinfo in
   let {obls;_} = Internal.get_obligations prg in
   if Int.equal (Array.length obls) 0 then (
     Flags.if_verbose (msg_generating_obl name) obls;
@@ -327,18 +323,15 @@ let add_definition ~name ?term t ~uctx ?(udecl = UState.default_univ_decl)
       res
     | _ -> res
 
-let add_mutual_definitions l ~uctx ?(udecl = UState.default_univ_decl)
-    ?tactic ~poly ?(scope = Locality.Global Locality.ImportDefaultBehavior)
-    ?(kind = Decls.(IsDefinition Definition)) ?(reduce = reduce) ?hook ?(opaque = false)
-    notations fixkind =
+let add_mutual_definitions l ~info ~uctx
+    ?tactic ?(reduce = reduce) ?(opaque = false) ~ntns fixkind =
   let deps = List.map (fun (ci,_,_) -> Declare.CInfo.get_name ci) l in
   let pm =
     List.fold_left
       (fun () (cinfo, b, obls) ->
-        let info = Declare.Info.make ~poly ~scope ~kind ~udecl ?hook () in
         let prg =
           ProgramDecl.make ~info ~cinfo ~opaque ~body:(Some b) ~uctx ~deps
-            ~fixpoint_kind:(Some fixkind) ~ntns:notations obls ~reduce
+            ~fixpoint_kind:(Some fixkind) ~ntns obls ~reduce
         in
         State.add (Declare.CInfo.get_name cinfo) prg)
       () l
diff --git a/vernac/obligations.mli b/vernac/obligations.mli
index c7ab4a0794..422d187373 100644
--- a/vernac/obligations.mli
+++ b/vernac/obligations.mli
@@ -66,18 +66,12 @@ val default_tactic : unit Proofview.tactic ref
    will return whether all the obligations were solved; if so, it will
    also register [c] with the kernel. *)
 val add_definition :
-     name:Names.Id.t
+     cinfo:types Declare.CInfo.t
+  -> info:Declare.Info.t
   -> ?term:constr
-  -> types
   -> uctx:UState.t
-  -> ?udecl:UState.universe_decl (** Universe binders and constraints *)
-  -> ?impargs:Impargs.manual_implicits
-  -> poly:bool
-  -> ?scope:Locality.locality
-  -> ?kind:Decls.logical_kind
   -> ?tactic:unit Proofview.tactic
   -> ?reduce:(constr -> constr)
-  -> ?hook:Declare.Hook.t
   -> ?opaque:bool
   -> RetrieveObl.obligation_info
   -> Declare.progress
@@ -88,16 +82,12 @@ val add_definition :
    except it takes a list now. *)
 val add_mutual_definitions :
      (Constr.t Declare.CInfo.t * Constr.t * RetrieveObl.obligation_info) list
+  -> info:Declare.Info.t
   -> uctx:UState.t
-  -> ?udecl:UState.universe_decl (** Universe binders and constraints *)
   -> ?tactic:unit Proofview.tactic
-  -> poly:bool
-  -> ?scope:Locality.locality
-  -> ?kind:Decls.logical_kind
   -> ?reduce:(constr -> constr)
-  -> ?hook:Declare.Hook.t
   -> ?opaque:bool
-  -> Vernacexpr.decl_notation list
+  -> ntns:Vernacexpr.decl_notation list
   -> Declare.Obls.fixpoint_kind
   -> unit