4 files changed, 7 insertions, 9 deletions
diff --git a/contrib/subtac/subtac.ml b/contrib/subtac/subtac.ml
index e9c2ed4e52..2d1be640b1 100644
--- a/contrib/subtac/subtac.ml
+++ b/contrib/subtac/subtac.ml
@@ -148,8 +148,8 @@ let subtac (loc, command) =
       | VernacAssumption (stre,nl,l) -> 
 	  vernac_assumption env isevars stre l nl
 
-      | VernacInstance (sup, is, props) ->
-	  ignore(Subtac_classes.new_instance sup is props)
+      | VernacInstance (sup, is, props, pri) ->
+	  ignore(Subtac_classes.new_instance sup is props pri)
 
       | VernacCoFixpoint (l, b) ->
 	  let _ = trace (str "Building cofixpoint") in
diff --git a/contrib/subtac/subtac_classes.ml b/contrib/subtac/subtac_classes.ml
index e439021635..a2184a557e 100644
--- a/contrib/subtac/subtac_classes.ml
+++ b/contrib/subtac/subtac_classes.ml
@@ -100,7 +100,7 @@ let type_class_instance_params isevars env id n ctx inst subst =
 let substitution_of_constrs ctx cstrs =
   List.fold_right2 (fun c (na, _, _) acc -> (na, c) :: acc) cstrs ctx []
 
-let new_instance ctx (instid, bk, cl) props =
+let new_instance ctx (instid, bk, cl) props pri =
   let env = Global.env() in
   let isevars = ref (Evd.create_evar_defs Evd.empty) in
   let bound = Implicit_quantifiers.ids_of_list (Termops.ids_of_context env) in
@@ -211,11 +211,10 @@ let new_instance ctx (instid, bk, cl) props =
   let hook cst = 
     let inst = 
       { is_class = k;
-	is_name = id;
+	is_pri = pri;
 	is_impl = cst;
       }
     in
-      Classes.add_instance_hint id;
       Impargs.declare_manual_implicits false (ConstRef cst) false imps;
       Typeclasses.add_instance inst
   in
diff --git a/contrib/subtac/subtac_classes.mli b/contrib/subtac/subtac_classes.mli
index 12a6e29549..c621f1516f 100644
--- a/contrib/subtac/subtac_classes.mli
+++ b/contrib/subtac/subtac_classes.mli
@@ -36,4 +36,5 @@ val new_instance :
   Topconstr.local_binder list ->
   typeclass_constraint ->
   binder_def_list ->
+  int option ->
   identifier
diff --git a/contrib/subtac/subtac_pretyping_F.ml b/contrib/subtac/subtac_pretyping_F.ml
index 5bcbf4db6c..730b12605e 100644
--- a/contrib/subtac/subtac_pretyping_F.ml
+++ b/contrib/subtac/subtac_pretyping_F.ml
@@ -572,11 +572,9 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
       | IsType ->
 	  (pretype_type empty_valcon env isevars lvar c).utj_val in
     let evd,_ = consider_remaining_unif_problems env !isevars in
-    let evd = nf_evar_defs evd in
     let evd = Typeclasses.resolve_typeclasses ~onlyargs:true ~all:false env (evars_of evd) evd in
-    let c' = nf_evar (evars_of evd) c' in
-      isevars := evd;
-      c'
+      isevars:=evd;
+      nf_evar (evars_of !isevars) c'
 
   (* TODO: comment faire remonter l'information si le typage a resolu des
      variables du sigma original. il faudrait que la fonction de typage