diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-03-16 09:24:00 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-03-25 15:38:34 +0100 |
| commit | 578d73a8b8eb6623bfa688c1e3ed9d1442bd435f (patch) | |
| tree | 6c67b6999002c00b23d06fd9bb4563afdbe75eb0 /checker/votour.ml | |
| parent | c1729637d4fe32ebe0268eb338fcf4d032bb5df7 (diff) | |
Exporting memory representation of STM tasks for votour.
Diffstat (limited to 'checker/votour.ml')
| -rw-r--r-- | checker/votour.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/checker/votour.ml b/checker/votour.ml index 2db92853a..7c954d6f9 100644 --- a/checker/votour.ml +++ b/checker/votour.ml @@ -219,7 +219,7 @@ let visit_vo f = {name="library"; pos=0; typ=Values.v_lib}; {name="univ constraints of opaque proofs"; pos=0;typ=Values.v_univopaques}; {name="discharging info"; pos=0; typ=Opt Any}; - {name="STM tasks"; pos=0; typ=Opt Any}; + {name="STM tasks"; pos=0; typ=Opt Values.v_stm_seg}; {name="opaque proofs"; pos=0; typ=Values.v_opaques}; |] in while true do |