diff options
| author | Gaëtan Gilbert | 2020-02-24 14:24:10 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-04-13 15:18:18 +0200 |
| commit | b98ef72ee300e52dd2c67f03da358e3c2102cdbb (patch) | |
| tree | ceddc2c4523978cfa0436047b44f3f326eeba106 /checker | |
| parent | 2d6b7d5997037d9a94524a733867f64cd34e851c (diff) | |
pass filters around
Diffstat (limited to 'checker')
| -rw-r--r-- | checker/values.ml | 13 |
1 files changed, 12 insertions, 1 deletions
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 |] |]) |