From b98ef72ee300e52dd2c67f03da358e3c2102cdbb Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Mon, 24 Feb 2020 14:24:10 +0100
Subject: pass filters around

---
 checker/values.ml | 13 ++++++++++++-
 1 file changed, 12 insertions(+), 1 deletion(-)

(limited to 'checker')

diff --git a/checker/values.ml b/checker/values.ml
index 12f7135cdf..b9efce6948 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -372,6 +372,17 @@ let v_compiled_lib =
 
 let v_obj = Dyn
 
+let v_globref = Sum("globref",0,[|
+    [|v_id|];
+    [|v_cst|];
+    [|v_ind|];
+    [|v_cons|]
+  |])
+
+let v_ext_gref = Sum("extended_global_reference",0,[|[|v_globref|];[|v_kn|]|])
+
+let v_open_filter = Sum ("open_filter",1,[|[|v_hset v_ext_gref|]|])
+
 let rec v_aobjs = Sum("algebraic_objects", 0,
   [| [|v_libobjs|];
      [|v_mp;v_subst|]
@@ -383,7 +394,7 @@ and v_libobjt = Sum("Libobject.t",0,
      [| v_substobjs |];
      [| v_aobjs |];
      [| v_libobjs |];
-     [| List v_mp |];
+     [| List (v_pair v_open_filter v_mp)|];
      [| v_obj |]
   |])
 
-- 
cgit v1.2.3