aboutsummaryrefslogtreecommitdiff
path: root/vernac/classes.ml
diff options
context:
space:
mode:
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 a411300b54..eb735b7cdf 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;