diff options
| author | Emilio Jesus Gallego Arias | 2020-03-15 17:52:16 -0400 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-05-18 19:08:13 +0200 |
| commit | 809291d5ef7371bfe8841b95126c0332da55578f (patch) | |
| tree | 6090e1df72a333a2b57ad21a147127da6228968d /stm | |
| parent | 2222e455f0501b700f198ab614d8743229062f73 (diff) | |
[obligations] Pre-functionalize Program state
In our quest to unify all the declaration paths, an important step
is to account for the state pertaining to `Program` declarations.
Whereas regular proofs keep are kept in a stack-like structure;
obligations for constants defined by `Program` are stored in a global
map which is manipulated by almost regular open/close proof primitives.
This PR is in preparation for the switch to a purely functional state
in #11836 ; the full switch requires deeper changes so it is helpful
to have this PR preparing most of the structure.
Most of the PR is routine; only remarkable change is that the hook for
admitted obligations is now called explicitly in `finish_admitted` as
it had to learn about the different types of proof_endings. Before,
obligations set it in `start_lemma` but only used in the `Admitted`
path.
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/stm.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/stm/stm.ml b/stm/stm.ml index b296f8f08f..aa5a14c7dd 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.program_tcc_summary_tag + DeclareObl.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.ProgramDecl.t CEphemeron.key Names.Id.Map.t (* Obligations.program_tcc_summary_tag *) + DeclareObl.State.t type partial_state = [ `Full of Vernacstate.t |