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

(limited to 'vernac/classes.ml')

diff --git a/vernac/classes.ml b/vernac/classes.ml
index 55af2e1a7d..21e2afe6a9 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -345,7 +345,7 @@ let declare_instance_program env sigma ~global ~poly name pri impargs udecl term
   let hook = Declare.Hook.make hook in
   let uctx = Evd.evar_universe_context sigma in
   let scope, kind = Declare.Global Declare.ImportDefaultBehavior, Decls.Instance in
-  let _ : DeclareObl.progress =
+  let _ : Declare.Obls.progress =
     Obligations.add_definition ~name ~term ~udecl ~scope ~poly ~kind ~hook ~impargs ~uctx typ obls
   in ()
 
-- 
cgit v1.2.3