Change Hint Resolve, Immediate to take a global reference as argument

instead of a general constr: this is the most common case and does
not loose generality (one can simply define constrs before Hint Resolving
them). Benefits:
- Natural semantics for typeclasses, not class resolution needed at
Hint Resolve time, meaning less trouble for users as well.
- Ability to [Hint Remove] any hint so declared.
- Simplifies the implementation as well.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15930 85f007b7-540e-0410-9357-904b9bb8a0f7

24 files changed, 168 insertions, 107 deletions

diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index 31c1643d2..25897950e 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -103,8 +103,8 @@ type comment =
   | CommentInt of int
 
 type hints_expr =
-  | HintsResolve of (int option * bool * constr_expr) list
-  | HintsImmediate of constr_expr list
+  | HintsResolve of (int option * bool * reference) list
+  | HintsImmediate of reference list
   | HintsUnfold of reference list
   | HintsTransparency of reference list * bool
   | HintsConstructors of reference list
diff --git a/library/declare.ml b/library/declare.ml
index aa10cf314..7364031d5 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -180,6 +180,17 @@ let declare_constant ?(internal = UserVerbose) id (cd,kind) =
   !xml_declare_constant (internal,kn);
   kn
 
+let declare_definition ?(internal=UserVerbose) ?(opaque=false) ?(kind=Decl_kinds.Definition)
+  id ?types body =
+  let cb = 
+    { Entries.const_entry_body = body;
+      const_entry_type = types;
+      const_entry_opaque = opaque;
+      const_entry_secctx = None }
+  in
+    declare_constant ~internal id
+      (Entries.DefinitionEntry cb, Decl_kinds.IsDefinition kind) 
+
 (** Declaration of inductive blocks *)
 
 let declare_inductive_argument_scopes kn mie =
diff --git a/library/declare.mli b/library/declare.mli
index 6f69f673e..9cc6e371c 100644
--- a/library/declare.mli
+++ b/library/declare.mli
@@ -57,6 +57,10 @@ type internal_flag =
 val declare_constant :
  ?internal:internal_flag -> identifier -> constant_declaration -> constant
 
+val declare_definition : 
+  ?internal:internal_flag -> ?opaque:bool -> ?kind:definition_object_kind ->
+  identifier -> ?types:constr -> constr -> constant
+
 (** [declare_mind me] declares a block of inductive types with
    their constructors in the current section; it returns the path of
    the whole block (boolean must be true iff it is a record) *)
diff --git a/library/global.mli b/library/global.mli
index ff3c73199..82b7cc8eb 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -101,6 +101,5 @@ val import : compiled_library -> Digest.t -> module_path
 val type_of_global : Globnames.global_reference -> types
 val env_of_context : Environ.named_context_val -> Environ.env
 
-
 (** spiwack: register/unregister function for retroknowledge *)
 val register : Retroknowledge.field -> constr -> constr -> unit
diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4
index eee6d3ce6..f2bf542ef 100644
--- a/parsing/g_proofs.ml4
+++ b/parsing/g_proofs.ml4
@@ -91,7 +91,7 @@ GEXTEND Gram
 	  VernacHints (enforce_module_locality local,dbnames, h)
       (* Declare "Resolve" explicitly so as to be able to later extend with
          "Resolve ->" and "Resolve <-" *)
-      | IDENT "Hint"; IDENT "Resolve"; lc = LIST1 constr; n = OPT natural;
+      | IDENT "Hint"; IDENT "Resolve"; lc = LIST1 reference; n = OPT natural;
 	  dbnames = opt_hintbases ->
 	  VernacHints (use_module_locality (),dbnames,
 	    HintsResolve (List.map (fun x -> (n, true, x)) lc))
@@ -101,9 +101,9 @@ GEXTEND Gram
     [ [ IDENT "Local" -> true | -> false ] ]
   ;
   hint:
-    [ [ IDENT "Resolve"; lc = LIST1 constr; n = OPT natural ->
+    [ [ IDENT "Resolve"; lc = LIST1 global; n = OPT natural ->
           HintsResolve (List.map (fun x -> (n, true, x)) lc)
-      | IDENT "Immediate"; lc = LIST1 constr -> HintsImmediate lc
+      | IDENT "Immediate"; lc = LIST1 global -> HintsImmediate lc
       | IDENT "Transparent"; lc = LIST1 global -> HintsTransparency (lc, true)
       | IDENT "Opaque"; lc = LIST1 global -> HintsTransparency (lc, false)
       | IDENT "Unfold"; lqid = LIST1 global -> HintsUnfold lqid
diff --git a/plugins/setoid_ring/Field_theory.v b/plugins/setoid_ring/Field_theory.v
index bc05c252c..341c0e6f5 100644
--- a/plugins/setoid_ring/Field_theory.v
+++ b/plugins/setoid_ring/Field_theory.v
@@ -84,15 +84,29 @@ Qed.
 Let eq_trans := Setoid.Seq_trans _ _ Rsth.
 Let eq_sym := Setoid.Seq_sym _ _ Rsth.
 Let eq_refl := Setoid.Seq_refl _ _ Rsth.
-
-Hint Resolve eq_refl rdiv_def rinv_l rI_neq_rO CRmorph.(morph1) .
-Hint Resolve (Rmul_ext Reqe) (Rmul_ext Reqe) (Radd_ext Reqe)
-             (ARsub_ext Rsth Reqe ARth) (Ropp_ext Reqe) SRinv_ext.
-Hint Resolve (ARadd_0_l  ARth) (ARadd_comm  ARth) (ARadd_assoc ARth)
-             (ARmul_1_l  ARth) (ARmul_0_l  ARth)
-             (ARmul_comm  ARth) (ARmul_assoc ARth) (ARdistr_l  ARth)
-             (ARopp_mul_l ARth) (ARopp_add  ARth)
-             (ARsub_def  ARth) .
+Let mor1h := CRmorph.(morph1).
+
+Hint Resolve eq_refl rdiv_def rinv_l rI_neq_rO .
+
+Let lem1 := Rmul_ext Reqe.
+Let lem2 := Rmul_ext Reqe.
+Let lem3 := (Radd_ext Reqe).
+Let lem4 := ARsub_ext Rsth Reqe ARth.
+Let lem5 := Ropp_ext Reqe.
+Let lem6 := ARadd_0_l  ARth.
+Let lem7 := ARadd_comm  ARth.
+Let lem8 := (ARadd_assoc ARth).
+Let lem9 := ARmul_1_l  ARth.
+Let lem10 := (ARmul_0_l  ARth).
+Let lem11 := ARmul_comm  ARth.
+Let lem12 := ARmul_assoc ARth.
+Let lem13 := (ARdistr_l  ARth).
+Let lem14 := ARopp_mul_l ARth.
+Let lem15 := (ARopp_add  ARth).
+Let lem16 := ARsub_def  ARth.
+
+Hint Resolve lem1 lem2 lem3 lem4 lem5 lem6 lem7 lem8 lem9 lem10
+     lem11 lem12 lem13 lem14 lem15 lem16 SRinv_ext.
 
  (* Power coefficients *)
  Variable Cpow : Type.
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 2749538c0..95fdcdfe6 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -39,6 +39,11 @@ let classes_transparent_state_ref = ref (fun () -> assert false)
 let register_classes_transparent_state = (:=) classes_transparent_state_ref
 let classes_transparent_state () = !classes_transparent_state_ref ()
 
+
+let declare_definition_ref = ref (fun ?internal ?opaque ?kind id ?types constr -> assert false)
+let register_declare_definition =
+  (:=) declare_definition_ref
+
 let solve_instanciation_problem = ref (fun _ _ _ -> assert false)
 
 let resolve_one_typeclass env evm t =
@@ -238,6 +243,12 @@ let check_instance env sigma c =
   with _ -> false
 
 let build_subclasses ~check env sigma glob pri =
+  let id = Nametab.basename_of_global glob in
+  let next_id = 
+    let i = ref (-1) in 
+      (fun () -> incr i;
+        Nameops.add_suffix id ("_subinstance_" ^ string_of_int !i))
+  in
   let rec aux pri c =
     let ty = Evarutil.nf_evar sigma (Retyping.get_type_of env sigma c) in
       match class_of_constr ty with
@@ -261,10 +272,13 @@ let build_subclasses ~check env sigma glob pri =
 		   | Some p, None -> Some (p + 1)
 		   | _, _ -> None
 		 in
-		   Some (ConstRef proj, pri, body)) tc.cl_projs 
+		 let c = !declare_definition_ref ~internal:true
+		   ~kind:Decl_kinds.Instance (next_id ()) body 
+		 in
+		   Some (ConstRef proj, pri, ConstRef c)) tc.cl_projs 
 	in
 	let declare_proj hints (cref, pri, body) =
-	  let rest = aux pri body in
+	  let rest = aux pri (constr_of_global body) in
 	    hints @ (pri, body) :: rest
 	in List.fold_left declare_proj [] projs 
   in aux pri (constr_of_global glob)
@@ -313,7 +327,7 @@ let discharge_instance (_, (action, inst)) =
 let is_local i = i.is_global = -1
 
 let add_instance check inst =
-  add_instance_hint (constr_of_global inst.is_impl) (is_local inst) inst.is_pri;
+  add_instance_hint inst.is_impl (is_local inst) inst.is_pri;
   List.iter (fun (pri, c) -> add_instance_hint c (is_local inst) pri) 
     (build_subclasses ~check:(check && not (isVarRef inst.is_impl))
        (Global.env ()) Evd.empty inst.is_impl inst.is_pri)
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index 039aeb1e6..729cbb2ad 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -103,9 +103,13 @@ val set_typeclass_transparency : evaluable_global_reference -> bool -> bool -> u
 val register_classes_transparent_state : (unit -> transparent_state) -> unit
 val classes_transparent_state : unit -> transparent_state
 
-val register_add_instance_hint : (constr -> bool (* local? *) -> int option -> unit) -> unit
+val register_declare_definition : (?internal:bool -> ?opaque:bool -> ?kind:definition_object_kind -> identifier -> ?types:constr -> constr -> constant) -> unit
+
+
+val register_add_instance_hint : 
+  (global_reference -> bool (* local? *) -> int option -> unit) -> unit
 val register_remove_instance_hint : (global_reference -> unit) -> unit
-val add_instance_hint : constr -> bool -> int option -> unit
+val add_instance_hint : global_reference -> bool -> int option -> unit
 val remove_instance_hint : global_reference -> unit
 
 val solve_instanciations_problem : (env -> evar_map -> evar_filter -> bool -> bool -> evar_map) ref
@@ -119,4 +123,4 @@ val declare_instance : int option -> bool -> global_reference -> unit
     subinstances and add only the missing ones. *)
 
 val build_subclasses : check:bool -> env -> evar_map -> global_reference -> int option (* priority *) ->
-  (int option * constr) list
+  (int option * global_reference) list
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 2df8b8ce5..b914e3877 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -185,11 +185,11 @@ let pr_hints local db h pr_c pr_pat =
     match h with
     | HintsResolve l ->
         str "Resolve " ++ prlist_with_sep sep
-	  (fun (pri, _, c) -> pr_c c ++
+	  (fun (pri, _, c) -> pr_reference c ++
 	    match pri with Some x -> spc () ++ str"(" ++ int x ++ str")" | None -> mt ())
 	  l
     | HintsImmediate l ->
-        str"Immediate" ++ spc() ++ prlist_with_sep sep pr_c l
+        str"Immediate" ++ spc() ++ prlist_with_sep sep pr_reference l
     | HintsUnfold l ->
         str "Unfold " ++ prlist_with_sep sep pr_reference l
     | HintsTransparency (l, b) ->
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 47b89e9af..b20caf450 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -560,7 +560,8 @@ let make_extern pri pat tacast =
      name = PathAny;
      code = Extern tacast })
 
-let make_trivial env sigma ?(name=PathAny) c =
+let make_trivial env sigma ?(name=PathAny) r =
+  let c = constr_of_global r in
   let t = hnf_constr env sigma (type_of env sigma c) in
   let hd = head_of_constr_reference (fst (head_constr t)) in
   let ce = mk_clenv_from dummy_goal (c,t) in
@@ -716,8 +717,9 @@ let add_resolves env sigma clist local dbnames =
        Lib.add_anonymous_leaf
 	 (inAutoHint
 	    (local,dbname, AddHints
-     	      (List.flatten (List.map (fun (x, hnf, path, y) ->
-		make_resolves env sigma (true,hnf,Flags.is_verbose()) x ~name:path y) clist)))))
+     	      (List.flatten (List.map (fun (x, hnf, path, gr) ->
+		make_resolves env sigma (true,hnf,Flags.is_verbose()) x ~name:path 
+		  (constr_of_global gr)) clist)))))
     dbnames
 
 let add_unfolds l local dbnames =
@@ -772,8 +774,8 @@ let forward_intern_tac =
 let set_extern_intern_tac f = forward_intern_tac := f
 
 type hints_entry =
-  | HintsResolveEntry of (int option * bool * hints_path_atom * constr) list
-  | HintsImmediateEntry of (hints_path_atom * constr) list
+  | HintsResolveEntry of (int option * bool * hints_path_atom * global_reference) list
+  | HintsImmediateEntry of (hints_path_atom * global_reference) list
   | HintsCutEntry of hints_path
   | HintsUnfoldEntry of evaluable_global_reference list
   | HintsTransparencyEntry of evaluable_global_reference list * bool
@@ -813,24 +815,19 @@ let prepare_hint env (sigma,c) =
       mkNamedLambda id t (iter (replace_term evar (mkVar id) c)) in
   iter c
 
-let path_of_constr_expr c =
-  match c with
-  | Constrexpr.CRef r -> (try PathHints [global r] with _ -> PathAny)
-  | _ -> PathAny
-      
 let interp_hints h =
-  let f c =
-    let evd,c = Constrintern.interp_open_constr Evd.empty (Global.env()) c in
-    let c = prepare_hint (Global.env()) (evd,c) in
-    Evarutil.check_evars (Global.env()) Evd.empty evd c;
-    c in
   let fr r =
     let gr = global_with_alias r in
     let r' = evaluable_of_global_reference (Global.env()) gr in
     Dumpglob.add_glob (loc_of_reference r) gr;
     r' in
-  let fres (o, b, c) = (o, b, path_of_constr_expr c, f c) in
-  let fi c = path_of_constr_expr c, f c in
+  let fres (o, b, c) =
+    let gr = global_with_alias c in
+      (o, b, PathHints [gr], gr) in
+  let fi c =
+    let gr = global_with_alias c in
+      PathHints [gr], gr
+  in
   let fp = Constrintern.intern_constr_pattern Evd.empty (Global.env()) in
   match h with
   | HintsResolve lhints -> HintsResolveEntry (List.map fres lhints)
@@ -843,7 +840,8 @@ let interp_hints h =
         let ind = global_inductive_with_alias qid in
 	Dumpglob.dump_reference (fst (qualid_of_reference qid)) "<>" (string_of_reference qid) "ind";
         List.tabulate (fun i -> let c = (ind,i+1) in
-			 None, true, PathHints [ConstructRef c], mkConstruct c)
+				let gr = ConstructRef c in
+			 None, true, PathHints [gr], gr)
 	  (nconstructors ind) in
 	HintsResolveEntry (List.flatten (List.map constr_hints_of_ind lqid))
   | HintsExtern (pri, patcom, tacexp) ->
diff --git a/tactics/auto.mli b/tactics/auto.mli
index 094030bea..de1d2ff6b 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.mli
@@ -96,8 +96,8 @@ type hint_db_name = string
 type hint_db = Hint_db.t
 
 type hints_entry =
-  | HintsResolveEntry of (int option * bool * hints_path_atom * constr) list
-  | HintsImmediateEntry of (hints_path_atom * constr) list
+  | HintsResolveEntry of (int option * bool * hints_path_atom * global_reference) list
+  | HintsImmediateEntry of (hints_path_atom * global_reference) list
   | HintsCutEntry of hints_path
   | HintsUnfoldEntry of evaluable_global_reference list
   | HintsTransparencyEntry of evaluable_global_reference list * bool
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index 1fc013496..f2f5417ef 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -250,7 +250,7 @@ let make_resolve_hyp env sigma st flags only_classes pri (id, _, cty) =
 	  let hints = build_subclasses ~check:false env sigma (VarRef id) None in
 	    (List.map_append
 	       (fun (pri, c) -> make_resolves env sigma 
-		  (true,false,Flags.is_verbose()) pri c) 
+		  (true,false,Flags.is_verbose()) pri (constr_of_global c))
 	       hints)
 	else []
       in
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index c2d5de265..1c9833571 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -273,9 +273,10 @@ END
 open Term
 open Coqlib
 
-let project_hint pri l2r c =
+let project_hint pri l2r r =
+  let gr = Smartlocate.global_with_alias r in
   let env = Global.env() in
-  let c = Constrintern.interp_constr Evd.empty env c in
+  let c = Globnames.constr_of_global gr in
   let t = Retyping.get_type_of env Evd.empty c in
   let t =
     Tacred.reduce_to_quantified_ref env Evd.empty (Lazy.force coq_iff_ref) t in
@@ -288,24 +289,28 @@ let project_hint pri l2r c =
   let c = Reductionops.whd_beta Evd.empty (mkApp (c,Termops.extended_rel_vect 0 sign)) in
   let c = it_mkLambda_or_LetIn
     (mkApp (p,[|mkArrow a (lift 1 b);mkArrow b (lift 1 a);c|])) sign in
-  (pri,true,Auto.PathAny,c)
+  let id =
+    Nameops.add_suffix (Nametab.basename_of_global gr) ("_proj_" ^ (if l2r then "l2r" else "r2l"))
+  in
+  let c = Declare.declare_definition ~internal:Declare.KernelSilent id c in
+    (pri,true,Auto.PathAny, Globnames.ConstRef c)
 
 let add_hints_iff l2r lc n bl =
   Auto.add_hints true bl
     (Auto.HintsResolveEntry (List.map (project_hint n l2r) lc))
 
 VERNAC COMMAND EXTEND HintResolveIffLR
-  [ "Hint" "Resolve" "->" ne_constr_list(lc) natural_opt(n)
+  [ "Hint" "Resolve" "->" ne_global_list(lc) natural_opt(n)
     ":" preident_list(bl) ] ->
   [ add_hints_iff true lc n bl ]
-| [ "Hint" "Resolve" "->" ne_constr_list(lc) natural_opt(n) ] ->
+| [ "Hint" "Resolve" "->" ne_global_list(lc) natural_opt(n) ] ->
   [ add_hints_iff true lc n ["core"] ]
 END
 VERNAC COMMAND EXTEND HintResolveIffRL
-  [ "Hint" "Resolve" "<-" ne_constr_list(lc) natural_opt(n)
+  [ "Hint" "Resolve" "<-" ne_global_list(lc) natural_opt(n)
     ":" preident_list(bl) ] ->
   [ add_hints_iff false lc n bl ]
-| [ "Hint" "Resolve" "<-" ne_constr_list(lc) natural_opt(n) ] ->
+| [ "Hint" "Resolve" "<-" ne_global_list(lc) natural_opt(n) ] ->
   [ add_hints_iff false lc n ["core"] ]
 END
 
diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v
index 36c328cf4..b8fdac8c9 100644
--- a/theories/Classes/RelationClasses.v
+++ b/theories/Classes/RelationClasses.v
@@ -56,7 +56,7 @@ Class Asymmetric {A} (R : relation A) :=
 Class Transitive {A} (R : relation A) :=
   transitivity : forall x y z, R x y -> R y z -> R x z.
 
-Hint Resolve @irreflexivity : ord.
+Hint Resolve irreflexivity : ord.
 
 Unset Implicit Arguments.
 
diff --git a/theories/Init/Peano.v b/theories/Init/Peano.v
index 8c6fba508..3c0fc02e4 100644
--- a/theories/Init/Peano.v
+++ b/theories/Init/Peano.v
@@ -30,9 +30,10 @@ Require Import Logic.
 Open Scope nat_scope.
 
 Definition eq_S := f_equal S.
+Definition f_equal_nat := f_equal (A:=nat).
 
-Hint Resolve (f_equal S): v62.
-Hint Resolve (f_equal (A:=nat)): core.
+Hint Resolve eq_S: v62.
+Hint Resolve f_equal_nat: core.
 
 (** The predecessor function *)
 
@@ -40,7 +41,8 @@ Definition pred (n:nat) : nat := match n with
                                  | O => n
                                  | S u => u
                                  end.
-Hint Resolve (f_equal pred): v62.
+Definition f_equal_pred := f_equal pred.
+Hint Resolve f_equal_pred: v62.
 
 Theorem pred_Sn : forall n:nat, n = pred (S n).
 Proof.
@@ -88,8 +90,10 @@ Fixpoint plus (n m:nat) : nat :=
 
 where "n + m" := (plus n m) : nat_scope.
 
-Hint Resolve (f_equal2 plus): v62.
-Hint Resolve (f_equal2 (A1:=nat) (A2:=nat)): core.
+Definition f_equal2_plus := f_equal2 plus.
+Hint Resolve f_equal2_plus: v62.
+Definition f_equal2_nat := f_equal2 (A1:=nat) (A2:=nat). 
+Hint Resolve f_equal2_nat: core.
 
 Lemma plus_n_O : forall n:nat, n = n + 0.
 Proof.
@@ -127,8 +131,8 @@ Fixpoint mult (n m:nat) : nat :=
   end
 
 where "n * m" := (mult n m) : nat_scope.
-
-Hint Resolve (f_equal2 mult): core.
+Definition f_equal2_mult := f_equal2 mult.
+Hint Resolve f_equal2_mult: core.
 
 Lemma mult_n_O : forall n:nat, 0 = n * 0.
 Proof.
diff --git a/theories/Lists/SetoidList.v b/theories/Lists/SetoidList.v
index 7d3c383c1..8fd229917 100644
--- a/theories/Lists/SetoidList.v
+++ b/theories/Lists/SetoidList.v
@@ -101,10 +101,12 @@ Proof. split; induction 1; auto. Qed.
 (** Results concerning lists modulo [eqA] *)
 
 Hypothesis eqA_equiv : Equivalence eqA.
+Definition eqarefl := (@Equivalence_Reflexive _ _ eqA_equiv).
+Definition eqatrans := (@Equivalence_Transitive _ _ eqA_equiv).
+Definition eqasym := (@Equivalence_Symmetric _ _ eqA_equiv).
 
-Hint Resolve (@Equivalence_Reflexive _ _ eqA_equiv).
-Hint Resolve (@Equivalence_Transitive _ _ eqA_equiv).
-Hint Immediate (@Equivalence_Symmetric _ _ eqA_equiv).
+Hint Resolve eqarefl eqatrans.
+Hint Immediate eqasym.
 
 Ltac inv := invlist InA; invlist sort; invlist lelistA; invlist NoDupA.
 
@@ -633,7 +635,9 @@ Variable ltA : A -> A -> Prop.
 Hypothesis ltA_strorder : StrictOrder ltA.
 Hypothesis ltA_compat : Proper (eqA==>eqA==>iff) ltA.
 
-Hint Resolve (@StrictOrder_Transitive _ _ ltA_strorder).
+Let sotrans := (@StrictOrder_Transitive _ _ ltA_strorder).
+
+Hint Resolve sotrans.
 
 Notation InfA:=(lelistA ltA).
 Notation SortA:=(sort ltA).
@@ -821,7 +825,7 @@ Arguments eq {A} x _.
 Lemma filter_InA : forall f, Proper (eqA==>eq) f ->
  forall l x, InA x (List.filter f l) <-> InA x l /\ f x = true.
 Proof.
-clear ltA ltA_compat ltA_strorder.
+clear sotrans ltA ltA_strorder ltA_compat.
 intros; do 2 rewrite InA_alt; intuition.
 destruct H0 as (y,(H0,H1)); rewrite filter_In in H1; exists y; intuition.
 destruct H0 as (y,(H0,H1)); rewrite filter_In in H1; intuition.
diff --git a/theories/MSets/MSetAVL.v b/theories/MSets/MSetAVL.v
index 1e66e2b5b..2182504dd 100644
--- a/theories/MSets/MSetAVL.v
+++ b/theories/MSets/MSetAVL.v
@@ -306,7 +306,7 @@ Include MSetGenTree.Props X I.
 Local Hint Immediate MX.eq_sym.
 Local Hint Unfold In lt_tree gt_tree Ok.
 Local Hint Constructors InT bst.
-Local Hint Resolve MX.eq_refl MX.eq_trans MX.lt_trans @ok.
+Local Hint Resolve MX.eq_refl MX.eq_trans MX.lt_trans ok.
 Local Hint Resolve lt_leaf gt_leaf lt_tree_node gt_tree_node.
 Local Hint Resolve lt_tree_not_in lt_tree_trans gt_tree_not_in gt_tree_trans.
 Local Hint Resolve elements_spec2.
diff --git a/theories/MSets/MSetGenTree.v b/theories/MSets/MSetGenTree.v
index cacd91343..b7f3f96c9 100644
--- a/theories/MSets/MSetGenTree.v
+++ b/theories/MSets/MSetGenTree.v
@@ -341,7 +341,7 @@ Module Import MX := OrderedTypeFacts X.
 Scheme tree_ind := Induction for tree Sort Prop.
 Scheme bst_ind := Induction for bst Sort Prop.
 
-Local Hint Resolve MX.eq_refl MX.eq_trans MX.lt_trans @ok.
+Local Hint Resolve MX.eq_refl MX.eq_trans MX.lt_trans ok.
 Local Hint Immediate MX.eq_sym.
 Local Hint Unfold In lt_tree gt_tree.
 Local Hint Constructors InT bst.
diff --git a/theories/MSets/MSetList.v b/theories/MSets/MSetList.v
index d9b1fd9bb..b0e09b719 100644
--- a/theories/MSets/MSetList.v
+++ b/theories/MSets/MSetList.v
@@ -228,16 +228,14 @@ Module MakeRaw (X: OrderedType) <: RawSets X.
   Notation Inf := (lelistA X.lt).
   Notation In := (InA X.eq).
 
-  (* TODO: modify proofs in order to avoid these hints *)
-  Hint Resolve (@Equivalence_Reflexive _ _ X.eq_equiv).
-  Hint Immediate (@Equivalence_Symmetric _ _ X.eq_equiv).
-  Hint Resolve (@Equivalence_Transitive _ _ X.eq_equiv).
+  Existing Instance X.eq_equiv.
+  Hint Extern 20 => solve [order].
 
   Definition IsOk s := Sort s.
 
   Class Ok (s:t) : Prop := ok : Sort s.
 
-  Hint Resolve @ok.
+  Hint Resolve ok.
   Hint Unfold Ok.
 
   Instance Sort_Ok s `(Hs : Sort s) : Ok s := { ok := Hs }.
@@ -343,7 +341,6 @@ Module MakeRaw (X: OrderedType) <: RawSets X.
   induction s; simpl; intros.
   intuition. inv; auto.
   elim_compare x a; inv; rewrite !InA_cons, ?IHs; intuition.
-  left; order.
   Qed.
 
   Lemma remove_inf :
@@ -402,8 +399,8 @@ Module MakeRaw (X: OrderedType) <: RawSets X.
   Global Instance union_ok s s' : forall `(Ok s, Ok s'), Ok (union s s').
   Proof.
   repeat rewrite <- isok_iff; revert s s'.
-  induction2; constructors; try apply @ok; auto.
-  apply Inf_eq with x'; auto; apply union_inf; auto; apply Inf_eq with x; auto.
+  induction2; constructors; try apply @ok; auto. 
+  apply Inf_eq with x'; auto; apply union_inf; auto; apply Inf_eq with x; auto; order.
   change (Inf x' (union (x :: l) l')); auto.
   Qed.
 
@@ -412,7 +409,6 @@ Module MakeRaw (X: OrderedType) <: RawSets X.
    In x (union s s') <-> In x s \/ In x s'.
   Proof.
   induction2; try rewrite ?InA_cons, ?Hrec, ?Hrec'; intuition; inv; auto.
-  left; order.
   Qed.
 
   Lemma inter_inf :
@@ -440,7 +436,6 @@ Module MakeRaw (X: OrderedType) <: RawSets X.
   Proof.
   induction2; try rewrite ?InA_cons, ?Hrec, ?Hrec'; intuition; inv; auto;
    try sort_inf_in; try order.
-  left; order.
   Qed.
 
   Lemma diff_inf :
diff --git a/theories/MSets/MSetRBT.v b/theories/MSets/MSetRBT.v
index b838495f9..92ad2fcfb 100644
--- a/theories/MSets/MSetRBT.v
+++ b/theories/MSets/MSetRBT.v
@@ -452,7 +452,7 @@ Local Notation Bk := (Node Black).
 Local Hint Immediate MX.eq_sym.
 Local Hint Unfold In lt_tree gt_tree Ok.
 Local Hint Constructors InT bst.
-Local Hint Resolve MX.eq_refl MX.eq_trans MX.lt_trans @ok.
+Local Hint Resolve MX.eq_refl MX.eq_trans MX.lt_trans ok.
 Local Hint Resolve lt_leaf gt_leaf lt_tree_node gt_tree_node.
 Local Hint Resolve lt_tree_not_in lt_tree_trans gt_tree_not_in gt_tree_trans.
 Local Hint Resolve elements_spec2.
diff --git a/theories/MSets/MSetWeakList.v b/theories/MSets/MSetWeakList.v
index fd4114cd4..7c8c5e6de 100644
--- a/theories/MSets/MSetWeakList.v
+++ b/theories/MSets/MSetWeakList.v
@@ -118,16 +118,18 @@ Module MakeRaw (X:DecidableType) <: WRawSets X.
   Notation In := (InA X.eq).
 
   (* TODO: modify proofs in order to avoid these hints *)
-  Hint Resolve (@Equivalence_Reflexive _ _ X.eq_equiv).
-  Hint Immediate (@Equivalence_Symmetric _ _ X.eq_equiv).
-  Hint Resolve (@Equivalence_Transitive _ _ X.eq_equiv).
+  Let eqr:= (@Equivalence_Reflexive _ _ X.eq_equiv).
+  Let eqsym:= (@Equivalence_Symmetric _ _ X.eq_equiv).
+  Let eqtrans:= (@Equivalence_Transitive _ _ X.eq_equiv).
+  Hint Resolve eqr eqtrans.
+  Hint Immediate eqsym.
 
   Definition IsOk := NoDup.
 
   Class Ok (s:t) : Prop := ok : NoDup s.
 
   Hint Unfold Ok.
-  Hint Resolve @ok.
+  Hint Resolve ok.
 
   Instance NoDup_Ok s (nd : NoDup s) : Ok s := { ok := nd }.
 
diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v
index 94d3e97a5..809169a4d 100644
--- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v
+++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v
@@ -354,6 +354,8 @@ Section Z_2nZ.
 
  (* Proof *)
  Context {specs : ZnZ.Specs ops}.
+ 
+ Create HintDb ZnZ.
 
  Hint Resolve
     ZnZ.spec_to_Z
@@ -397,9 +399,9 @@ Section Z_2nZ.
     ZnZ.spec_sqrt
     ZnZ.spec_WO
     ZnZ.spec_OW
-    ZnZ.spec_WW.
-
- Ltac wwauto := unfold ww_to_Z; auto.
+    ZnZ.spec_WW : ZnZ.
+ 
+ Ltac wwauto := unfold ww_to_Z; eauto with ZnZ.
 
  Let wwB := base _ww_digits.
 
@@ -414,7 +416,7 @@ Section Z_2nZ.
  Notation "[[ x ]]" := (zn2z_to_Z wwB to_Z x)  (at level 0, x at level 99).
 
  Let spec_ww_to_Z   : forall x, 0 <= [| x |] < wwB.
- Proof. refine (spec_ww_to_Z w_digits w_to_Z _);auto. Qed.
+ Proof. refine (spec_ww_to_Z w_digits w_to_Z _); wwauto. Qed.
 
  Let spec_ww_of_pos : forall p,
      Zpos p = (Z.of_N (fst (ww_of_pos p)))*wwB + [|(snd (ww_of_pos p))|].
@@ -438,15 +440,15 @@ Section Z_2nZ.
  Proof. reflexivity. Qed.
 
  Let spec_ww_1 : [|ww_1|] = 1.
- Proof. refine (spec_ww_1 w_0 w_1 w_digits w_to_Z _ _);auto. Qed.
+ Proof. refine (spec_ww_1 w_0 w_1 w_digits w_to_Z _ _);wwauto. Qed.
 
  Let spec_ww_Bm1 : [|ww_Bm1|] = wwB - 1.
- Proof. refine (spec_ww_Bm1 w_Bm1 w_digits w_to_Z _);auto. Qed.
+ Proof. refine (spec_ww_Bm1 w_Bm1 w_digits w_to_Z _);wwauto. Qed.
 
  Let spec_ww_compare :
   forall x y, compare x y = Z.compare [|x|] [|y|].
  Proof.
-  refine (spec_ww_compare w_0 w_digits w_to_Z w_compare _ _ _);auto.
+  refine (spec_ww_compare w_0 w_digits w_to_Z w_compare _ _ _);wwauto.
  Qed.
 
  Let spec_ww_eq0 : forall x, eq0 x = true -> [|x|] = 0.
@@ -455,14 +457,14 @@ Section Z_2nZ.
  Let spec_ww_opp_c : forall x, [-|opp_c x|] = -[|x|].
  Proof.
   refine(spec_ww_opp_c w_0 w_0 W0 w_opp_c w_opp_carry w_digits w_to_Z _ _ _ _);
-  auto.
+   wwauto.
  Qed.
 
  Let spec_ww_opp : forall x, [|opp x|] = (-[|x|]) mod wwB.
  Proof.
   refine(spec_ww_opp w_0 w_0 W0 w_opp_c w_opp_carry w_opp
    w_digits w_to_Z _ _ _ _ _);
-  auto.
+  wwauto.
  Qed.
 
  Let spec_ww_opp_carry : forall x, [|opp_carry x|] = wwB - [|x|] - 1.
@@ -473,7 +475,7 @@ Section Z_2nZ.
 
  Let spec_ww_succ_c : forall x, [+|succ_c x|] = [|x|] + 1.
  Proof.
-  refine (spec_ww_succ_c w_0 w_0 ww_1 w_succ_c w_digits w_to_Z _ _ _ _);auto.
+  refine (spec_ww_succ_c w_0 w_0 ww_1 w_succ_c w_digits w_to_Z _ _ _ _);wwauto.
  Qed.
 
  Let spec_ww_add_c  : forall x y, [+|add_c x y|] = [|x|] + [|y|].
@@ -495,7 +497,7 @@ Section Z_2nZ.
 
  Let spec_ww_add : forall x y, [|add x y|] = ([|x|] + [|y|]) mod wwB.
  Proof.
-  refine (spec_ww_add w_add_c w_add w_add_carry w_digits w_to_Z _ _ _ _);auto.
+  refine (spec_ww_add w_add_c w_add w_add_carry w_digits w_to_Z _ _ _ _);wwauto.
  Qed.
 
  Let spec_ww_add_carry : forall x y, [|add_carry x y|]=([|x|]+[|y|]+1)mod wwB.
@@ -608,13 +610,14 @@ Section Z_2nZ.
  Qed.
 
  Let spec_low: forall x,
-  w_to_Z (low x) = [|x|] mod wB.
+  w_to_Z (low x) = [|x|] mod wB. 
   intros x; case x; simpl low.
-    unfold ww_to_Z, w_to_Z, w_0; rewrite ZnZ.spec_0; simpl; auto.
+    unfold ww_to_Z, w_to_Z, w_0; rewrite ZnZ.spec_0; simpl; wwauto.
   intros xh xl; simpl.
   rewrite Z.add_comm; rewrite Z_mod_plus; auto with zarith.
   rewrite Zmod_small; auto with zarith.
-  unfold wB, base; auto with zarith.
+  unfold wB, base; eauto with ZnZ zarith.
+  unfold wB, base; eauto with ZnZ zarith.
  Qed.
 
  Let spec_ww_digits:
@@ -632,7 +635,7 @@ Section Z_2nZ.
  Proof.
  refine (spec_ww_head00 w_0 w_0W
                 w_compare w_head0 w_add2 w_zdigits _ww_zdigits
-                w_to_Z _ _ _ (eq_refl _ww_digits) _ _ _ _); auto.
+                w_to_Z _ _ _ (eq_refl _ww_digits) _ _ _ _); wwauto.
  exact ZnZ.spec_head00.
  exact ZnZ.spec_zdigits.
  Qed.
@@ -715,7 +718,7 @@ refine
       [|a|] = [|q|] * [|b|] + [|r|] /\
       0 <= [|r|] < [|b|].
  Proof.
-  refine (spec_ww_div w_digits ww_1 compare div_gt w_to_Z _ _ _ _);auto.
+  refine (spec_ww_div w_digits ww_1 compare div_gt w_to_Z _ _ _ _);wwauto.
  Qed.
 
  Let spec_ww_mod_gt : forall a b,
@@ -735,7 +738,7 @@ refine
 
  Let spec_ww_mod :  forall a b, 0 < [|b|] -> [|mod_ a b|] = [|a|] mod [|b|].
  Proof.
-  refine (spec_ww_mod w_digits W0 compare mod_gt w_to_Z _ _ _);auto.
+  refine (spec_ww_mod w_digits W0 compare mod_gt w_to_Z _ _ _);wwauto.
  Qed.
 
  Let spec_ww_gcd_gt : forall a b, [|a|] > [|b|] ->
@@ -743,7 +746,7 @@ refine
  Proof.
   refine (@spec_ww_gcd_gt t w_digits W0 w_to_Z _
     w_0 w_0 w_eq0 w_gcd_gt _ww_digits
-  _ gcd_gt_fix _ _ _ _ gcd_cont _);auto.
+  _ gcd_gt_fix _ _ _ _ gcd_cont _);wwauto.
   refine (@spec_ww_gcd_gt_aux t w_digits w_0 w_WW w_0W w_compare w_opp_c w_opp
    w_opp_carry w_sub_c w_sub w_sub_carry w_gcd_gt w_add_mul_div w_head0
    w_div21 div32 _ww_zdigits ww_1 add_mul_div w_zdigits w_to_Z
@@ -752,13 +755,13 @@ refine
   exact ZnZ.spec_zdigits.
   exact spec_ww_add_mul_div.
   refine (@spec_gcd_cont t w_digits ww_1 w_to_Z _ _ w_0 w_1 w_compare
-   _ _);auto.
+   _ _);wwauto.
  Qed.
 
  Let spec_ww_gcd : forall a b, Zis_gcd [|a|] [|b|] [|gcd a b|].
  Proof.
   refine (@spec_ww_gcd t w_digits W0 compare w_to_Z _ _ w_0 w_0 w_eq0 w_gcd_gt
-  _ww_digits _ gcd_gt_fix _ _ _ _ gcd_cont _);auto.
+  _ww_digits _ gcd_gt_fix _ _ _ _ gcd_cont _);wwauto.
   refine (@spec_ww_gcd_gt_aux t w_digits w_0 w_WW w_0W w_compare w_opp_c w_opp
    w_opp_carry w_sub_c w_sub w_sub_carry w_gcd_gt w_add_mul_div w_head0
    w_div21 div32 _ww_zdigits ww_1 add_mul_div w_zdigits w_to_Z
@@ -767,7 +770,7 @@ refine
   exact ZnZ.spec_zdigits.
   exact spec_ww_add_mul_div.
   refine (@spec_gcd_cont t w_digits ww_1 w_to_Z _ _ w_0 w_1 w_compare
-   _ _);auto.
+   _ _);wwauto.
  Qed.
 
  Let spec_ww_is_even : forall x,
@@ -818,6 +821,8 @@ refine
  Proof.
  unfold wB, base; apply Z.pow_pos_nonneg; auto with zarith.
  Qed.
+ 
+ Hint Transparent ww_to_Z.
 
  Let ww_testbit_high n x y : Z.pos w_digits <= n ->
   Z.testbit [|WW x y|] n =
@@ -826,8 +831,8 @@ refine
   intros Hn.
   assert (E : ZnZ.to_Z x = [|WW x y|] / wB).
   { simpl.
-    rewrite Z.div_add_l; auto with zarith.
-    now rewrite Z.div_small, Z.add_0_r. }
+    rewrite Z.div_add_l; eauto with ZnZ zarith.
+    now rewrite Z.div_small, Z.add_0_r; wwauto. }
   rewrite E.
   unfold wB, base. rewrite Z.div_pow2_bits.
   - f_equal; auto with zarith.
@@ -842,7 +847,7 @@ refine
   assert (E : ZnZ.to_Z y = [|WW x y|] mod wB).
   { simpl; symmetry.
     rewrite Z.add_comm, Z.mod_add; auto with zarith.
-    apply Z.mod_small; auto with zarith. }
+    apply Z.mod_small; eauto with ZnZ zarith. }
   rewrite E.
   unfold wB, base. symmetry. apply Z.mod_pow2_bits_low; auto.
  Qed.
diff --git a/theories/Reals/RIneq.v b/theories/Reals/RIneq.v
index 4dea8e07b..bfa975aab 100644
--- a/theories/Reals/RIneq.v
+++ b/theories/Reals/RIneq.v
@@ -409,7 +409,9 @@ Proof.
   rewrite Rplus_assoc; rewrite H; ring.
 Qed.
 
-Hint Resolve (f_equal (A:=R)): real.
+Definition f_equal_R := (f_equal (A:=R)).
+
+Hint Resolve f_equal_R : real.
 
 Lemma Rplus_eq_compat_l : forall r r1 r2, r1 = r2 -> r + r1 = r + r2.
 Proof.
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 5fe3d3f12..38b5703f3 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -34,7 +34,7 @@ let set_typeclass_transparency c local b =
 let _ =
   Typeclasses.register_add_instance_hint
     (fun inst local pri ->
-     let path = try Auto.PathHints [global_of_constr inst] with _ -> Auto.PathAny in
+     let path = try Auto.PathHints [inst] with _ -> Auto.PathAny in
       Flags.silently (fun () ->
 	Auto.add_hints local [typeclasses_db]
 	  (Auto.HintsResolveEntry