From c8b54d74bc7cf29cc04d0a3cedbf4a106f6e744c Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 4 May 2020 11:18:34 +0200
Subject: [declare] Merge `DeclareObl` into `Declare`

This is needed as a first step to refactor and unify the obligation
save path and state; in particular `Equations` is a heavy user of
Hooks to modify obligations state, thus in order to make the hook
aware of this we need to place the obligation state before the hook.

As a good side-effect, `inline_private_constants` and `Hook.call` are
not exported from `Declare` anymore.
---
 vernac/comProgramFixpoint.ml | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

(limited to 'vernac/comProgramFixpoint.ml')

diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml
index 4e9e24b119..4aa46e0a86 100644
--- a/vernac/comProgramFixpoint.ml
+++ b/vernac/comProgramFixpoint.ml
@@ -273,7 +273,7 @@ let collect_evars_of_term evd c ty =
   evars (Evd.from_ctx (Evd.evar_universe_context evd))
 
 let do_program_recursive ~scope ~poly fixkind fixl =
-  let cofix = fixkind = DeclareObl.IsCoFixpoint in
+  let cofix = fixkind = Declare.Obls.IsCoFixpoint in
   let (env, rec_sign, udecl, evd), fix, info =
     interp_recursive ~cofix ~program_mode:true fixl
   in
@@ -314,8 +314,8 @@ let do_program_recursive ~scope ~poly fixkind fixl =
   end in
   let uctx = Evd.evar_universe_context evd in
   let kind = match fixkind with
-  | DeclareObl.IsFixpoint _ -> Decls.Fixpoint
-  | DeclareObl.IsCoFixpoint -> Decls.CoFixpoint
+  | Declare.Obls.IsFixpoint _ -> Decls.Fixpoint
+  | Declare.Obls.IsCoFixpoint -> Decls.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
@@ -345,7 +345,7 @@ let do_fixpoint ~scope ~poly l =
     | _, _ when List.for_all (fun ro -> match ro with None | Some { CAst.v = CStructRec _} -> true | _ -> false) g ->
       let annots = List.map (fun fix ->
           Vernacexpr.(ComFixpoint.adjust_rec_order ~structonly:true fix.binders fix.rec_order)) l in
-      let fixkind = DeclareObl.IsFixpoint annots in
+      let fixkind = Declare.Obls.IsFixpoint annots in
       let l = List.map2 (fun fix rec_order -> { fix with Vernacexpr.rec_order }) l annots in
       do_program_recursive ~scope ~poly fixkind l
 
@@ -355,4 +355,4 @@ let do_fixpoint ~scope ~poly l =
 
 let do_cofixpoint ~scope ~poly fixl =
   let fixl = List.map (fun fix -> { fix with Vernacexpr.rec_order = None }) fixl in
-  do_program_recursive ~scope ~poly DeclareObl.IsCoFixpoint fixl
+  do_program_recursive ~scope ~poly Declare.Obls.IsCoFixpoint fixl
-- 
cgit v1.2.3