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/syntax_def.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'interp/syntax_def.ml')

diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml
index 767c69e3b6..d6aa527f4d 100644
--- a/interp/syntax_def.ml
+++ b/interp/syntax_def.ml
@@ -71,7 +71,7 @@ let in_syntax_constant : (bool * syndef) -> obj =
   declare_object {(default_object "SYNDEF") with
     cache_function = cache_syntax_constant;
     load_function = load_syntax_constant;
-    open_function = open_syntax_constant;
+    open_function = todo_filter open_syntax_constant;
     subst_function = subst_syntax_constant;
     classify_function = classify_syntax_constant }
 
-- 
cgit v1.2.3