Merge PR #9645: [proof] Remove terminator type, unifying regular and obligation ones.

Ack-by: ejgallego
Ack-by: gares
Reviewed-by: ppedrot

1 files changed, 6 insertions, 6 deletions

diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml
index 563758df25..23c98c97f9 100644
--- a/vernac/comProgramFixpoint.ml
+++ b/vernac/comProgramFixpoint.ml
@@ -229,7 +229,7 @@ let build_wellfounded (recname,pl,bl,arityc,body) poly r measure notation =
       in hook, recname, typ
   in
   (* XXX: Capturing sigma here... bad bad *)
-  let hook = Lemmas.mk_hook (hook sigma) in
+  let hook = DeclareDef.Hook.make (hook sigma) in
   Obligations.check_evars env sigma;
   let evars, _, evars_def, evars_typ =
     Obligations.eterm_obligations env recname sigma 0 def typ
@@ -248,7 +248,7 @@ let collect_evars_of_term evd c ty =
   evars (Evd.from_ctx (Evd.evar_universe_context evd))
 
 let do_program_recursive local poly fixkind fixl ntns =
-  let cofix = fixkind = Obligations.IsCoFixpoint in
+  let cofix = fixkind = DeclareObl.IsCoFixpoint in
   let (env, rec_sign, pl, evd), fix, info =
     interp_recursive ~cofix ~program_mode:true fixl ntns
   in
@@ -289,8 +289,8 @@ let do_program_recursive local poly fixkind fixl ntns =
   end in
   let ctx = Evd.evar_universe_context evd in
   let kind = match fixkind with
-  | Obligations.IsFixpoint _ -> (local, poly, Fixpoint)
-  | Obligations.IsCoFixpoint -> (local, poly, CoFixpoint)
+  | DeclareObl.IsFixpoint _ -> (local, poly, Fixpoint)
+  | DeclareObl.IsCoFixpoint -> (local, poly, CoFixpoint)
   in
   Obligations.add_mutual_definitions defs ~kind ~univdecl:pl ctx ntns fixkind
 
@@ -316,7 +316,7 @@ let do_program_fixpoint local poly l =
 
     | _, _ when List.for_all (fun ro -> match ro with None | Some { CAst.v = CStructRec _} -> true | _ -> false) g ->
         let fixl,ntns = extract_fixpoint_components ~structonly:true l in
-        let fixkind = Obligations.IsFixpoint (List.map (fun d -> d.fix_annot) fixl) in
+        let fixkind = DeclareObl.IsFixpoint (List.map (fun d -> d.fix_annot) fixl) in
           do_program_recursive local poly fixkind fixl ntns
 
     | _, _ ->
@@ -341,5 +341,5 @@ let do_fixpoint local poly l =
 
 let do_cofixpoint local poly l =
   let fixl,ntns = extract_cofixpoint_components l in
-  do_program_recursive local poly Obligations.IsCoFixpoint fixl ntns;
+  do_program_recursive local poly DeclareObl.IsCoFixpoint fixl ntns;
   if not (check_safe ()) then Feedback.feedback Feedback.AddedAxiom else ()