[proof] Unify obligation proof save path: Part I, declareObl

We move obligation declaration-specific functions to their own
file. This way, `Lemmas` can access them, and in the next part we can
factorize common parts in the save proof.

1 files changed, 5 insertions, 5 deletions

diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml
index 69e2a209eb..6296347fd0 100644
--- a/vernac/comProgramFixpoint.ml
+++ b/vernac/comProgramFixpoint.ml
@@ -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 ()