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

---
 plugins/ltac/tacenv.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/ltac/tacenv.ml')

diff --git a/plugins/ltac/tacenv.ml b/plugins/ltac/tacenv.ml
index ce9189792e..76d47f5482 100644
--- a/plugins/ltac/tacenv.ml
+++ b/plugins/ltac/tacenv.ml
@@ -182,7 +182,7 @@ let inMD : bool * ltac_constant option * bool * glob_tactic_expr *
   declare_object {(default_object "TAC-DEFINITION") with
      cache_function  = cache_md;
      load_function   = load_md;
-     open_function   = open_md;
+     open_function   = simple_open open_md;
      subst_function = subst_md;
      classify_function = classify_md}
 
-- 
cgit v1.2.3