diff options
| author | Pierre-Marie Pédrot | 2019-10-08 22:00:55 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2019-10-18 11:17:27 +0200 |
| commit | 3e5a44e099d3fe847693887a09b57dfb4e2349e8 (patch) | |
| tree | 2b86845824b2fe01ed197df6d77368cac8633e0d | |
| parent | cc9856e33fa1a15fe699e8d9cd7b76086563683d (diff) | |
Fix votour after the change of representation of opaques.
| -rw-r--r-- | checker/votour.ml | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/checker/votour.ml b/checker/votour.ml index 5a610e6938..97584831e5 100644 --- a/checker/votour.ml +++ b/checker/votour.ml @@ -364,7 +364,6 @@ let visit_vo f = make_seg "summary" Values.v_libsum; make_seg "library" Values.v_lib; 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_opaquetable; |] in |