Merge branch 'master'.

13 files changed, 122 insertions, 99 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 490bc2801..38c105666 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -279,9 +279,9 @@ let rec find_row_ind = function
 let inductive_template evdref env tmloc ind =
   let indu = evd_comb1 (Evd.fresh_inductive_instance env) evdref ind in
   let arsign = inductive_alldecls_env env indu in
-  let hole_source = match tmloc with
-    | Some loc -> fun i -> (loc, Evar_kinds.TomatchTypeParameter (ind,i))
-    | None -> fun _ -> (Loc.ghost, Evar_kinds.InternalHole) in
+  let hole_source i = match tmloc with
+    | Some loc -> (loc, Evar_kinds.TomatchTypeParameter (ind,i))
+    | None -> (Loc.ghost, Evar_kinds.TomatchTypeParameter (ind,i)) in
    let (_,evarl,_) =
     List.fold_right
       (fun decl (subst,evarl,n) ->
@@ -855,7 +855,7 @@ let subst_predicate (subst,copt) ccl tms =
     | Some c -> c::subst in
   substnl_predicate sigma 0 ccl tms
 
-let specialize_predicate_var (cur,typ,dep) tms ccl =
+let specialize_predicate_var (cur,typ,dep) env tms ccl =
   let c = match dep with
   | Anonymous -> None
   | Name _ -> Some cur
@@ -863,7 +863,10 @@ let specialize_predicate_var (cur,typ,dep) tms ccl =
   let l =
     match typ with
     | IsInd (_, IndType (_, _), []) -> []
-    | IsInd (_, IndType (_, realargs), names) -> realargs
+    | IsInd (_, IndType (indf, realargs), names) ->
+       let arsign,_ = get_arity env indf in
+       let arsign = List.map EConstr.of_rel_decl arsign in
+       subst_of_rel_context_instance arsign realargs
     | NotInd _ -> [] in
   subst_predicate (l,c) ccl tms
 
@@ -1403,7 +1406,7 @@ and match_current pb (initial,tomatch) =
 and shift_problem ((current,t),_,na) pb =
   let ty = type_of_tomatch t in
   let tomatch = lift_tomatch_stack 1 pb.tomatch in
-  let pred = specialize_predicate_var (current,t,na) pb.tomatch pb.pred in
+  let pred = specialize_predicate_var (current,t,na) pb.env pb.tomatch pb.pred in
   let pb =
     { pb with
        env = push_rel (LocalDef (na,current,ty)) pb.env;
@@ -1420,7 +1423,7 @@ and shift_problem ((current,t),_,na) pb =
    are already introduced in the context, we avoid creating aliases to
    themselves by treating this case specially. *)
 and pop_problem ((current,t),_,na) pb =
-  let pred = specialize_predicate_var (current,t,na) pb.tomatch pb.pred in
+  let pred = specialize_predicate_var (current,t,na) pb.env pb.tomatch pb.pred in
   let pb =
     { pb with
        pred = pred;
@@ -1963,14 +1966,22 @@ let noccur_with_meta sigma n m term =
   try (occur_rec n term; true) with LocalOccur -> false
 
 let prepare_predicate loc typing_fun env sigma tomatchs arsign tycon pred =
+  let refresh_tycon sigma t =
+    (** If we put the typing constraint in the term, it has to be
+       refreshed to preserve the invariant that no algebraic universe
+       can appear in the term.  *)
+    refresh_universes ~status:Evd.univ_flexible ~onlyalg:true (Some true)
+		      env sigma t
+  in
   let preds =
     match pred, tycon with
     (* No return clause *)
     | None, Some t when not (noccur_with_meta sigma 0 max_int t) ->
 	(* If the tycon is not closed w.r.t real variables, we try *)
         (* two different strategies *)
-	(* First strategy: we abstract the tycon wrt to the dependencies *)
-        let p1 =
+       (* First strategy: we abstract the tycon wrt to the dependencies *)
+         let sigma, t = refresh_tycon sigma t in
+         let p1 =
           prepare_predicate_from_arsign_tycon env sigma loc tomatchs arsign t in
 	(* Second strategy: we build an "inversion" predicate *)
 	let sigma2,pred2 = build_inversion_problem loc env sigma tomatchs t in
@@ -1981,7 +1992,7 @@ let prepare_predicate loc typing_fun env sigma tomatchs arsign tycon pred =
 	(* No dependent type constraint, or no constraints at all: *)
 	(* we use two strategies *)
         let sigma,t = match tycon with
-	| Some t -> sigma,t
+	| Some t -> refresh_tycon sigma t
 	| None -> 
           let sigma = Sigma.Unsafe.of_evar_map sigma in
           let Sigma ((t, _), sigma, _) =
diff --git a/pretyping/cases.mli b/pretyping/cases.mli
index 3df2d6873..6c2b5bf68 100644
--- a/pretyping/cases.mli
+++ b/pretyping/cases.mli
@@ -115,10 +115,10 @@ val compile : 'a pattern_matching_problem -> unsafe_judgment
 
 val prepare_predicate :            Loc.t ->
            (Evarutil.type_constraint ->
-            Environ.env -> Evd.evar_map ref -> 'a -> unsafe_judgment) ->
+            Environ.env -> Evd.evar_map ref -> glob_constr -> unsafe_judgment) ->
            Environ.env ->
            Evd.evar_map ->
            (types * tomatch_type) list ->
            rel_context list ->
            constr option ->
-           'a option -> (Evd.evar_map * Names.name list * constr) list
+           glob_constr option -> (Evd.evar_map * Names.name list * constr) list
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 1cbea68dd..043616a51 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -1109,7 +1109,7 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs =
               match evar_conv_x ts env_evar evd CUMUL idty evty with
               | UnifFailure _ -> error "Cannot find an instance"
               | Success evd ->
-              match reconsider_conv_pbs (evar_conv_x ts) evd with
+              match reconsider_unif_constraints (evar_conv_x ts) evd with
               | UnifFailure _ -> error "Cannot find an instance"
               | Success evd ->
               evd
@@ -1244,7 +1244,7 @@ let rec solve_unconstrained_evars_with_candidates ts evd =
             let conv_algo = evar_conv_x ts in
             let evd = check_evar_instance evd evk (EConstr.of_constr a) conv_algo in
             let evd = Evd.define evk a evd in
-            match reconsider_conv_pbs conv_algo evd with
+            match reconsider_unif_constraints conv_algo evd with
             | Success evd -> solve_unconstrained_evars_with_candidates ts evd
             | UnifFailure _ -> aux l
           with
@@ -1267,7 +1267,7 @@ let solve_unconstrained_impossible_cases env evd =
 	Evd.define evk (EConstr.Unsafe.to_constr ty) evd' 
     | _ -> evd') evd evd
 
-let consider_remaining_unif_problems env
+let solve_unif_constraints_with_heuristics env
     ?(ts=Conv_oracle.get_transp_state (Environ.oracle env)) evd =
   let evd = solve_unconstrained_evars_with_candidates ts evd in
   let rec aux evd pbs progress stuck =
@@ -1301,6 +1301,8 @@ let consider_remaining_unif_problems env
   check_problems_are_solved env heuristic_solved_evd;
   solve_unconstrained_impossible_cases env heuristic_solved_evd
 
+let consider_remaining_unif_problems = solve_unif_constraints_with_heuristics
+
 (* Main entry points *)
 
 exception UnableToUnify of evar_map * unification_error
diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli
index a0ff924ef..fc07f0fbe 100644
--- a/pretyping/evarconv.mli
+++ b/pretyping/evarconv.mli
@@ -34,7 +34,10 @@ val e_cumul : env -> ?ts:transparent_state -> evar_map ref -> constr -> constr -
 (** Try heuristics to solve pending unification problems and to solve
     evars with candidates *)
 
+val solve_unif_constraints_with_heuristics : env -> ?ts:transparent_state -> evar_map -> evar_map
+
 val consider_remaining_unif_problems : env -> ?ts:transparent_state -> evar_map -> evar_map
+(** @deprecated Alias for [solve_unif_constraints_with_heuristics] *)
 
 (** Check all pending unification problems are solved and raise an
     error otherwise *)
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 398f2665e..4d78d2eb0 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -44,33 +44,39 @@ let get_polymorphic_positions sigma f =
         templ.template_param_levels)
   | _ -> assert false
 
-let refresh_level evd s =
-  match Evd.is_sort_variable evd s with
-  | None -> true
-  | Some l -> not (Evd.is_flexible_level evd l)
-
 let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) ?(refreshset=false)
 		      pbty env evd t =
   let evdref = ref evd in
   let modified = ref false in
-  let rec refresh status dir t = 
-    match EConstr.kind !evdref t with
-    | Sort (Type u as s) when
-      (match Univ.universe_level u with
-      | None -> true
-      | Some l -> not onlyalg && refresh_level evd s) ->
+  (* direction: true for fresh universes lower than the existing ones *)
+  let refresh_sort status ~direction s =
     let s' = evd_comb0 (new_sort_variable status) evdref in
     let evd = 
-      if dir then set_leq_sort env !evdref s' s
+      if direction then set_leq_sort env !evdref s' s
       else set_leq_sort env !evdref s s'
     in
-      modified := true; evdref := evd; mkSort s'
-    | Sort (Prop Pos as s) when refreshset && not dir ->
-       let s' = evd_comb0 (new_sort_variable status) evdref in
-       let evd = set_leq_sort env !evdref s s' in
-       modified := true; evdref := evd; mkSort s'
+    modified := true; evdref := evd; mkSort s'
+  in
+  let rec refresh ~onlyalg status ~direction t =
+    match EConstr.kind !evdref t with
+    | Sort (Type u as s) ->
+       (match Univ.universe_level u with
+	| None -> refresh_sort status ~direction s
+	| Some l ->
+	   (match Evd.universe_rigidity evd l with
+	    | UnivRigid ->
+	       if not onlyalg then refresh_sort status ~direction s
+	       else t
+	    | UnivFlexible alg ->
+	       if onlyalg && alg then
+	         (evdref := Evd.make_flexible_variable !evdref false l; t)
+	       else t))
+    | Sort (Prop Pos as s) when refreshset && not direction ->
+       (* Cannot make a universe "lower" than "Set",
+          only refreshing when we want higher universes. *)
+       refresh_sort status ~direction s
     | Prod (na,u,v) -> 
-      mkProd (na,u,refresh status dir v)
+      mkProd (na, u, refresh ~onlyalg status ~direction v)
     | _ -> t
   (** Refresh the types of evars under template polymorphic references *)
   and refresh_term_evars onevars top t =
@@ -83,7 +89,7 @@ let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) ?(refreshset=false)
       Array.iter (refresh_term_evars onevars false) args
     | Evar (ev, a) when onevars ->
       let evi = Evd.find !evdref ev in
-      let ty' = refresh univ_flexible true (EConstr.of_constr evi.evar_concl) in
+      let ty' = refresh ~onlyalg univ_flexible ~direction:true (EConstr.of_constr evi.evar_concl) in
 	if !modified then 
 	  evdref := Evd.add !evdref ev {evi with evar_concl = EConstr.Unsafe.to_constr ty'}
 	else ()
@@ -103,9 +109,11 @@ let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) ?(refreshset=false)
   in
   let t' = 
     if isArity !evdref t then
-      (match pbty with
-      | None -> t
-      | Some dir -> refresh status dir t)
+      match pbty with
+      | None ->
+	 (* No cumulativity needed, but we still need to refresh the algebraics *)
+	 refresh ~onlyalg:true univ_flexible ~direction:false t
+      | Some direction -> refresh ~onlyalg status ~direction t
     else (refresh_term_evars false true t; t)
   in
     if !modified then !evdref, t' else !evdref, t
@@ -1680,7 +1688,7 @@ let status_changed evd lev (pbty,_,t1,t2) =
   (try Evar.Set.mem (head_evar evd t1) lev with NoHeadEvar -> false) ||
   (try Evar.Set.mem (head_evar evd t2) lev with NoHeadEvar -> false)
 
-let reconsider_conv_pbs conv_algo evd =
+let reconsider_unif_constraints conv_algo evd =
   let (evd,pbs) = extract_changed_conv_pbs evd (status_changed evd) in
   List.fold_left
     (fun p (pbty,env,t1,t2 as x) ->
@@ -1693,6 +1701,8 @@ let reconsider_conv_pbs conv_algo evd =
     (Success evd)
     pbs
 
+let reconsider_conv_pbs = reconsider_unif_constraints
+
 (* Tries to solve problem t1 = t2.
  * Precondition: t1 is an uninstantiated evar
  * Returns an optional list of evars that were instantiated, or None
@@ -1703,7 +1713,7 @@ let solve_simple_eqn conv_algo ?(choose=false) env evd (pbty,(evk1,args1 as ev1)
   try
     let t2 = whd_betaiota evd t2 in (* includes whd_evar *)
     let evd = evar_define conv_algo ~choose env evd pbty ev1 t2 in
-      reconsider_conv_pbs conv_algo evd
+      reconsider_unif_constraints conv_algo evd
   with
     | NotInvertibleUsingOurAlgorithm t ->
         UnifFailure (evd,NotClean (ev1,env,t))
diff --git a/pretyping/evarsolve.mli b/pretyping/evarsolve.mli
index b827a0ca4..02b5c59d2 100644
--- a/pretyping/evarsolve.mli
+++ b/pretyping/evarsolve.mli
@@ -59,7 +59,10 @@ val solve_evar_evar : ?force:bool ->
 val solve_simple_eqn : conv_fun -> ?choose:bool -> env ->  evar_map ->
   bool option * existential * constr -> unification_result
 
+val reconsider_unif_constraints : conv_fun -> evar_map -> unification_result
+
 val reconsider_conv_pbs : conv_fun -> evar_map -> unification_result
+(** @deprecated Alias for [reconsider_unif_constraints] *)
 
 val is_unification_pattern_evar : env -> evar_map -> existential -> constr list ->
   constr -> alias list option
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 9e823ab4c..d5967c4bf 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -24,14 +24,14 @@ open Context.Rel.Declaration
 
 let type_of_inductive env (ind,u) =
  let (mib,_ as specif) = Inductive.lookup_mind_specif env ind in
- Typeops.check_hyps_inclusion env (mkInd ind) mib.mind_hyps;
+ Typeops.check_hyps_inclusion env mkInd ind mib.mind_hyps;
  Inductive.type_of_inductive env (specif,u)
 
 (* Return type as quoted by the user *)
 let type_of_constructor env (cstr,u) =
  let (mib,_ as specif) =
    Inductive.lookup_mind_specif env (inductive_of_constructor cstr) in
- Typeops.check_hyps_inclusion env (mkConstruct cstr) mib.mind_hyps;
+ Typeops.check_hyps_inclusion env mkConstruct cstr mib.mind_hyps;
  Inductive.type_of_constructor (cstr,u) specif
 
 (* Return constructor types in user form *)
@@ -632,7 +632,7 @@ let type_of_projection_knowing_arg env sigma p c ty =
       raise (Invalid_argument "type_of_projection_knowing_arg_type: not an inductive type")
   in
   let (_,u), pars = dest_ind_family pars in
-  substl (c :: List.rev pars) (Typeops.type_of_projection env (p,u))
+  substl (c :: List.rev pars) (Typeops.type_of_projection_constant env (p,u))
 
 (***********************************************)
 (* Guard condition *)
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 563769df5..846d8055a 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -249,7 +249,7 @@ type inference_hook = env -> evar_map -> evar -> evar_map * constr
 
 type inference_flags = {
   use_typeclasses : bool;
-  use_unif_heuristics : bool;
+  solve_unification_constraints : bool;
   use_hook : inference_hook option;
   fail_evar : bool;
   expand_evars : bool
@@ -296,7 +296,7 @@ let apply_inference_hook hook evdref pending =
 
 let apply_heuristics env evdref fail_evar =
   (* Resolve eagerly, potentially making wrong choices *)
-  try evdref := consider_remaining_unif_problems
+  try evdref := solve_unif_constraints_with_heuristics
 	~ts:(Typeclasses.classes_transparent_state ()) env !evdref
   with e when CErrors.noncritical e ->
     let e = CErrors.push e in if fail_evar then iraise e
@@ -343,7 +343,7 @@ let solve_remaining_evars flags env current_sigma pending =
   if flags.use_typeclasses then apply_typeclasses env evdref frozen false;
   if Option.has_some flags.use_hook then
     apply_inference_hook (Option.get flags.use_hook env) evdref pending;
-  if flags.use_unif_heuristics then apply_heuristics env evdref false;
+  if flags.solve_unification_constraints then apply_heuristics env evdref false;
   if flags.fail_evar then check_evars_are_solved env !evdref frozen pending;
   !evdref
 
@@ -1121,14 +1121,14 @@ let ise_pretype_gen flags env sigma lvar kind c =
 
 let default_inference_flags fail = {
   use_typeclasses = true;
-  use_unif_heuristics = true;
+  solve_unification_constraints = true;
   use_hook = None;
   fail_evar = fail;
   expand_evars = true }
 
 let no_classes_no_fail_inference_flags = {
   use_typeclasses = false;
-  use_unif_heuristics = true;
+  solve_unification_constraints = true;
   use_hook = None;
   fail_evar = false;
   expand_evars = true }
@@ -1194,7 +1194,7 @@ let understand_ltac flags env sigma lvar kind c =
 
 let constr_flags = {
   use_typeclasses = true;
-  use_unif_heuristics = true;
+  solve_unification_constraints = true;
   use_hook = None;
   fail_evar = true;
   expand_evars = true }
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index 47ad93d7e..7284c0655 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -52,7 +52,7 @@ type inference_hook = env -> evar_map -> evar -> evar_map * constr
 
 type inference_flags = {
   use_typeclasses : bool;
-  use_unif_heuristics : bool;
+  solve_unification_constraints : bool;
   use_hook : inference_hook option;
   fail_evar : bool;
   expand_evars : bool
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index a1585ef52..8be3b8328 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -1295,7 +1295,7 @@ let sigma_compare_sorts env pb s0 s1 sigma =
   match pb with
   | Reduction.CONV -> Evd.set_eq_sort env sigma s0 s1
   | Reduction.CUMUL -> Evd.set_leq_sort env sigma s0 s1
-    
+
 let sigma_compare_instances ~flex i0 i1 sigma =
   try Evd.set_eq_instances ~flex sigma i0 i1
   with Evd.UniversesDiffer
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index ce570ee12..478499d91 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -68,7 +68,8 @@ type typeclass = {
   cl_props : Context.Rel.t;
 
   (* The method implementaions as projections. *)
-  cl_projs : (Name.t * (direction * int option) option * constant option) list;
+  cl_projs : (Name.t * (direction * Vernacexpr.hint_info_expr) option
+	      * constant option) list;
   
   cl_strict : bool;
 
@@ -79,10 +80,9 @@ type typeclasses = typeclass Refmap.t
 
 type instance = {
   is_class: global_reference;
-  is_pri: int option;
+  is_info: Vernacexpr.hint_info_expr;
   (* Sections where the instance should be redeclared,
-     -1 for discard, 0 for none, mutable to avoid redeclarations
-     when multiple rebuild_object happen. *)
+     -1 for discard, 0 for none. *)
   is_global: int;
   is_poly: bool;
   is_impl: global_reference;
@@ -92,15 +92,15 @@ type instances = (instance Refmap.t) Refmap.t
 
 let instance_impl is = is.is_impl
 
-let instance_priority is = is.is_pri
+let hint_priority is = is.is_info.Vernacexpr.hint_priority
 
-let new_instance cl pri glob poly impl =
+let new_instance cl info glob poly impl =
   let global =
     if glob then Lib.sections_depth ()
     else -1
   in
     { is_class = cl.cl_impl;
-      is_pri = pri ;
+      is_info = info ;
       is_global = global ;
       is_poly = poly;
       is_impl = impl }
@@ -274,7 +274,9 @@ let check_instance env sigma c =
       not (Evd.has_undefined evd)
   with e when CErrors.noncritical e -> false
 
-let build_subclasses ~check env sigma glob pri =
+open Vernacexpr
+
+let build_subclasses ~check env sigma glob { hint_priority = pri } =
   let _id = Nametab.basename_of_global glob in
   let _next_id = 
     let i = ref (-1) in 
@@ -298,25 +300,25 @@ let build_subclasses ~check env sigma glob pri =
 	   match b with 
 	   | None -> None
 	   | Some (Backward, _) -> None
-	   | Some (Forward, pri') ->
+	   | Some (Forward, info) ->
 	     let proj = Option.get proj in
 	     let rels = List.map (fun d -> Termops.map_rel_decl EConstr.Unsafe.to_constr d) rels in
 	     let body = it_mkLambda_or_LetIn (mkApp (mkConstU (proj,u), projargs)) rels in
 	       if check && check_instance env sigma (EConstr.of_constr body) then None
 	       else 
-		 let pri = 
-		   match pri, pri' with
+		 let newpri =
+		   match pri, info.hint_priority with
 		   | Some p, Some p' -> Some (p + p')
 		   | Some p, None -> Some (p + 1)
 		   | _, _ -> None
 		 in
-		   Some (ConstRef proj, pri, body)) tc.cl_projs 
+		   Some (ConstRef proj, { info with hint_priority = newpri }, body)) tc.cl_projs
 	in
-	let declare_proj hints (cref, pri, body) =
+	let declare_proj hints (cref, info, body) =
 	  let path' = cref :: path in
 	  let ty = Retyping.get_type_of env sigma (EConstr.of_constr body) in
 	  let rest = aux pri body ty path' in
-	    hints @ (path', pri, body) :: rest
+	    hints @ (path', info, body) :: rest
 	in List.fold_left declare_proj [] projs 
   in
   let term = Universes.constr_of_global_univ (glob,Univ.UContext.instance ctx) in
@@ -370,11 +372,11 @@ let is_local i = Int.equal i.is_global (-1)
 let add_instance check inst =
   let poly = Global.is_polymorphic inst.is_impl in
   add_instance_hint (IsGlobal inst.is_impl) [inst.is_impl] (is_local inst) 
-    inst.is_pri poly;
+    inst.is_info poly;
   List.iter (fun (path, pri, c) -> add_instance_hint (IsConstr c) path
     (is_local inst) pri poly)
     (build_subclasses ~check:(check && not (isVarRef inst.is_impl))
-       (Global.env ()) (Evd.from_env (Global.env ())) inst.is_impl inst.is_pri)
+       (Global.env ()) (Evd.from_env (Global.env ())) inst.is_impl inst.is_info)
 
 let rebuild_instance (action, inst) =
   let () = match action with
@@ -406,26 +408,22 @@ let remove_instance i =
   Lib.add_anonymous_leaf (instance_input (RemoveInstance, i));
   remove_instance_hint i.is_impl
 
-let declare_instance pri local glob =
+let declare_instance info local glob =
   let ty = Global.type_of_global_unsafe glob in
+  let info = Option.default {hint_priority = None; hint_pattern = None} info in
     match class_of_constr Evd.empty (EConstr.of_constr ty) with
     | Some (rels, ((tc,_), args) as _cl) ->
-      add_instance (new_instance tc pri (not local) (Flags.use_polymorphic_flag ()) glob)
-(*       let path, hints = build_subclasses (not local) (Global.env ()) Evd.empty glob in *)
-(*       let entries = List.map (fun (path, pri, c) -> (pri, local, path, c)) hints in *)
-(* 	Auto.add_hints local [typeclasses_db] (Auto.HintsResolveEntry entries); *)
-(* 	Auto.add_hints local [typeclasses_db]  *)
-(* 	(Auto.HintsCutEntry (PathSeq (PathStar (PathAtom PathAny), path))) *)
+      add_instance (new_instance tc info (not local) (Flags.use_polymorphic_flag ()) glob)
     | None -> ()
 
 let add_class cl =
   add_class cl;
   List.iter (fun (n, inst, body) ->
 	     match inst with
-	     | Some (Backward, pri) ->
+	     | Some (Backward, info) ->
 	       (match body with
 	       | None -> CErrors.error "Non-definable projection can not be declared as a subinstance"
-	       | Some b -> declare_instance pri false (ConstRef b))
+	       | Some b -> declare_instance (Some info) false (ConstRef b))
 	     | _ -> ())
   cl.cl_projs
 
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index 0c30296d3..7990b12cd 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -32,7 +32,7 @@ type typeclass = {
       Some may be undefinable due to sorting restrictions or simply undefined if 
       no name is provided. The [int option option] indicates subclasses whose hint has
       the given priority. *)
-  cl_projs : (Name.t * (direction * int option) option * constant option) list;
+  cl_projs : (Name.t * (direction * Vernacexpr.hint_info_expr) option * constant option) list;
 
   (** Whether we use matching or full unification during resolution *)
   cl_strict : bool; 
@@ -50,7 +50,7 @@ val all_instances : unit -> instance list
 
 val add_class : typeclass -> unit
 
-val new_instance : typeclass -> int option -> bool -> Decl_kinds.polymorphic -> 
+val new_instance : typeclass -> Vernacexpr.hint_info_expr -> bool -> Decl_kinds.polymorphic ->
   global_reference -> instance
 val add_instance : instance -> unit
 val remove_instance : instance -> unit
@@ -71,7 +71,7 @@ val class_of_constr : evar_map -> EConstr.constr -> (EConstr.rel_context * (type
   
 val instance_impl : instance -> global_reference
 
-val instance_priority : instance -> int option
+val hint_priority : instance -> int option
 
 val is_class : global_reference -> bool
 val is_instance : global_reference -> bool
@@ -113,21 +113,22 @@ val classes_transparent_state : unit -> transparent_state
 
 val add_instance_hint_hook : 
   (global_reference_or_constr -> global_reference list ->
-   bool (* local? *) -> int option -> Decl_kinds.polymorphic -> unit) Hook.t
+   bool (* local? *) -> Vernacexpr.hint_info_expr -> Decl_kinds.polymorphic -> unit) Hook.t
 val remove_instance_hint_hook : (global_reference -> unit) Hook.t
 val add_instance_hint : global_reference_or_constr -> global_reference list -> 
-  bool -> int option -> Decl_kinds.polymorphic -> unit
+  bool -> Vernacexpr.hint_info_expr -> Decl_kinds.polymorphic -> unit
 val remove_instance_hint : global_reference -> unit
 
 val solve_all_instances_hook : (env -> evar_map -> evar_filter -> bool -> bool -> bool -> evar_map) Hook.t
 val solve_one_instance_hook : (env -> evar_map -> EConstr.types -> bool -> evar_map * EConstr.constr) Hook.t
 
-val declare_instance : int option -> bool -> global_reference -> unit
+val declare_instance : Vernacexpr.hint_info_expr option -> bool -> global_reference -> unit
 
 
 (** Build the subinstances hints for a given typeclass object.
     check tells if we should check for existence of the 
     subinstances and add only the missing ones. *)
 
-val build_subclasses : check:bool -> env -> evar_map -> global_reference -> int option (* priority *) ->
-  (global_reference list * int option * constr) list
+val build_subclasses : check:bool -> env -> evar_map -> global_reference ->
+		       Vernacexpr.hint_info_expr ->
+		       (global_reference list * Vernacexpr.hint_info_expr * constr) list
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 336b3348c..8824c06ab 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -1251,7 +1251,7 @@ let is_mimick_head sigma ts f =
 let try_to_coerce env evd c cty tycon =
   let j = make_judge c cty in
   let (evd',j') = inh_conv_coerce_rigid_to true Loc.ghost env evd j tycon in
-  let evd' = Evarconv.consider_remaining_unif_problems env evd' in
+  let evd' = Evarconv.solve_unif_constraints_with_heuristics env evd' in
   let evd' = Evd.map_metas_fvalue (fun c -> EConstr.Unsafe.to_constr (nf_evar evd' (EConstr.of_constr c))) evd' in
     (evd',j'.uj_val)
 
@@ -1301,7 +1301,11 @@ let solve_simple_evar_eqn ts env evd ev rhs =
   | UnifFailure (evd,reason) ->
       error_cannot_unify env evd ~reason (mkEvar ev,rhs);
   | Success evd ->
-      Evarconv.consider_remaining_unif_problems env evd
+     if Flags.version_less_or_equal Flags.V8_5 then
+       (* We used to force solving unrelated problems at arbitrary times *)
+       Evarconv.solve_unif_constraints_with_heuristics env evd
+     else (* solve_simple_eqn calls reconsider_unif_constraints itself *)
+       evd
 
 (* [w_merge env sigma b metas evars] merges common instances in metas
    or in evars, possibly generating new unification problems; if [b]
@@ -1328,7 +1332,6 @@ let w_merge env with_types flags (evd,metas,evars : subst0) =
 	      if is_mimick_head evd flags.modulo_delta f then
 		let evd' =
 		  mimick_undefined_evar evd flags f (Array.length cl) evk in
-		(* let evd' = Evarconv.consider_remaining_unif_problems env evd' in *)
 		  w_merge_rec evd' metas evars eqns
 	      else
 		let evd' = 
@@ -1424,8 +1427,7 @@ let w_merge env with_types flags (evd,metas,evars : subst0) =
                 (* Assign evars in the order of assignments during unification *)
                 (List.rev evars) []
   in
-    if with_types then check_types res
-    else res
+  if with_types then check_types res else res
 
 let retract_coercible_metas evd =
   let (metas, evd) = retract_coercible_metas evd in
@@ -1492,7 +1494,7 @@ let w_typed_unify_array env evd flags f1 l1 f2 l2 =
   let subst = Array.fold_left2 fold_subst subst l1 l2 in
   let evd = w_merge env true flags.merge_unify_flags subst in
   try_resolve_typeclasses env evd flags.resolve_evars
-    (mkApp(f1,l1)) (mkApp(f2,l2))
+                          (mkApp(f1,l1)) (mkApp(f2,l2))
 
 (* takes a substitution s, an open term op and a closed term cl
    try to find a subterm of cl which matches op, if op is just a Meta
@@ -1924,21 +1926,14 @@ let secondOrderAbstraction env evd flags typ (p, oplist) =
     error_wrong_abstraction_type env evd'
       (Evd.meta_name evd p) pred typp predtyp;
   w_merge env false flags.merge_unify_flags
-    (evd',[p,pred,(Conv,TypeProcessed)],[])
-
-  (* let evd',metas,evars =  *)
-  (*   try unify_0 env evd' CUMUL flags predtyp typp  *)
-  (*   with NotConvertible -> *)
-  (*     error_wrong_abstraction_type env evd *)
-  (*       (Evd.meta_name evd p) pred typp predtyp *)
-  (* in *)
-  (*   w_merge env false flags (evd',(p,pred,(Conv,TypeProcessed))::metas,evars) *)
+          (evd',[p,pred,(Conv,TypeProcessed)],[])
 
 let secondOrderDependentAbstraction env evd flags typ (p, oplist) =
   let typp = Typing.meta_type evd p in
   let evd, pred = abstract_list_all_with_dependencies env evd typp typ oplist in
   w_merge env false flags.merge_unify_flags
-    (evd,[p,pred,(Conv,TypeProcessed)],[])
+          (evd,[p,pred,(Conv,TypeProcessed)],[])
+
 
 let secondOrderAbstractionAlgo dep =
   if dep then secondOrderDependentAbstraction else secondOrderAbstraction