aboutsummaryrefslogtreecommitdiff
path: root/checker/values.ml
diff options
context:
space:
mode:
Diffstat (limited to 'checker/values.ml')
-rw-r--r--checker/values.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/checker/values.ml b/checker/values.ml
index cc9ac1f834..6b340635d7 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -357,7 +357,7 @@ and v_libobjt = Sum("Libobject.t",0,
[| v_substobjs |];
[| v_aobjs |];
[| v_libobjs |];
- [| v_bool; v_mp |];
+ [| List v_mp |];
[| v_obj |]
|])
@@ -395,7 +395,7 @@ 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|])
+ Tuple ("summary", [|v_dp;v_deps|])
let v_lib =
Tuple ("library",[|v_compiled_lib;v_libraryobjs|])