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

---
 interp/notation.ml | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

(limited to 'interp/notation.ml')

diff --git a/interp/notation.ml b/interp/notation.ml
index 6291a88bb0..0afbb9cd62 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -206,7 +206,7 @@ let classify_scope (local,_,_ as o) =
 let inScope : bool * bool * scope_item -> obj =
   declare_object {(default_object "SCOPE") with
       cache_function = cache_scope;
-      open_function = open_scope;
+      open_function = simple_open open_scope;
       subst_function = subst_scope;
       discharge_function = discharge_scope;
       classify_function = classify_scope }
@@ -980,9 +980,12 @@ let subst_prim_token_interpretation (subs,infos) =
 let classify_prim_token_interpretation infos =
     if infos.pt_local then Dispose else Substitute infos
 
+let open_prim_token_interpretation i o =
+  if Int.equal i 1 then cache_prim_token_interpretation o
+
 let inPrimTokenInterp : prim_token_infos -> obj =
   declare_object {(default_object "PRIM-TOKEN-INTERP") with
-     open_function  = (fun i o -> if Int.equal i 1 then cache_prim_token_interpretation o);
+     open_function  = simple_open open_prim_token_interpretation;
      cache_function = cache_prim_token_interpretation;
      subst_function = subst_prim_token_interpretation;
      classify_function = classify_prim_token_interpretation}
-- 
cgit v1.2.3