aboutsummaryrefslogtreecommitdiff
path: root/checker
diff options
context:
space:
mode:
Diffstat (limited to 'checker')
-rw-r--r--checker/values.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/checker/values.ml b/checker/values.ml
index 38cb243f80..4e99d087df 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -374,7 +374,7 @@ and v_modtype =
let v_vodigest = Sum ("module_impl",0, [| [|String|]; [|String;String|] |])
let v_deps = Array (v_tuple "dep" [|v_dp;v_vodigest|])
let v_compiled_lib =
- v_tuple "compiled" [|v_dp;v_module;v_context_set;v_deps;v_engagement;Any|]
+ v_tuple "compiled" [|v_dp;v_module;v_context_set;v_deps;v_engagement|]
(** Library objects *)