From 24fc879cf2380bb28dd8c0f5ff8c7805ad121e1f Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Thu, 12 Sep 2019 20:49:48 +0200
Subject: Optimize multiple imports

---
 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 1590097731..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_mp |];
+     [| List v_mp |];
      [| v_obj |]
   |])
 
-- 
cgit v1.2.3