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 708419e7cc..1590097731 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 |];
+ [| v_mp |];
[| v_obj |]
|])