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/comDefinition.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'vernac/comDefinition.ml')

diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml
index 95f3955309..eac8f92e2e 100644
--- a/vernac/comDefinition.ml
+++ b/vernac/comDefinition.ml
@@ -127,7 +127,7 @@ let do_definition_program ?hook ~name ~scope ~poly ~kind udecl bl red_option c c
     interp_definition ~program_mode udecl bl ~poly red_option c ctypopt
   in
   let term, ty, uctx, obls = Declare.prepare_obligation ~name ~poly ~body ~types ~udecl evd in
-  let _ : DeclareObl.progress =
+  let _ : Declare.Obls.progress =
     Obligations.add_definition
       ~name ~term ty ~uctx ~udecl ~impargs ~scope ~poly ~kind ?hook obls
   in ()
-- 
cgit v1.2.3