aboutsummaryrefslogtreecommitdiff
path: root/stm
diff options
context:
space:
mode:
Diffstat (limited to 'stm')
-rw-r--r--stm/stm.ml6
1 files changed, 3 insertions, 3 deletions
diff --git a/stm/stm.ml b/stm/stm.ml
index a0247e0d8f..4f435f1fa5 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -208,7 +208,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,
- Obligations.program_tcc_summary_tag
+ DeclareObl.program_tcc_summary_tag
type cached_state =
| EmptyState
@@ -884,7 +884,7 @@ end = struct (* {{{ *)
Lemmas.Stack.t option *
int * (* Evarutil.meta_counter_summary_tag *)
int * (* Evd.evar_counter_summary_tag *)
- Obligations.program_info Names.Id.Map.t (* Obligations.program_tcc_summary_tag *)
+ DeclareObl.program_info CEphemeron.key Names.Id.Map.t (* Obligations.program_tcc_summary_tag *)
type partial_state =
[ `Full of Vernacstate.t
@@ -3238,7 +3238,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 Obligations.stm_get_fix_exn (fun () -> !State.fix_exn_ref)
+let () = Hook.set DeclareObl.stm_get_fix_exn (fun () -> !State.fix_exn_ref)
type document = VCS.vcs
let backup () = VCS.backup ()