From 4614010ceddb9ed5100fa4e43d2807b172143a19 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Mon, 8 Jul 2019 15:00:36 +0200
Subject: Specialize `ImportObject` to `Export`

`Import` does not actually need to register an object, only `Export`
does. So we specialize and rename the object into `ExportObject`.
---
 checker/values.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'checker')

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 |]
   |])
 
-- 
cgit v1.2.3