aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--toplevel/classes.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 898ef0d9e..0a83c49c8 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -198,7 +198,7 @@ let new_instance ?(abstract=false) ?(global=false) poly ctx (instid, bk, cl) pro
(None,poly,(termtype,ctx),None), Decl_kinds.IsAssumption Decl_kinds.Logical)
in
Universes.register_universe_binders (ConstRef cst) pl;
- instance_hook k None global imps ?hook (ConstRef cst); id
+ instance_hook k pri global imps ?hook (ConstRef cst); id
end
else (
let props =