From 06159c53e84ab1cff0299890767576972eaf83c2 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Tue, 23 Jun 2020 22:18:23 +0200
Subject: [obligation] Switch to new declare info API.

---
 vernac/comProgramFixpoint.ml | 9 ++++++---
 1 file changed, 6 insertions(+), 3 deletions(-)

(limited to 'vernac/comProgramFixpoint.ml')

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
-- 
cgit v1.2.3