diff options
| author | Pierre-Marie Pédrot | 2019-09-26 17:02:26 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-10-04 18:00:26 +0200 |
| commit | 69551b566a1339543967a41ff4aaa4580e7394fc (patch) | |
| tree | 4b60e8a6bb3c25c029e43fd40fd56e5839db6e68 /checker/votour.ml | |
| parent | d5f2e13e51c3404d326f04513a50d264790a7a4c (diff) | |
Merge Direct and Indirect nodes in Opaqueproof.
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 f0e0cf22ab..5a610e6938 100644 --- a/checker/votour.ml +++ b/checker/votour.ml @@ -366,7 +366,7 @@ let visit_vo f = make_seg "univ constraints of opaque proofs" Values.v_univopaques; make_seg "discharging info" (Opt Any); make_seg "STM tasks" (Opt Values.v_stm_seg); - make_seg "opaque proofs" Values.v_opaques; + make_seg "opaque proofs" Values.v_opaquetable; |] in let repr = if Sys.word_size = 64 then (module ReprMem : S) else (module ReprObj : S) |