diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-11-29 01:42:21 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-12-09 18:17:50 +0100 |
| commit | 5676b113920fb48d4898817d6c0ce3353b06107f (patch) | |
| tree | 71dbe3f412ec441fd72dbf02a70ce9bb3e9a06c7 /vernac/obligations.ml | |
| parent | 8c9166435d6926babf697c3f575a8653f465cc76 (diff) | |
[summary] Adapt STM to the new Summary API.
We need to a partial restore. I think that we could design a better
API, but further work on the toplevel state should improve it
progressively.
Diffstat (limited to 'vernac/obligations.ml')
| -rw-r--r-- | vernac/obligations.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/vernac/obligations.ml b/vernac/obligations.ml index 24d664951..bdae27e5b 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -429,8 +429,8 @@ let map_replace k v m = ProgMap.add k (CEphemeron.create v) (ProgMap.remove k m) let map_keys m = ProgMap.fold (fun k _ l -> k :: l) m [] -let from_prg : program_info ProgMap.t ref = - Summary.ref ProgMap.empty ~name:"program-tcc-table" +let from_prg, program_tcc_summary_tag = + Summary.ref_tag ProgMap.empty ~name:"program-tcc-table" let close sec = if not (ProgMap.is_empty !from_prg) then |