From 1b984a697076aae9bbdb96efbecbbbec274cbf2a Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Mon, 14 Mar 2016 11:14:44 +0100
Subject: Typeclasses: respect Declare Instance priority

---
 toplevel/classes.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 898ef0d9e1..0a83c49c8d 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 =
-- 
cgit v1.2.3