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.
---
 stm/stm.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'stm')

diff --git a/stm/stm.ml b/stm/stm.ml
index aa5a14c7dd..177a76e64b 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -202,7 +202,7 @@ let mkTransCmd cast cids ceff cqueue =
 (* Parts of the system state that are morally part of the proof state *)
 let summary_pstate = Evarutil.meta_counter_summary_tag,
                      Evd.evar_counter_summary_tag,
-                     DeclareObl.State.prg_tag
+                     Declare.Obls.State.prg_tag
 
 type cached_state =
   | EmptyState
@@ -878,7 +878,7 @@ end = struct (* {{{ *)
     Vernacstate.LemmaStack.t option *
     int *                                   (* Evarutil.meta_counter_summary_tag *)
     int *                                   (* Evd.evar_counter_summary_tag *)
-    DeclareObl.State.t
+    Declare.Obls.State.t
 
   type partial_state =
     [ `Full of Vernacstate.t
@@ -3308,7 +3308,7 @@ let unreachable_state_hook = Hooks.unreachable_state_hook
 let document_add_hook = Hooks.document_add_hook
 let document_edit_hook = Hooks.document_edit_hook
 let sentence_exec_hook = Hooks.sentence_exec_hook
-let () = Hook.set DeclareObl.stm_get_fix_exn (fun () -> !State.fix_exn_ref)
+let () = Declare.Obls.stm_get_fix_exn := (fun () -> !State.fix_exn_ref)
 
 type document = VCS.vcs
 let backup () = VCS.backup ()
-- 
cgit v1.2.3