aboutsummaryrefslogtreecommitdiffhomepage
path: root/checker/votour.ml
diff options
context:
space:
mode:
Diffstat (limited to 'checker/votour.ml')
-rw-r--r--checker/votour.ml1
1 files changed, 1 insertions, 0 deletions
diff --git a/checker/votour.ml b/checker/votour.ml
index 01965bb4b..bb8e06702 100644
--- a/checker/votour.ml
+++ b/checker/votour.ml
@@ -249,6 +249,7 @@ let visit_vo f =
Printf.printf
"At prompt, <n> enters the <n>-th child, u goes up 1 level, x exits\n\n%!";
let segments = [|
+ 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);