aboutsummaryrefslogtreecommitdiff
path: root/checker/values.ml
diff options
context:
space:
mode:
Diffstat (limited to 'checker/values.ml')
-rw-r--r--checker/values.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/checker/values.ml b/checker/values.ml
index 76e3ab0d45..cce0ce7203 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -435,7 +435,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;v_deps|])
+ Tuple ("summary", [|v_dp;v_deps;String|])
let v_lib =
Tuple ("library",[|v_compiled_lib;v_libraryobjs|])