diff options
| author | Emilio Jesus Gallego Arias | 2020-03-07 04:25:40 -0500 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-03-19 17:18:55 -0400 |
| commit | e2e4912212c5f6ab94eaded61e53b0478f9b17c8 (patch) | |
| tree | 4e22ed0bf4a8bc60ffd5f58c71fff65a70ad6560 /stm | |
| parent | 1db28d6844cc993daacc0797ac7d537d2f4172dd (diff) | |
[obligations] More progress towards unification of the save path
We make internal types `private` as an step towards the unification of
the save path with the rest of the system.
In particular, this is allow us to guarantee invariants
w.r.t. external users as the large majority of fields are always
constant.
This will also enable at some point a common creation of proof entry
with the rest of the system.
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/stm.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/stm/stm.ml b/stm/stm.ml index 73356c42f1..62556d38ff 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -878,7 +878,7 @@ end = struct (* {{{ *) Vernacstate.LemmaStack.t option * int * (* Evarutil.meta_counter_summary_tag *) int * (* Evd.evar_counter_summary_tag *) - DeclareObl.program_info CEphemeron.key Names.Id.Map.t (* Obligations.program_tcc_summary_tag *) + DeclareObl.ProgramDecl.t CEphemeron.key Names.Id.Map.t (* Obligations.program_tcc_summary_tag *) type partial_state = [ `Full of Vernacstate.t |