Separate checking univ_decls and obtaining universe binder names.

1 files changed, 4 insertions, 4 deletions

diff --git a/vernac/classes.ml b/vernac/classes.ml
index ed37bab6d..6f5f96ee2 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -119,14 +119,14 @@ let declare_instance_constant k info global imps ?hook id decl poly evm term ter
 				 (Univops.universes_of_constr term) in
     Evd.restrict_universe_context evm levels 
   in
-  let pl, uctx = Evd.check_univ_decl evm decl in
+  let uctx = Evd.check_univ_decl evm decl in
   let entry = 
     Declare.definition_entry ~types:termtype ~poly ~univs:uctx term
   in
   let cdecl = (DefinitionEntry entry, kind) in
   let kn = Declare.declare_constant id cdecl in
     Declare.definition_message id;
-    Universes.register_universe_binders (ConstRef kn) pl;
+    Universes.register_universe_binders (ConstRef kn) (Evd.universe_binders evm);
     instance_hook k info global imps ?hook (ConstRef kn);
     id
 
@@ -203,12 +203,12 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance)
 	    nf t
 	in
 	Pretyping.check_evars env Evd.empty !evars (EConstr.of_constr termtype);
-	let pl, ctx = Evd.check_univ_decl !evars decl in
+        let ctx = Evd.check_univ_decl !evars decl in
 	let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest id
 	  (ParameterEntry 
             (None,poly,(termtype,ctx),None), Decl_kinds.IsAssumption Decl_kinds.Logical)
 	in
-	  Universes.register_universe_binders (ConstRef cst) pl;
+          Universes.register_universe_binders (ConstRef cst) (Evd.universe_binders !evars);
 	  instance_hook k pri global imps ?hook (ConstRef cst); id
       end
     else (