diff options
| author | Emilio Jesus Gallego Arias | 2019-02-24 02:24:47 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-06-17 12:30:13 +0200 |
| commit | a296e879112f2e88b2fdfbf2fe90f1807f90b890 (patch) | |
| tree | 8a0bd991117086222175377bb01ee2a70b904258 /stm | |
| parent | a2ea73d84be2fe95eeda42f5f5ac458f0af9968f (diff) | |
[proof] Unify obligation proof save path: Part I, declareObl
We move obligation declaration-specific functions to their own
file. This way, `Lemmas` can access them, and in the next part we can
factorize common parts in the save proof.
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/stm.ml | 6 |
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 () |