aboutsummaryrefslogtreecommitdiff
path: root/vernac/classes.ml
diff options
context:
space:
mode:
authorGaëtan Gilbert2020-02-24 14:24:10 +0100
committerGaëtan Gilbert2020-04-13 15:18:18 +0200
commitb98ef72ee300e52dd2c67f03da358e3c2102cdbb (patch)
treeceddc2c4523978cfa0436047b44f3f326eeba106 /vernac/classes.ml
parent2d6b7d5997037d9a94524a733867f64cd34e851c (diff)
pass filters around
Diffstat (limited to 'vernac/classes.ml')
-rw-r--r--vernac/classes.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/vernac/classes.ml b/vernac/classes.ml
index 3d38713e09..a9425b15d2 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -116,7 +116,7 @@ let instance_input : instance -> obj =
{ (default_object "type classes instances state") with
cache_function = cache_instance;
load_function = (fun _ x -> cache_instance x);
- open_function = (fun _ x -> cache_instance x);
+ open_function = simple_open (fun _ x -> cache_instance x);
classify_function = classify_instance;
discharge_function = discharge_instance;
rebuild_function = rebuild_instance;
@@ -237,7 +237,7 @@ let class_input : typeclass -> obj =
{ (default_object "type classes state") with
cache_function = cache_class;
load_function = (fun _ -> cache_class);
- open_function = (fun _ -> cache_class);
+ open_function = simple_open (fun _ -> cache_class);
classify_function = (fun x -> Substitute x);
discharge_function = (fun a -> Some (discharge_class a));
rebuild_function = rebuild_class;