diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-03-17 10:21:41 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-06-24 00:13:17 +0200 |
| commit | e2e88741120332f9e97459852d7361e2d8939881 (patch) | |
| tree | 9674a8785e31974fb73b96b840014d86d5e14b1b /checker/votour.ml | |
| parent | a2fa3dd1ec96cd70c817ff375d7b857924bb9825 (diff) | |
Splitting the library representation on disk in two.
The first part only contains the summary of the library, while the second
one contains the effective content of it.
Diffstat (limited to 'checker/votour.ml')
| -rw-r--r-- | checker/votour.ml | 1 |
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); |