- Fix treatment of globality flag for typeclass instance hints (they

  were all declared as global).
- Add possibility to remove hints (Resolve or Immediate only) based on
  the name of the lemma.


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

17 files changed, 188 insertions, 68 deletions

diff --git a/lib/util.ml b/lib/util.ml
index fb271ea421..a8e716e0f3 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -488,6 +488,15 @@ let list_map4 f l1 l2 l3 l4 =
   in
   map (l1,l2,l3,l4)
 
+let rec list_smartfilter f l = match l with
+    [] -> l
+  | h::tl ->
+      let tl' = list_smartfilter f tl in
+	if f h then
+	  if tl' == tl then l
+	  else h :: tl'
+	else tl'
+	  
 let list_index x =
   let rec index_x n = function
     | y::l -> if x = y then n else index_x (succ n) l
diff --git a/lib/util.mli b/lib/util.mli
index 13be5521d6..5248d0e6b1 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -149,6 +149,10 @@ val list_map4 :
 val list_filter_i :
   (int -> 'a -> bool) -> 'a list -> 'a list
 
+(** [list_smartfilter f [a1...an] = List.filter f [a1...an]] but if for all i
+   [f ai = true], then [list_smartfilter f l==l] *)
+val list_smartfilter : ('a -> bool) -> 'a list -> 'a list
+
 (** [list_index] returns the 1st index of an element in a list (counting from 1) *)
 val list_index : 'a -> 'a list -> int
 
diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4
index 2b6759aed0..3139f5759a 100644
--- a/parsing/g_proofs.ml4
+++ b/parsing/g_proofs.ml4
@@ -85,6 +85,8 @@ GEXTEND Gram
       | IDENT "Create"; IDENT "HintDb" ;
 	  id = IDENT ; b = [ "discriminated" -> true | -> false ] ->
 	    VernacCreateHintDb (use_module_locality (), id, b)
+      | IDENT "Remove"; IDENT "Hints"; ids = LIST1 global; dbnames = opt_hintbases ->
+	  VernacRemoveHints (use_module_locality (), dbnames, ids)
       | IDENT "Hint"; local = obsolete_locality; h = hint;
 	  dbnames = opt_hintbases ->
 	  VernacHints (enforce_module_locality local,dbnames, h)
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index e550cfa26a..72a2ba198b 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -562,7 +562,7 @@ GEXTEND Gram
 	 pri = OPT [ "|"; i = natural -> i ] ;
 	 props = [ ":="; "{"; r = record_declaration; "}" -> r |
 	     ":="; c = lconstr -> c | -> CRecord (loc, None, []) ] ->
-	   VernacInstance (false, not (use_non_locality ()),
+	   VernacInstance (false, not (use_section_locality ()),
 			   snd namesup, (fst namesup, expl, t), props, pri)
 
       | IDENT "Existing"; IDENT "Instance"; is = global -> 
@@ -631,7 +631,7 @@ GEXTEND Gram
       | IDENT "Declare"; IDENT "Instance"; namesup = instance_name; ":";
 	 expl = [ "!" -> Glob_term.Implicit | -> Glob_term.Explicit ] ; t = operconstr LEVEL "200";
 	 pri = OPT [ "|"; i = natural -> i ] ->
-	   VernacInstance (true, not (use_non_locality ()),
+	   VernacInstance (true, not (use_section_locality ()),
 			   snd namesup, (fst namesup, expl, t),
 			   CRecord (loc, None, []), pri)
 
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index bba1e1a8fb..956d7eb064 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -795,8 +795,12 @@ let rec pr_vernac = function
         (pr_locality local ++ str "Ltac " ++
         prlist_with_sep (fun () -> fnl() ++ str"with ") pr_tac_body l)
   | VernacCreateHintDb (local,dbname,b) ->
-      hov 1 (pr_locality local ++ str "Create " ++ str "HintDb " ++ 
+      hov 1 (pr_locality local ++ str "Create HintDb " ++ 
 		str dbname ++ (if b then str" discriminated" else mt ()))
+  | VernacRemoveHints (local, dbnames, ids) ->
+      hov 1 (pr_locality local ++ str "Remove Hints " ++
+	       prlist_with_sep spc (fun r -> pr_id (coerce_reference_to_id r)) ids ++ 
+	       pr_opt_hintbases dbnames)
   | VernacHints (local,dbnames,h) ->
       pr_hints local dbnames h pr_constr pr_constr_pattern_expr
   | VernacSyntacticDefinition (id,(ids,c),local,onlyparsing) ->
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 84815e0988..12cccdf0c3 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -22,11 +22,16 @@ open Libobject
 (*i*)
 
 
-let add_instance_hint_ref = ref (fun id pri -> assert false)
+let add_instance_hint_ref = ref (fun id local pri -> assert false)
 let register_add_instance_hint =
   (:=) add_instance_hint_ref
 let add_instance_hint id = !add_instance_hint_ref id
 
+let remove_instance_hint_ref = ref (fun id -> assert false)
+let register_remove_instance_hint =
+  (:=) remove_instance_hint_ref
+let remove_instance_hint id = !remove_instance_hint_ref id
+
 let set_typeclass_transparency_ref = ref (fun id pri -> assert false)
 let register_set_typeclass_transparency =
   (:=) set_typeclass_transparency_ref
@@ -212,50 +217,77 @@ let add_class cl =
  * instances persistent object
  *)
 
-let load_instance (_,inst) = 
+type instance_action = 
+  | AddInstance
+  | RemoveInstance
+
+let load_instance inst = 
   let insts = 
     try Gmap.find inst.is_class !instances 
     with Not_found -> Gmap.empty in
   let insts = Gmap.add inst.is_impl inst insts in
   instances := Gmap.add inst.is_class insts !instances
 
-let cache_instance = load_instance
+let remove_instance inst =
+  let insts = 
+    try Gmap.find inst.is_class !instances 
+    with Not_found -> assert false in
+  let insts = Gmap.remove inst.is_impl insts in
+  instances := Gmap.add inst.is_class insts !instances
+
+let cache_instance (_, (action, i)) =
+  match action with 
+  | AddInstance -> load_instance i
+  | RemoveInstance -> remove_instance i      
 
-let subst_instance (subst,inst) = 
+let subst_instance (subst, (action, inst)) = action,
   { inst with 
       is_class = fst (subst_global subst inst.is_class);
       is_impl = fst (subst_global subst inst.is_impl) }
 
-let discharge_instance (_,inst) =
+let discharge_instance (_, (action, inst)) =
   if inst.is_global <= 0 then None
-  else Some 
+  else Some (action,
     { inst with 
       is_global = pred inst.is_global;
       is_class = Lib.discharge_global inst.is_class;
-      is_impl = Lib.discharge_global inst.is_impl }
+      is_impl = Lib.discharge_global inst.is_impl })
     
-let rebuild_instance inst =
-  add_instance_hint inst.is_impl inst.is_pri;
-  inst
 
-let classify_instance inst =
-  if inst.is_global = -1 then Dispose
-  else Substitute inst
+let is_local i = i.is_global = -1
+
+let rebuild_instance (action, inst) =
+  if action = AddInstance then
+    add_instance_hint inst.is_impl (is_local inst) inst.is_pri;
+  (action, inst)
+
+let classify_instance (action, inst) =
+  if is_local inst then Dispose
+  else Substitute (action, inst)
+
+let load_instance (_, (action, inst) as ai) =
+  cache_instance ai;
+  if action = AddInstance then
+    add_instance_hint inst.is_impl (is_local inst) inst.is_pri
 
 let instance_input =
   declare_object
     { (default_object "type classes instances state") with
       cache_function = cache_instance;
-      load_function = (fun _ -> load_instance);
-      open_function = (fun _ -> load_instance);
+      load_function = (fun _ x -> cache_instance x);
+      open_function = (fun _ x -> cache_instance x);
       classify_function = classify_instance;
       discharge_function = discharge_instance;
       rebuild_function = rebuild_instance;
       subst_function = subst_instance }
 
 let add_instance i =
-  Lib.add_anonymous_leaf (instance_input i);
-  add_instance_hint i.is_impl i.is_pri
+  Lib.add_anonymous_leaf (instance_input (AddInstance, i));
+  add_instance_hint i.is_impl (is_local i) i.is_pri
+
+let remove_instance i =
+  Lib.add_anonymous_leaf (instance_input (RemoveInstance, i));
+  remove_instance_hint i.is_impl
 
 open Declarations
 
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index 800deefda4..3fa1981a3c 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -52,6 +52,7 @@ val add_inductive_class : inductive -> unit
 
 val new_instance : typeclass -> int option -> bool -> global_reference -> instance
 val add_instance : instance -> unit
+val remove_instance : instance -> unit
 
 val class_info : global_reference -> typeclass (** raises a UserError if not a class *)
 
@@ -89,8 +90,10 @@ val resolve_one_typeclass : env -> evar_map -> types -> open_constr
 val register_set_typeclass_transparency : (evaluable_global_reference -> bool -> unit) -> unit
 val set_typeclass_transparency : evaluable_global_reference -> bool -> unit
 
-val register_add_instance_hint : (global_reference -> int option -> unit) -> unit
-val add_instance_hint : global_reference -> int option -> 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 : global_reference -> bool -> int option -> unit
+val remove_instance_hint : global_reference -> unit
 
 val solve_instanciations_problem : (env -> evar_map -> bool -> bool -> bool -> evar_map) ref
 val solve_instanciation_problem : (env -> evar_map -> types -> open_constr) ref
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 8a05736ca4..f4985f40e1 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -57,6 +57,7 @@ type auto_tactic =
 type pri_auto_tactic = {
   pri  : int;            (* A number between 0 and 4, 4 = lower priority *)
   pat  : constr_pattern option; (* A pattern for the concl of the Goal *)
+  name  : global_reference option; (* A potential name to refer to the hint *) 
   code : auto_tactic     (* the tactic to apply when the concl matches pat *)
 }
 
@@ -213,6 +214,20 @@ module Hint_db = struct
 
   let add_list l db = List.fold_right add_one l db
 
+  let remove_sdl p sdl = list_smartfilter p sdl 
+  let remove_he st p (sl1, sl2, dn as he) =
+    let sl1' = remove_sdl p sl1 and sl2' = remove_sdl p sl2 in
+      if sl1' == sl1 && sl2' == sl2 then he
+      else rebuild_dn st (sl1', sl2', dn)
+
+  let remove_list grs db =
+    let filter h = match h.name with None -> true | Some gr -> not (List.mem gr grs) in
+    let hintmap = Constr_map.map (remove_he db.hintdb_state filter) db.hintdb_map in
+    let hintnopat = list_smartfilter (fun (ge, sd) -> filter sd) db.hintdb_nopat in
+      { db with hintdb_map = hintmap; hintdb_nopat = hintnopat }
+
+  let remove_one gr db = remove_list [gr] db
+
   let iter f db =
     f None (List.map snd db.hintdb_nopat);
     Constr_map.iter (fun k (l,l',_) -> f (Some k) (l@l')) db.hintdb_map
@@ -280,7 +295,9 @@ let try_head_pattern c =
 
 let dummy_goal = Goal.V82.dummy_goal
 
-let make_exact_entry sigma pri (c,cty) =
+let name_of_constr c = try Some (global_of_constr c) with Not_found -> None
+
+let make_exact_entry sigma pri ?name (c,cty) =
   let cty = strip_outer_cast cty in
     match kind_of_term cty with
     | Prod _ -> failwith "make_exact_entry"
@@ -293,9 +310,10 @@ let make_exact_entry sigma pri (c,cty) =
           (Some hd,
 	  { pri = (match pri with None -> 0 | Some p -> p);
 	    pat = Some pat;
+	    name = name;
 	    code = Give_exact c })
 
-let make_apply_entry env sigma (eapply,hnf,verbose) pri (c,cty) =
+let make_apply_entry env sigma (eapply,hnf,verbose) pri ?name (c,cty) =
   let cty = if hnf then hnf_constr env sigma cty else cty in
     match kind_of_term cty with
     | Prod _ ->
@@ -310,6 +328,7 @@ let make_apply_entry env sigma (eapply,hnf,verbose) pri (c,cty) =
 	  (Some hd,
           { pri = (match pri with None -> nb_hyp cty | Some p -> p);
             pat = Some pat;
+	    name = name;
             code = Res_pf(c,{ce with env=empty_env}) })
 	else begin
 	  if not eapply then failwith "make_apply_entry";
@@ -319,6 +338,7 @@ let make_apply_entry env sigma (eapply,hnf,verbose) pri (c,cty) =
           (Some hd,
             { pri = (match pri with None -> nb_hyp cty + nmiss | Some p -> p);
               pat = Some pat;
+	      name = name;
               code = ERes_pf(c,{ce with env=empty_env}) })
         end
     | _ -> failwith "make_apply_entry"
@@ -327,12 +347,12 @@ let make_apply_entry env sigma (eapply,hnf,verbose) pri (c,cty) =
    c is a constr
    cty is the type of constr *)
 
-let make_resolves env sigma flags pri c =
+let make_resolves env sigma flags pri ?name c =
   let cty = type_of env sigma c in
   let ents =
     map_succeed
       (fun f -> f (c,cty))
-      [make_exact_entry sigma pri; make_apply_entry env sigma flags pri]
+      [make_exact_entry sigma pri ?name; make_apply_entry env sigma flags pri ?name]
   in
   if ents = [] then
     errorlabstrm "Hint"
@@ -344,7 +364,7 @@ let make_resolves env sigma flags pri c =
 (* used to add an hypothesis to the local hint database *)
 let make_resolve_hyp env sigma (hname,_,htyp) =
   try
-    [make_apply_entry env sigma (true, true, false) None
+    [make_apply_entry env sigma (true, true, false) None ~name:(VarRef hname)
        (mkVar hname, htyp)]
   with
     | Failure _ -> []
@@ -352,24 +372,28 @@ let make_resolve_hyp env sigma (hname,_,htyp) =
 
 (* REM : in most cases hintname = id *)
 let make_unfold eref =
-  (Some (global_of_evaluable_reference eref),
+  let g = global_of_evaluable_reference eref in
+  (Some g,
    { pri = 4;
      pat = None;
+     name = Some g;
      code = Unfold_nth eref })
 
 let make_extern pri pat tacast =
   let hdconstr = Option.map try_head_pattern pat in
   (hdconstr,
-   { pri=pri;
+   { pri = pri;
      pat = pat;
-     code= Extern tacast })
+     name = None;
+     code = Extern tacast })
 
-let make_trivial env sigma c =
+let make_trivial env sigma ?name c =
   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
   (Some hd, { pri=1;
          pat = Some (snd (Pattern.pattern_of_constr sigma (clenv_type ce)));
+	 name = name;
          code=Res_pf_THEN_trivial_fail(c,{ce with env=empty_env}) })
 
 open Vernacexpr
@@ -401,15 +425,22 @@ let add_transparency dbname grs b =
       st grs
   in searchtable_add (dbname, Hint_db.set_transparent_state db st')
 
+let remove_hints dbname hintlist grs =
+  let db = get_db dbname in
+  let db' = Hint_db.remove_list grs db in
+    searchtable_add (dbname, db')
+
 type hint_action = | CreateDB of bool * transparent_state
 		   | AddTransparency of evaluable_global_reference list * bool
-		   | AddTactic of (global_reference option * pri_auto_tactic) list
+		   | AddHints of (global_reference option * pri_auto_tactic) list
+		   | RemoveHints of global_reference list
 
 let cache_autohint (_,(local,name,hints)) =
   match hints with
   | CreateDB (b, st) -> searchtable_add (name, Hint_db.empty st b)
   | AddTransparency (grs, b) -> add_transparency name grs b
-  | AddTactic hints -> add_hint name hints
+  | AddHints hints -> add_hint name hints
+  | RemoveHints grs -> remove_hints name hints grs
 
 let forward_subst_tactic =
   ref (fun _ -> failwith "subst_tactic is not installed for auto")
@@ -482,13 +513,17 @@ let subst_autohint (subst,(local,name,hintlist as obj)) =
     | AddTransparency (grs, b) ->
 	let grs' = list_smartmap (subst_evaluable_reference subst) grs in
 	  if grs==grs' then obj else (local, name, AddTransparency (grs', b))
-    | AddTactic hintlist ->
+    | AddHints hintlist ->
 	let hintlist' = list_smartmap subst_hint hintlist in
 	  if hintlist' == hintlist then obj else
-	    (local,name,AddTactic hintlist')
+	    (local,name,AddHints hintlist')
+    | RemoveHints grs ->
+	let grs' = list_smartmap (fun x -> fst (subst_global subst x)) grs in
+	  if grs==grs' then obj else (local, name, RemoveHints grs')
+
 
 let classify_autohint ((local,name,hintlist) as obj) =
-  if local or hintlist = (AddTactic []) then Dispose else Substitute obj
+  if local or hintlist = (AddHints []) then Dispose else Substitute obj
 
 let inAutoHint =
   declare_object {(default_object "AUTOHINT") with
@@ -501,6 +536,13 @@ let inAutoHint =
 let create_hint_db l n st b =
   Lib.add_anonymous_leaf (inAutoHint (l,n,CreateDB (b, st)))
 
+let remove_hints local dbnames grs =
+  let dbnames = if dbnames = [] then ["core"] else dbnames in
+    List.iter
+      (fun dbname ->
+	 Lib.add_anonymous_leaf (inAutoHint(local, dbname, RemoveHints grs)))
+      dbnames
+
 (**************************************************************************)
 (*                     The "Hint" vernacular command                      *)
 (**************************************************************************)
@@ -509,16 +551,16 @@ let add_resolves env sigma clist local dbnames =
     (fun dbname ->
        Lib.add_anonymous_leaf
 	 (inAutoHint
-	    (local,dbname, AddTactic
-     	      (List.flatten (List.map (fun (x, hnf, y) ->
-		make_resolves env sigma (true,hnf,Flags.is_verbose()) x y) clist)))))
+	    (local,dbname, AddHints
+     	      (List.flatten (List.map (fun (x, hnf, name, y) ->
+		make_resolves env sigma (true,hnf,Flags.is_verbose()) x ?name y) clist)))))
     dbnames
 
 
 let add_unfolds l local dbnames =
   List.iter
     (fun dbname -> Lib.add_anonymous_leaf
-       (inAutoHint (local,dbname, AddTactic (List.map make_unfold l))))
+       (inAutoHint (local,dbname, AddHints (List.map make_unfold l))))
     dbnames
 
 let add_transparency l b local dbnames =
@@ -539,10 +581,10 @@ let add_extern pri pat tacast local dbname =
 	      (str "The meta-variable ?" ++ Ppconstr.pr_patvar i ++ str" is not bound.")
 	| []  ->
 	    Lib.add_anonymous_leaf
-	      (inAutoHint(local,dbname, AddTactic [make_extern pri (Some pat) tacast])))
+	      (inAutoHint(local,dbname, AddHints [make_extern pri (Some pat) tacast])))
     | None ->
 	Lib.add_anonymous_leaf
-	  (inAutoHint(local,dbname, AddTactic [make_extern pri None tacast]))
+	  (inAutoHint(local,dbname, AddHints [make_extern pri None tacast]))
 
 let add_externs pri pat tacast local dbnames =
   List.iter (add_extern pri pat tacast local) dbnames
@@ -551,7 +593,7 @@ let add_trivials env sigma l local dbnames =
   List.iter
     (fun dbname ->
        Lib.add_anonymous_leaf (
-	 inAutoHint(local,dbname, AddTactic (List.map (make_trivial env sigma) l))))
+	 inAutoHint(local,dbname, AddHints (List.map (fun (name, c) -> make_trivial env sigma ?name c) l))))
     dbnames
 
 let forward_intern_tac =
@@ -560,8 +602,8 @@ let forward_intern_tac =
 let set_extern_intern_tac f = forward_intern_tac := f
 
 type hints_entry =
-  | HintsResolveEntry of (int option * bool * constr) list
-  | HintsImmediateEntry of constr list
+  | HintsResolveEntry of (int option * bool * global_reference option * constr) list
+  | HintsImmediateEntry of (global_reference option * constr) list
   | HintsUnfoldEntry of evaluable_global_reference list
   | HintsTransparencyEntry of evaluable_global_reference list * bool
   | HintsExternEntry of
@@ -602,6 +644,11 @@ let prepare_hint env (sigma,c) =
       mkNamedLambda id t (iter (replace_term evar (mkVar id) c)) in
   iter c
 
+let name_of_constr_expr c =
+  match c with
+  | Topconstr.CRef r -> (try Some (global r) with _ -> None)
+  | _ -> None 
+      
 let interp_hints h =
   let f c =
     let evd,c = Constrintern.interp_open_constr Evd.empty (Global.env()) c in
@@ -613,17 +660,20 @@ let interp_hints h =
     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, name_of_constr_expr c, f c) in
+  let fi c = name_of_constr_expr c, f c in
   let fp = Constrintern.intern_constr_pattern Evd.empty (Global.env()) in
   match h with
-  | HintsResolve lhints -> HintsResolveEntry (List.map (on_pi3 f) lhints)
-  | HintsImmediate lhints -> HintsImmediateEntry (List.map f lhints)
+  | HintsResolve lhints -> HintsResolveEntry (List.map fres lhints)
+  | HintsImmediate lhints -> HintsImmediateEntry (List.map fi lhints)
   | HintsUnfold lhints -> HintsUnfoldEntry (List.map fr lhints)
   | HintsTransparency (lhints, b) ->
       HintsTransparencyEntry (List.map fr lhints, b)
   | HintsConstructors lqid ->
       let constr_hints_of_ind qid =
         let ind = global_inductive_with_alias qid in
-        list_tabulate (fun i -> None, true, mkConstruct (ind,i+1))
+        list_tabulate (fun i -> let c = (ind,i+1) in
+			 None, true, Some (ConstructRef c), mkConstruct c)
 	  (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 73249d43ad..cd8808bff2 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.mli
@@ -35,6 +35,7 @@ open Glob_term
 type pri_auto_tactic = {
   pri   : int;            (** A number between 0 and 4, 4 = lower priority *)
   pat   : constr_pattern option; (** A pattern for the concl of the Goal *)
+  name  : global_reference option; (** A potential name to refer to the hint *) 
   code  : auto_tactic;    (** the tactic to apply when the concl matches pat *)
 }
 
@@ -56,6 +57,8 @@ module Hint_db :
     val map_auto : global_reference * constr -> t -> pri_auto_tactic list
     val add_one : hint_entry -> t -> t
     val add_list : (hint_entry) list -> t -> t
+    val remove_one : global_reference -> t -> t
+    val remove_list : global_reference list -> t -> t
     val iter : (global_reference option -> stored_data list -> unit) -> t -> unit
 
     val use_dn : t -> bool
@@ -70,8 +73,8 @@ type hint_db_name = string
 type hint_db = Hint_db.t
 
 type hints_entry =
-  | HintsResolveEntry of (int option * bool * constr) list
-  | HintsImmediateEntry of constr list
+  | HintsResolveEntry of (int option * bool * global_reference option * constr) list
+  | HintsImmediateEntry of (global_reference option * constr) list
   | HintsUnfoldEntry of evaluable_global_reference list
   | HintsTransparencyEntry of evaluable_global_reference list * bool
   | HintsExternEntry of
@@ -90,6 +93,8 @@ val searchtable_add : (hint_db_name * hint_db) -> unit
 
 val create_hint_db : bool -> hint_db_name -> transparent_state -> bool -> unit
 
+val remove_hints : bool -> hint_db_name list -> global_reference list -> unit
+
 val current_db_names : unit -> hint_db_name list
 
 val interp_hints : hints_expr -> hints_entry
@@ -112,7 +117,7 @@ val print_hint_db : Hint_db.t -> unit
    [c] is the term given as an exact proof to solve the goal;
    [ctyp] is the type of [c]. *)
 
-val make_exact_entry : evar_map -> int option -> constr * constr -> hint_entry
+val make_exact_entry : evar_map -> int option -> ?name:global_reference -> constr * constr -> hint_entry
 
 (** [make_apply_entry (eapply,hnf,verbose) pri (c,cty)].
    [eapply] is true if this hint will be used only with EApply;
@@ -122,8 +127,8 @@ val make_exact_entry : evar_map -> int option -> constr * constr -> hint_entry
    [cty] is the type of [c]. *)
 
 val make_apply_entry :
-  env -> evar_map -> bool * bool * bool -> int option -> constr * constr
-      -> hint_entry
+  env -> evar_map -> bool * bool * bool -> int option -> ?name:global_reference -> 
+  constr * constr -> hint_entry
 
 (** A constr which is Hint'ed will be:
    - (1) used as an Exact, if it does not start with a product
@@ -133,8 +138,8 @@ val make_apply_entry :
          has missing arguments. *)
 
 val make_resolves :
-  env -> evar_map -> bool * bool * bool -> int option -> constr ->
-      hint_entry list
+  env -> evar_map -> bool * bool * bool -> int option -> ?name:global_reference -> 
+  constr -> hint_entry list
 
 (** [make_resolve_hyp hname htyp].
    used to add an hypothesis to the local hint database;
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 7b2bf08cb7..bbeb9425e1 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -187,6 +187,17 @@ END
 
 open Autorewrite
 
+let pr_orient _prc _prlc _prt = function
+  | true -> Pp.mt ()
+  | false -> Pp.str " <-"
+
+let pr_orient_string _prc _prlc _prt (orient, s) =
+  pr_orient _prc _prlc _prt orient ++ Pp.spc () ++ Pp.str s
+
+ARGUMENT EXTEND orient_string TYPED AS (bool * string) PRINTED BY pr_orient_string
+| [ orient(r) preident(i) ] -> [ r, i ]
+END
+
 TACTIC EXTEND autorewrite
 | [ "autorewrite" "with" ne_preident_list(l) in_arg_hyp(cl) ] ->
     [ auto_multi_rewrite  l (glob_in_arg_hyp_to_clause  cl) ]
@@ -275,7 +286,7 @@ 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,c)
+  (pri,true,None,c)
 
 let add_hints_iff l2r lc n bl =
   Auto.add_hints true bl
diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4
index 89a8a5389f..127a61db5e 100644
--- a/tactics/rewrite.ml4
+++ b/tactics/rewrite.ml4
@@ -1342,7 +1342,7 @@ let declare_an_instance n s args =
 let declare_instance a aeq n s = declare_an_instance n s [a;aeq]
 
 let anew_instance binders instance fields =
-  new_instance binders instance (CRecord (dummy_loc,None,fields)) ~generalize:false None
+  new_instance binders instance (CRecord (dummy_loc,None,fields)) ~global:true ~generalize:false None
 
 let declare_instance_refl binders a aeq n lemma =
   let instance = declare_instance a aeq (add_suffix n "_Reflexive") "Coq.Classes.RelationClasses.Reflexive"
diff --git a/theories/FSets/FMapFacts.v b/theories/FSets/FMapFacts.v
index 80884c527a..7272421af7 100644
--- a/theories/FSets/FMapFacts.v
+++ b/theories/FSets/FMapFacts.v
@@ -759,7 +759,6 @@ Module WProperties_fun (E:DecidableType)(M:WSfun E).
   Notation eqk := (@eq_key elt).
 
   Instance eqk_equiv : Equivalence eqk.
-  Proof. split; repeat red; eauto. Qed.
 
   Instance eqke_equiv : Equivalence eqke.
   Proof.
diff --git a/theories/Structures/OrderedType.v b/theories/Structures/OrderedType.v
index 6b9007fdd3..c21d4fa0f4 100644
--- a/theories/Structures/OrderedType.v
+++ b/theories/Structures/OrderedType.v
@@ -315,17 +315,12 @@ Module KeyOrderedType(O:OrderedType).
   Hint Resolve ltk_trans ltk_not_eqk ltk_not_eqke.
   Hint Immediate eqk_sym eqke_sym.
 
-  Global Instance eqk_equiv : Equivalence eqk.
-  Proof. split; eauto. Qed.
+  Global Instance eqk_equiv : Equivalence eqk. 
 
   Global Instance eqke_equiv : Equivalence eqke.
   Proof. split; eauto. Qed.
 
   Global Instance ltk_strorder : StrictOrder ltk.
-  Proof.
-   split; eauto.
-   intros (x,e); compute; apply (StrictOrder_Irreflexive x).
-  Qed.
 
   Global Instance ltk_compat : Proper (eqk==>eqk==>iff) ltk.
   Proof.
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 3084da768a..34b023d6f0 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -36,11 +36,11 @@ let set_typeclass_transparency c b =
     
 let _ =
   Typeclasses.register_add_instance_hint
-    (fun inst pri ->
+    (fun inst local pri ->
       Flags.silently (fun () ->
-	Auto.add_hints false [typeclasses_db]
+	Auto.add_hints local [typeclasses_db]
 	  (Auto.HintsResolveEntry
-	      [pri, false, constr_of_global inst])) ());
+	     [pri, false, Some inst, constr_of_global inst])) ());
   Typeclasses.register_set_typeclass_transparency set_typeclass_transparency
     
 let declare_class g =
@@ -180,7 +180,7 @@ let new_instance ?(abstract=false) ?(global=false) ctx (instid, bk, cl) props
 	Evarutil.check_evars env Evd.empty !evars termtype;
 	let cst = Declare.declare_constant ~internal:Declare.KernelSilent id
 	  (Entries.ParameterEntry (termtype,None), Decl_kinds.IsAssumption Decl_kinds.Logical)
-	in instance_hook k None false imps ?hook (ConstRef cst); id
+	in instance_hook k None global imps ?hook (ConstRef cst); id
       end
     else
       begin
diff --git a/toplevel/ide_blob.ml b/toplevel/ide_blob.ml
index 7e7834743f..a4c4b1d9fd 100644
--- a/toplevel/ide_blob.ml
+++ b/toplevel/ide_blob.ml
@@ -117,6 +117,7 @@ let rec attribute_of_vernac_command = function
   (* Commands *)
   | VernacDeclareTacticDefinition _ -> []
   | VernacCreateHintDb _ -> []
+  | VernacRemoveHints _ -> []
   | VernacHints _ -> []
   | VernacSyntacticDefinition _ -> []
   | VernacDeclareImplicits _ -> []
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index ca4a82ea69..e3d3d20326 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -782,6 +782,9 @@ let vernac_declare_tactic_definition (local,x,def) =
 let vernac_create_hintdb local id b =
   Auto.create_hint_db local id full_transparent_state b
 
+let vernac_remove_hints local dbs ids =
+  Auto.remove_hints local dbs (List.map Smartlocate.global_with_alias ids)
+
 let vernac_hints local lb h =
   Auto.add_hints local lb (Auto.interp_hints h)
 
@@ -1396,6 +1399,7 @@ let interp c = match c with
   (* Commands *)
   | VernacDeclareTacticDefinition def -> vernac_declare_tactic_definition def
   | VernacCreateHintDb (local,dbname,b) -> vernac_create_hintdb local dbname b
+  | VernacRemoveHints (local,dbnames,ids) -> vernac_remove_hints local dbnames ids
   | VernacHints (local,dbnames,hints) -> vernac_hints local dbnames hints
   | VernacSyntacticDefinition (id,c,l,b) ->vernac_syntactic_definition id c l b
   | VernacDeclareImplicits (local,qid,l) ->vernac_declare_implicits local qid l
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index ac3b3964ab..3b9bf9a55f 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -302,6 +302,7 @@ type vernac_expr =
   | VernacDeclareTacticDefinition of
       (locality_flag * rec_flag * (reference * bool * raw_tactic_expr) list)
   | VernacCreateHintDb of locality_flag * string * bool
+  | VernacRemoveHints of locality_flag * string list * reference list
   | VernacHints of locality_flag * string list * hints_expr
   | VernacSyntacticDefinition of identifier located * (identifier list * constr_expr) *
       locality_flag * onlyparsing_flag