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/values.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/values.ml')
| -rw-r--r-- | checker/values.ml | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/checker/values.ml b/checker/values.ml index cf93466b0..b2d74821d 100644 --- a/checker/values.ml +++ b/checker/values.ml @@ -13,7 +13,7 @@ To ensure this file is up-to-date, 'make' now compares the md5 of cic.mli with a copy we maintain here: -MD5 0a174243f8b06535c9eecbbe8d339fe1 checker/cic.mli +MD5 f5fd749af797e08efee22122742bc740 checker/cic.mli *) @@ -350,8 +350,11 @@ let v_stm_seg = v_pair v_tasks v_counters (** Toplevel structures in a vo (see Cic.mli) *) +let v_libsum = + Tuple ("summary", [|v_dp;Array v_dp;v_deps|]) + let v_lib = - Tuple ("library",[|v_dp;v_compiled_lib;v_libraryobjs;v_deps;Array v_dp|]) + Tuple ("library",[|v_compiled_lib;v_libraryobjs|]) let v_opaques = Array (v_computation v_constr) let v_univopaques = |