Merge subinstances branch by me and Tom Prince.

This adds two experimental features to the typeclass implementation:
- Path cuts: a way to specify through regular expressions on instance names
search pathes that should be avoided (e.g. [proper_flip proper_flip]).
Regular expression matching is implemented through naïve derivatives.
- Forward hints for subclasses: e.g. [Equivalence -> Reflexive] is no
longer applied backwards, but introducing a specific [Equivalence] in the
environment register a [Reflexive] hint as well. Currently not
backwards-compatible, the next patch will allow to specify direction
of subclasses hints.

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

6 files changed, 347 insertions, 102 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index db2524c30..e15c30a3b 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -54,10 +54,22 @@ type 'a auto_tactic =
   | Unfold_nth of evaluable_global_reference       (* Hint Unfold *)
   | Extern     of glob_tactic_expr       (* Hint Extern *)
 
+type hints_path_atom = 
+  | PathHints of global_reference list
+  | PathAny
+
+type hints_path =
+  | PathAtom of hints_path_atom
+  | PathStar of hints_path
+  | PathSeq of hints_path * hints_path
+  | PathOr of hints_path * hints_path
+  | PathEmpty
+  | PathEpsilon
+
 type 'a gen_auto_tactic = {
   pri  : int;            (* A number lower is higher 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 *)
+  name  : hints_path_atom; (* A potential name to refer to the hint *) 
   code : 'a auto_tactic     (* the tactic to apply when the concl matches pat *)
 }
 
@@ -80,18 +92,18 @@ let insert v l =
   insrec l
 
 (* Nov 98 -- Papageno *)
-(* Les Hints sont ré-organisés en plusieurs databases.
+(* Les Hints sont ré-organisés en plusieurs databases.
 
-  La table impérative "searchtable", de type "hint_db_table",
-   associe une database (hint_db) à chaque nom.
+  La table impérative "searchtable", de type "hint_db_table",
+   associe une database (hint_db) à chaque nom.
 
   Une hint_db est une table d'association fonctionelle constr -> search_entry
-  Le constr correspond à la constante de tête de la conclusion.
+  Le constr correspond à la constante de tête de la conclusion.
 
   Une search_entry est un triplet comprenant :
-     - la liste des tactiques qui n'ont pas de pattern associé
+     - la liste des tactiques qui n'ont pas de pattern associé
      - la liste des tactiques qui ont un pattern
-     - un discrimination net borné (Btermdn.t) constitué de tous les
+     - un discrimination net borné (Btermdn.t) constitué de tous les
        patterns de la seconde liste de tactiques *)
 
 type stored_data = int * pri_auto_tactic
@@ -137,7 +149,9 @@ let eq_pri_auto_tactic (_, x) (_, y) =
 let add_tac pat t st (l,l',dn) =
   match pat with
   | None -> if not (List.exists (eq_pri_auto_tactic t) l) then (insert t l, l', dn) else (l, l', dn)
-  | Some pat -> if not (List.exists (eq_pri_auto_tactic t) l') then (l, insert t l', Bounded_net.add st dn (pat,t)) else (l, l', dn)
+  | Some pat -> 
+    if not (List.exists (eq_pri_auto_tactic t) l') 
+    then (l, insert t l', Bounded_net.add st dn (pat,t)) else (l, l', dn)
 
 let rebuild_dn st ((l,l',dn) : search_entry) =
   (l, l', List.fold_left (fun dn (id, t) -> Bounded_net.add (Some st) dn (Option.get t.pat, (id, t)))
@@ -173,10 +187,119 @@ let translate_hint (go,p) =
   in
   (go,{ p with code = code })
 
+let path_matches hp hints =
+  let rec aux hp hints k =
+    match hp, hints with
+    | PathAtom _, [] -> false
+    | PathAtom PathAny, (_ :: hints') -> k hints'
+    | PathAtom p, (h :: hints') -> 
+      if p = h then k hints' else false
+    | PathStar hp', hints -> 
+      k hints || aux hp' hints (fun hints' -> aux hp hints' k)
+    | PathSeq (hp, hp'), hints -> 
+      aux hp hints (fun hints' -> aux hp' hints' k)
+    | PathOr (hp, hp'), hints ->
+      aux hp hints k || aux hp' hints k
+    | PathEmpty, _ -> false
+    | PathEpsilon, hints -> k hints
+  in aux hp hints (fun hints' -> true)
+
+let rec matches_epsilon = function
+  | PathAtom _ -> false
+  | PathStar _ -> true
+  | PathSeq (p, p') -> matches_epsilon p && matches_epsilon p'
+  | PathOr (p, p') -> matches_epsilon p || matches_epsilon p'
+  | PathEmpty -> false
+  | PathEpsilon -> true
+
+let rec is_empty = function
+  | PathAtom _ -> false
+  | PathStar _ -> false
+  | PathSeq (p, p') -> is_empty p || is_empty p'
+  | PathOr (p, p') -> matches_epsilon p && matches_epsilon p'
+  | PathEmpty -> true
+  | PathEpsilon -> false
+
+let rec path_derivate hp hint =
+  let rec derivate_atoms hints hints' =
+    match hints, hints' with
+    | gr :: grs, gr' :: grs' when gr = gr' -> derivate_atoms grs grs'
+    | [], [] -> PathEpsilon
+    | [], hints -> PathEmpty
+    | grs, [] -> PathAtom (PathHints grs)
+    | _, _ -> PathEmpty 
+  in
+    match hp with
+    | PathAtom PathAny -> PathEpsilon
+    | PathAtom (PathHints grs) -> 
+      (match grs, hint with
+       | h :: hints, PathAny -> PathEmpty
+       | hints, PathHints hints' -> derivate_atoms hints hints'
+       | _, _ -> assert false)
+    | PathStar p -> if path_matches p [hint] then hp else PathEpsilon
+    | PathSeq (hp, hp') ->
+      let hpder = path_derivate hp hint in
+	if matches_epsilon hp then 
+	  PathOr (PathSeq (hpder, hp'), path_derivate hp' hint)
+	else if is_empty hpder then PathEmpty 
+	else PathSeq (hpder, hp')
+    | PathOr (hp, hp') ->
+      PathOr (path_derivate hp hint, path_derivate hp' hint)
+    | PathEmpty -> PathEmpty
+    | PathEpsilon -> PathEmpty
+
+let rec normalize_path h =
+  match h with
+  | PathStar PathEpsilon -> PathEpsilon
+  | PathSeq (PathEmpty, _) | PathSeq (_, PathEmpty) -> PathEmpty
+  | PathSeq (PathEpsilon, p) | PathSeq (p, PathEpsilon) -> normalize_path p
+  | PathOr (PathEmpty, p) | PathOr (p, PathEmpty) -> normalize_path p
+  | PathOr (p, q) -> 
+    let p', q' = normalize_path p, normalize_path q in
+      if p = p' && q = q' then h
+      else normalize_path (PathOr (p', q'))
+  | PathSeq (p, q) -> 
+    let p', q' = normalize_path p, normalize_path q in
+      if p = p' && q = q' then h
+      else normalize_path (PathSeq (p', q'))
+  | _ -> h
+
+let path_derivate hp hint = normalize_path (path_derivate hp hint)
+
+let rec pp_hints_path = function
+  | PathAtom (PathAny) -> str"."
+  | PathAtom (PathHints grs) -> prlist_with_sep pr_spc pr_global grs
+  | PathStar p -> str "(" ++ pp_hints_path p ++ str")*"
+  | PathSeq (p, p') -> pp_hints_path p ++ str" ; " ++ pp_hints_path p'
+  | PathOr (p, p') -> 
+    str "(" ++ pp_hints_path p ++ spc () ++ str"|" ++ spc () ++ pp_hints_path p' ++ str ")"
+  | PathEmpty -> str"Ø"
+  | PathEpsilon -> str"ε"
+
+let rec subst_hints_path subst hp =
+  match hp with
+  | PathAtom PathAny -> hp
+  | PathAtom (PathHints grs) -> 
+    let gr' gr = fst (subst_global subst gr) in
+    let grs' = list_smartmap gr' grs in
+      if grs' == grs then hp else PathAtom (PathHints grs')
+  | PathStar p -> let p' = subst_hints_path subst p in
+      if p' == p then hp else PathStar p'
+  | PathSeq (p, q) ->
+    let p' = subst_hints_path subst p in
+    let q' = subst_hints_path subst q in
+      if p' == p && q' == q then hp else PathSeq (p', q')
+  | PathOr (p, q) ->
+    let p' = subst_hints_path subst p in
+    let q' = subst_hints_path subst q in
+      if p' == p && q' == q then hp else PathOr (p', q')
+  | _ -> hp
+
 module Hint_db = struct
 
   type t = {
     hintdb_state : Names.transparent_state;
+    hintdb_cut : hints_path;
     hintdb_unfolds : Idset.t * Cset.t;
     mutable hintdb_max_id : int;
     use_dn : bool;
@@ -190,6 +313,7 @@ module Hint_db = struct
     let h = t.hintdb_max_id in t.hintdb_max_id <- succ t.hintdb_max_id; h
 
   let empty st use_dn = { hintdb_state = st;
+			  hintdb_cut = PathEmpty;
 			  hintdb_unfolds = (Idset.empty, Cset.empty);
 			  hintdb_max_id = 0;
 			  use_dn = use_dn;
@@ -199,7 +323,7 @@ module Hint_db = struct
   let find key db =
     try Constr_map.find key db.hintdb_map
     with Not_found -> empty_se
-
+ 
   let map_none db =
     List.map snd (Sort.merge pri_order (List.map snd db.hintdb_nopat) [])
     
@@ -271,7 +395,7 @@ module Hint_db = struct
       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 filter (_, h) = match h.name with PathHints [gr] -> not (List.mem gr grs) | _ -> true 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 }
@@ -279,8 +403,8 @@ module Hint_db = struct
   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
+    f None (List.map (fun x -> snd (snd x)) db.hintdb_nopat);
+    Constr_map.iter (fun k (l,l',_) -> f (Some k) (List.map snd (l@l'))) db.hintdb_map
 
   let transparent_state db = db.hintdb_state
 
@@ -288,6 +412,11 @@ module Hint_db = struct
     if db.use_dn then rebuild_db st db
     else { db with hintdb_state = st }
 
+  let add_cut path db =
+    { db with hintdb_cut = normalize_path (PathOr (db.hintdb_cut, path)) }
+
+  let cut db = db.hintdb_cut
+
   let unfolds db = db.hintdb_unfolds
 
   let use_dn db = db.use_dn
@@ -348,7 +477,7 @@ let try_head_pattern c =
 
 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 make_exact_entry sigma pri ?(name=PathAny) (c,cty) =
   let cty = strip_outer_cast cty in
     match kind_of_term cty with
     | Prod _ -> failwith "make_exact_entry"
@@ -364,7 +493,7 @@ let make_exact_entry sigma pri ?name (c,cty) =
 	    name = name;
 	    code = Give_exact c })
 
-let make_apply_entry env sigma (eapply,hnf,verbose) pri ?name (c,cty) =
+let make_apply_entry env sigma (eapply,hnf,verbose) pri ?(name=PathAny) (c,cty) =
   let cty = if hnf then hnf_constr env sigma cty else cty in
     match kind_of_term cty with
     | Prod _ ->
@@ -415,7 +544,8 @@ let make_resolves env sigma flags pri ?name 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 ~name:(VarRef hname)
+    [make_apply_entry env sigma (true, true, false) None 
+       ~name:(PathHints [VarRef hname])
        (mkVar hname, htyp)]
   with
     | Failure _ -> []
@@ -427,7 +557,7 @@ let make_unfold eref =
   (Some g,
    { pri = 4;
      pat = None;
-     name = Some g;
+     name = PathHints [g];
      code = Unfold_nth eref })
 
 let make_extern pri pat tacast =
@@ -435,10 +565,10 @@ let make_extern pri pat tacast =
   (hdconstr,
    { pri = pri;
      pat = pat;
-     name = None;
+     name = PathAny;
      code = Extern tacast })
 
-let make_trivial env sigma ?name c =
+let make_trivial env sigma ?(name=PathAny) 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
@@ -476,7 +606,7 @@ 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 remove_hint dbname grs =
   let db = get_db dbname in
   let db' = Hint_db.remove_list grs db in
     searchtable_add (dbname, db')
@@ -486,6 +616,12 @@ type hint_action =
   | AddTransparency of evaluable_global_reference list * bool
   | AddHints of hint_entry list
   | RemoveHints of global_reference list
+  | AddCut of hints_path
+
+let add_cut dbname path =
+  let db = get_db dbname in
+  let db' = Hint_db.add_cut path db in
+    searchtable_add (dbname, db')
 
 type hint_obj = bool * string * hint_action  (* locality, name, action *)
 
@@ -494,7 +630,8 @@ let cache_autohint (_,(local,name,hints)) =
   | CreateDB (b, st) -> searchtable_add (name, Hint_db.empty st b)
   | AddTransparency (grs, b) -> add_transparency name grs b
   | AddHints hints -> add_hint name hints
-  | RemoveHints grs -> remove_hints name hints grs
+  | RemoveHints grs -> remove_hint name grs
+  | AddCut path -> add_cut name path
 
 let forward_subst_tactic =
   ref (fun _ -> failwith "subst_tactic is not installed for auto")
@@ -553,7 +690,9 @@ let subst_autohint (subst,(local,name,hintlist as obj)) =
     | 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')
-
+    | AddCut path ->
+      let path' = subst_hints_path subst path in
+	if path' == path then obj else (local, name, AddCut path')
 
 let classify_autohint ((local,name,hintlist) as obj) =
   if local or hintlist = (AddHints []) then Dispose else Substitute obj
@@ -563,8 +702,7 @@ let inAutoHint : hint_obj -> obj =
                     cache_function = cache_autohint;
 		    load_function = (fun _ -> cache_autohint);
 		    subst_function = subst_autohint;
-		    classify_function = classify_autohint }
-
+		    classify_function = classify_autohint; }
 
 let create_hint_db l n st b =
   Lib.add_anonymous_leaf (inAutoHint (l,n,CreateDB (b, st)))
@@ -585,17 +723,22 @@ let add_resolves env sigma clist local dbnames =
        Lib.add_anonymous_leaf
 	 (inAutoHint
 	    (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)))))
+     	      (List.flatten (List.map (fun (x, hnf, path, y) ->
+		make_resolves env sigma (true,hnf,Flags.is_verbose()) x ~name:path y) clist)))))
     dbnames
 
-
 let add_unfolds l local dbnames =
   List.iter
     (fun dbname -> Lib.add_anonymous_leaf
        (inAutoHint (local,dbname, AddHints (List.map make_unfold l))))
     dbnames
 
+let add_cuts l local dbnames =
+  List.iter
+    (fun dbname -> Lib.add_anonymous_leaf
+       (inAutoHint (local,dbname, AddCut l)))
+    dbnames
+
 let add_transparency l b local dbnames =
   List.iter
     (fun dbname -> Lib.add_anonymous_leaf
@@ -626,7 +769,8 @@ let add_trivials env sigma l local dbnames =
   List.iter
     (fun dbname ->
        Lib.add_anonymous_leaf (
-	 inAutoHint(local,dbname, AddHints (List.map (fun (name, c) -> make_trivial env sigma ?name c) l))))
+	 inAutoHint(local,dbname, 
+		    AddHints (List.map (fun (name, c) -> make_trivial env sigma ~name c) l))))
     dbnames
 
 let forward_intern_tac =
@@ -635,8 +779,9 @@ let forward_intern_tac =
 let set_extern_intern_tac f = forward_intern_tac := f
 
 type hints_entry =
-  | HintsResolveEntry of (int option * bool * global_reference option * constr) list
-  | HintsImmediateEntry of (global_reference option * constr) list
+  | HintsResolveEntry of (int option * bool * hints_path_atom * constr) list
+  | HintsImmediateEntry of (hints_path_atom * constr) list
+  | HintsCutEntry of hints_path
   | HintsUnfoldEntry of evaluable_global_reference list
   | HintsTransparencyEntry of evaluable_global_reference list * bool
   | HintsExternEntry of
@@ -677,10 +822,10 @@ 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 =
+let path_of_constr_expr c =
   match c with
-  | Topconstr.CRef r -> (try Some (global r) with _ -> None)
-  | _ -> None 
+  | Topconstr.CRef r -> (try PathHints [global r] with _ -> PathAny)
+  | _ -> PathAny
       
 let interp_hints h =
   let f c =
@@ -693,8 +838,8 @@ 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 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 fp = Constrintern.intern_constr_pattern Evd.empty (Global.env()) in
   match h with
   | HintsResolve lhints -> HintsResolveEntry (List.map fres lhints)
@@ -706,7 +851,7 @@ let interp_hints h =
       let constr_hints_of_ind qid =
         let ind = global_inductive_with_alias qid in
         list_tabulate (fun i -> let c = (ind,i+1) in
-			 None, true, Some (ConstructRef c), mkConstruct c)
+			 None, true, PathHints [ConstructRef c], mkConstruct c)
 	  (nconstructors ind) in
 	HintsResolveEntry (List.flatten (List.map constr_hints_of_ind lqid))
   | HintsExtern (pri, patcom, tacexp) ->
@@ -725,6 +870,7 @@ let add_hints local dbnames0 h =
   match h with
   | HintsResolveEntry lhints -> add_resolves env sigma lhints local dbnames
   | HintsImmediateEntry lhints -> add_trivials env sigma lhints local dbnames
+  | HintsCutEntry lhints -> add_cuts lhints local dbnames
   | HintsUnfoldEntry lhints -> add_unfolds lhints local dbnames
   | HintsTransparencyEntry (lhints, b) ->
       add_transparency lhints b local dbnames
@@ -827,17 +973,18 @@ let print_hint_db db =
 	    else str"Non-discriminated database")));
   msgnl (hov 2 (str"Unfoldable variable definitions: " ++ pr_idpred ids));
   msgnl (hov 2 (str"Unfoldable constant definitions: " ++ pr_cpred csts));
+  msgnl (hov 2 (str"Cut: " ++ pp_hints_path (Hint_db.cut db)));
   Hint_db.iter
     (fun head hintlist ->
       match head with
       | Some head ->
 	  msg (hov 0
 		  (str "For " ++ pr_global head ++ str " -> " ++
-		      pr_hint_list hintlist))
+		      pr_hint_list (List.map (fun x -> (0,x)) hintlist)))
       | None ->
 	  msg (hov 0
 		  (str "For any goal -> " ++
-		      pr_hint_list hintlist)))
+		      pr_hint_list (List.map (fun x -> (0, x)) hintlist))))
     db
 
 let print_hint_db_by_name dbname =
@@ -934,16 +1081,16 @@ let make_local_hint_db ?ts eapply lems gl =
     (Hint_db.add_list hintlist (Hint_db.empty ts false)) gl
 
 (* Serait-ce possible de compiler d'abord la tactique puis de faire la
-   substitution sans passer par bdize dont l'objectif est de préparer un
+   substitution sans passer par bdize dont l'objectif est de préparer un
    terme pour l'affichage ? (HH) *)
 
-(* Si on enlève le dernier argument (gl) conclPattern est calculé une
+(* Si on enlève le dernier argument (gl) conclPattern est calculé une
 fois pour toutes : en particulier si Pattern.somatch produit une UserError
-Ce qui fait que si la conclusion ne matche pas le pattern, Auto échoue, même
-si après Intros la conclusion matche le pattern.
+Ce qui fait que si la conclusion ne matche pas le pattern, Auto échoue, même
+si après Intros la conclusion matche le pattern.
 *)
 
-(* conclPattern doit échouer avec error car il est rattraper par tclFIRST *)
+(* conclPattern doit échouer avec error car il est rattraper par tclFIRST *)
 
 let forward_interp_tactic =
   ref (fun _ -> failwith "interp_tactic is not installed for auto")
@@ -964,8 +1111,8 @@ let conclPattern concl pat tac gl =
 (**************************************************************************)
 
 (* local_db is a Hint database containing the hypotheses of current goal *)
-(* Papageno : cette fonction a été pas mal simplifiée depuis que la base
-  de Hint impérative a été remplacée par plusieurs bases fonctionnelles *)
+(* Papageno : cette fonction a été pas mal simplifiée depuis que la base
+  de Hint impérative a été remplacée par plusieurs bases fonctionnelles *)
 
 let flags_of_state st =
   {auto_unif_flags with
diff --git a/tactics/auto.mli b/tactics/auto.mli
index ce2b33013..521c5ed24 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.mli
@@ -32,16 +32,20 @@ type 'a auto_tactic =
 
 open Glob_term
 
+type hints_path_atom = 
+  | PathHints of global_reference list
+  | PathAny
+
 type 'a gen_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 *)
+  name  : hints_path_atom; (** A potential name to refer to the hint *) 
   code  : 'a auto_tactic; (** the tactic to apply when the concl matches pat *)
 }
 
 type pri_auto_tactic = clausenv gen_auto_tactic
 
-type stored_data = int * pri_auto_tactic
+type stored_data = int * clausenv gen_auto_tactic
 
 type search_entry
 
@@ -49,24 +53,40 @@ type search_entry
 
 type hint_entry = global_reference option * types gen_auto_tactic
 
+type hints_path =
+  | PathAtom of hints_path_atom
+  | PathStar of hints_path
+  | PathSeq of hints_path * hints_path
+  | PathOr of hints_path * hints_path
+  | PathEmpty
+  | PathEpsilon
+
+val normalize_path : hints_path -> hints_path
+val path_matches : hints_path -> hints_path_atom list -> bool
+val path_derivate : hints_path -> hints_path_atom -> hints_path
+val pp_hints_path : hints_path -> Pp.std_ppcmds
+
 module Hint_db :
   sig
     type t
     val empty : transparent_state -> bool -> t
     val find : global_reference -> t -> search_entry
-    val map_none : t ->pri_auto_tactic list
+    val map_none : t -> pri_auto_tactic list
     val map_all : global_reference -> t -> pri_auto_tactic list
     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 iter : (global_reference option -> pri_auto_tactic list -> unit) -> t -> unit
 
     val use_dn : t -> bool
     val transparent_state : t -> transparent_state
     val set_transparent_state : t -> transparent_state -> t
 
+    val add_cut : hints_path -> t -> t
+    val cut : t -> hints_path
+
     val unfolds : t -> Idset.t * Cset.t
   end
 
@@ -75,8 +95,9 @@ type hint_db_name = string
 type hint_db = Hint_db.t
 
 type hints_entry =
-  | HintsResolveEntry of (int option * bool * global_reference option * constr) list
-  | HintsImmediateEntry of (global_reference option * constr) list
+  | HintsResolveEntry of (int option * bool * hints_path_atom * constr) list
+  | HintsImmediateEntry of (hints_path_atom * constr) list
+  | HintsCutEntry of hints_path
   | HintsUnfoldEntry of evaluable_global_reference list
   | HintsTransparencyEntry of evaluable_global_reference list * bool
   | HintsExternEntry of
@@ -119,7 +140,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 -> ?name:global_reference -> constr * constr -> hint_entry
+val make_exact_entry : evar_map -> int option -> ?name:hints_path_atom -> 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;
@@ -129,7 +150,7 @@ val make_exact_entry : evar_map -> int option -> ?name:global_reference -> const
    [cty] is the type of [c]. *)
 
 val make_apply_entry :
-  env -> evar_map -> bool * bool * bool -> int option -> ?name:global_reference -> 
+  env -> evar_map -> bool * bool * bool -> int option -> ?name:hints_path_atom -> 
   constr * constr -> hint_entry
 
 (** A constr which is Hint'ed will be:
@@ -140,7 +161,7 @@ val make_apply_entry :
          has missing arguments. *)
 
 val make_resolves :
-  env -> evar_map -> bool * bool * bool -> int option -> ?name:global_reference -> 
+  env -> evar_map -> bool * bool * bool -> int option -> ?name:hints_path_atom -> 
   constr -> hint_entry list
 
 (** [make_resolve_hyp hname htyp].
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index c9951bea2..a974c76a0 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -34,7 +34,7 @@ let subst_hint subst hint =
   let typ' = subst_mps subst hint.rew_type in
   let pat' = subst_mps subst hint.rew_pat in
   let t' = Tacinterp.subst_tactic subst hint.rew_tac in
-    if hint.rew_lemma == cst' && hint.rew_tac == t' then hint else
+    if hint.rew_lemma == cst' && hint.rew_type == typ' && hint.rew_tac == t' then hint else
       { hint with
 	rew_lemma = cst'; rew_type = typ';
 	rew_pat = pat';	rew_tac = t' }
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index 184f521e1..1f8ee3af6 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -146,7 +146,7 @@ let rec e_trivial_fail_db db_list local_db goal =
 	  let hintl = make_resolve_hyp (pf_env g') (project g') d in
           (e_trivial_fail_db db_list
 	      (Hint_db.add_list hintl local_db) g'))) ::
-    (List.map (fun (x,_,_,_) -> x) (e_trivial_resolve db_list local_db (pf_concl goal)))
+    (List.map (fun (x,_,_,_,_) -> x) (e_trivial_resolve db_list local_db (pf_concl goal)))
   in 
   tclFIRST (List.map tclCOMPLETE tacl) goal 
 
@@ -166,7 +166,7 @@ and e_my_find_search db_list local_db hdc complete concl =
       (local_db::db_list)
   in
   let tac_of_hint =
-    fun (flags, {pri=b; pat = p; code=t}) ->
+    fun (flags, {pri = b; pat = p; code = t; name = name}) ->
       let tac =
 	match t with
 	  | Res_pf (term,cl) -> with_prods nprods (term,cl) (unify_resolve flags)
@@ -177,14 +177,16 @@ and e_my_find_search db_list local_db hdc complete concl =
 	        (if complete then tclIDTAC else e_trivial_fail_db db_list local_db)
 	  | Unfold_nth c -> tclWEAK_PROGRESS (unfold_in_concl [all_occurrences,c])
 	  | Extern tacast -> 
-	    tclTHEN
-	      (fun gl -> Refiner.tclEVARS (mark_unresolvables (project gl)) gl)
+(* 	    tclTHEN *)
+(* 	      (fun gl -> Refiner.tclEVARS (mark_unresolvables (project gl)) gl) *)
 	      (conclPattern concl p tacast)
       in
       let tac = if complete then tclCOMPLETE tac else tac in
 	match t with
-	| Extern _ -> (tac,b,true,lazy (pr_autotactic t))
-	| _ -> (tac,b,false,lazy (pr_autotactic t))
+	| Extern _ -> (tac,b,true, name, lazy (pr_autotactic t))
+	| _ -> 
+(* 	  let tac gl = with_pattern (pf_env gl) (project gl) flags p concl tac gl in *)
+	    (tac,b,false, name, lazy (pr_autotactic t))
   in List.map tac_of_hint hintl
 
 and e_trivial_resolve db_list local_db gl =
@@ -212,7 +214,9 @@ let pr_ev evs ev = Printer.pr_constr_env (Goal.V82.env evs ev) (Evarutil.nf_evar
 let pr_depth l = prlist_with_sep (fun () -> str ".") pr_int (List.rev l)
 
 type autoinfo = { hints : Auto.hint_db; is_evar: existential_key option;
-		  only_classes: bool; auto_depth: int list; auto_last_tac: std_ppcmds Lazy.t}
+		  only_classes: bool; auto_depth: int list; auto_last_tac: std_ppcmds Lazy.t;
+		  auto_path : global_reference option list;
+		  auto_cut : hints_path }
 type autogoal = goal * autoinfo
 type 'ans fk = unit -> 'ans
 type ('a,'ans) sk = 'a -> 'ans fk -> 'ans
@@ -239,24 +243,35 @@ let make_resolve_hyp env sigma st flags only_classes pri (id, _, cty) =
   let keep = not only_classes || is_class in
     if keep then 
       let c = mkVar id in
+      let name = PathHints [VarRef id] in
       let hints =
 	if is_class then
-	  let hints = build_subclasses env sigma (mkVar id) in
-	    list_map_append
-	      (make_resolves env sigma (true,false,Flags.is_verbose()) None) hints
+	  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) 
+	       hints)
 	else []
       in
-	hints @ map_succeed 
-	  (fun f -> try f (c,cty) with UserError _ -> failwith "") 
-	[make_exact_entry sigma pri; make_apply_entry env sigma flags pri]
+        (hints @ map_succeed 
+	 (fun f -> try f (c,cty) with UserError _ -> failwith "") 
+	 [make_exact_entry ~name sigma pri; make_apply_entry ~name env sigma flags pri])
     else []
 
 let pf_filtered_hyps gls = 
   Goal.V82.hyps gls.Evd.sigma (sig_it gls)
 
 let make_hints g st only_classes sign =
-  let hintlist = list_map_append 
-    (pf_apply make_resolve_hyp g st (true,false,false) only_classes None) sign
+  let paths, hintlist = 
+    List.fold_left 
+    (fun (paths, hints) hyp ->
+     if is_section_variable (pi1 hyp) then (paths, hints)
+     else
+       let path, hint = 		    
+	 PathEmpty, pf_apply make_resolve_hyp g st (true,false,false) only_classes None hyp
+       in
+	 (PathOr (paths, path), hint @ hints))
+    (PathEmpty, []) sign
   in Hint_db.add_list hintlist (Hint_db.empty st true)
     
 let make_autogoal_hints = 
@@ -289,17 +304,10 @@ let intro_tac : atac =
       in {it = gls'; sigma = s})
 
 let normevars_tac : atac = 
-  { skft = fun sk fk {it = gl; sigma = s} ->
-    let gl', sigma' = Goal.V82.nf_evar s (fst gl) in
-      sk {it = [gl', snd gl]; sigma = sigma'} fk }
-
-  (* lift_tactic tclNORMEVAR *)
-  (*   (fun {it = gls; sigma = s} info -> *)
-  (*     let gls' = *)
-  (* 	List.map (fun g' -> *)
-  (* 	  (g', { info with auto_last_tac = str"NORMEVAR" })) gls *)
-  (*     in {it = gls'; sigma = s}) *)
-
+  { skft = fun sk fk {it = (gl, info); sigma = s} ->
+    let gl', sigma' = Goal.V82.nf_evar s gl in
+    let info' = { info with auto_last_tac = lazy (str"normevars") } in
+      sk {it = [gl', info']; sigma = sigma'} fk }
 
 (* Ordering of states is lexicographic on the number of remaining goals. *)
 let compare (pri, _, _, res) (pri', _, _, res') =
@@ -319,20 +327,21 @@ let hints_tac hints =
       let tacgl = {it = gl; sigma = s} in
       let poss = e_possible_resolve hints info.hints concl in
       let rec aux i foundone = function
-	| (tac, _, b, pp) :: tl ->
+	| (tac, _, b, name, pp) :: tl ->
+	  let derivs = path_derivate info.auto_cut name in
 	  let res = 
-	    try Some (tac tacgl) 
+            try
+		if path_matches derivs [] then None else Some (tac tacgl)
 	    with e when catchable e -> None 
 	  in
 	    (match res with
-	       | None -> 
-		 aux i foundone tl
+	       | None -> aux i foundone tl
 	       | Some {it = gls; sigma = s'} ->
 	    	   if !typeclasses_debug then
 		     msgnl (pr_depth (i :: info.auto_depth) ++ str": " ++ Lazy.force pp
 			    ++ str" on" ++ spc () ++ pr_ev s gl);
 		   let fk =
-		     (fun () -> (* if !typeclasses_debug then msgnl (str"backtracked after " ++ pp); *)
+		     (fun () -> if !typeclasses_debug then msgnl (str"backtracked after " ++ Lazy.force pp);
 			aux (succ i) true tl)
 		   in
 		   let sgls =
@@ -349,7 +358,7 @@ let hints_tac hints =
 		       | None -> gls', s'
 		       | Some (evgls, s') ->
 			 (* Reorder with dependent subgoals. *)
-			 (List.map (fun (ev, x) -> Some ev, x) evgls @ gls', s')
+			 (gls' @ List.map (fun (ev, x) -> Some ev, x) evgls, s')
 		   in
 		   let gls' = list_map_i
 		     (fun j (evar, g) ->
@@ -360,7 +369,8 @@ let hints_tac hints =
 			      if b && not (Environ.eq_named_context_val (Goal.V82.hyps s' g) (Goal.V82.hyps s' gl))
 			      then make_autogoal_hints info.only_classes
 				~st:(Hint_db.transparent_state info.hints) {it = g; sigma = s'}
-			      else info.hints }
+			      else info.hints;
+			      auto_cut = derivs }
 			in g, info) 1 newgls in
 		   let glsv = {it = gls'; sigma = s'} in
 		     sk glsv fk)
@@ -372,9 +382,14 @@ let hints_tac hints =
 	  fk ()
     in aux 1 false poss }
 
-let dependent only_classes evd oev concl =
-  if oev <> None then true
-  else not (Intset.is_empty (Evarutil.evars_of_term concl))
+let isProp env sigma concl = 
+  let ty = Retyping.get_type_of env sigma concl in
+    kind_of_term ty = Sort (Prop Null)
+
+let needs_backtrack only_classes env evd oev concl =
+  if oev = None || isProp env evd concl then
+    not (Intset.is_empty (Evarutil.evars_of_term concl))
+  else true
 
 let then_list (second : atac) (sk : (auto_result, 'a) sk) : (auto_result, 'a) sk =
   let rec aux s (acc : autogoal list list) fk = function
@@ -386,11 +401,15 @@ let then_list (second : atac) (sk : (auto_result, 'a) sk) : (auto_result, 'a) sk
 	       (fun {it=gls';sigma=s'} fk' ->
 		  let needs_backtrack = 
 		    if gls' = [] then
- 		      dependent info.only_classes s' info.is_evar (Goal.V82.concl s gl)
+ 		      needs_backtrack info.only_classes
+		        (Goal.V82.env s gl) s' info.is_evar (Goal.V82.concl s gl)
 		    else true
 		  in
-		  let fk'' = if not needs_backtrack then
-		    (if !typeclasses_debug then msgnl (str"no backtrack on " ++ pr_ev s gl); fk) else fk' 
+		  let fk'' = 
+		    if not needs_backtrack then
+		      (if !typeclasses_debug then msgnl (str"no backtrack on " ++ pr_ev s gl ++ 
+							 str " after " ++ Lazy.force info.auto_last_tac); fk) 
+		    else fk' 
 		  in aux s' (gls'::acc) fk'' gls)
 	       fk {it = (gl,info); sigma = s})
     | [] -> Some (List.rev acc, s, fk)
@@ -425,14 +444,20 @@ let rec fix_limit limit (t : 'a tac) : 'a tac =
   if limit = 0 then fail_tac 
   else then_tac t { skft = fun sk fk -> (fix_limit (pred limit) t).skft sk fk }
     
-let make_autogoal ?(only_classes=true) ?(st=full_transparent_state) ev g =
+let make_autogoal ?(only_classes=true) ?(st=full_transparent_state) cut ev g =
   let hints = make_autogoal_hints only_classes ~st g in
     (g.it, { hints = hints ; is_evar = ev; 
-	     only_classes = only_classes; auto_depth = []; auto_last_tac = lazy (mt()) })
+	     only_classes = only_classes; auto_depth = []; auto_last_tac = lazy (str"none");
+	     auto_path = []; auto_cut = cut })
       
-let make_autogoals ?(only_classes=true) ?(st=full_transparent_state) gs evm' =
+
+let cut_of_hints h =
+  List.fold_left (fun cut db -> PathOr (Hint_db.cut db, cut)) PathEmpty h
+
+let make_autogoals ?(only_classes=true) ?(st=full_transparent_state) hints gs evm' =
+  let cut = cut_of_hints hints in
   { it = list_map_i (fun i g -> 
-    let (gl, auto) = make_autogoal ~only_classes ~st (Some (fst g)) {it = snd g; sigma = evm'} in
+    let (gl, auto) = make_autogoal ~only_classes ~st cut (Some (fst g)) {it = snd g; sigma = evm'} in
       (gl, { auto with auto_depth = [i]})) 1 gs; sigma = evm' }
 
 let get_result r = 
@@ -440,11 +465,11 @@ let get_result r =
   | None -> None
   | Some (gls, fk) -> Some (gls.sigma,fk)
 	
-let run_on_evars ?(only_classes=true) ?(st=full_transparent_state) p evm tac =
+let run_on_evars ?(only_classes=true) ?(st=full_transparent_state) p evm hints tac =
   match evars_to_goals p evm with
   | None -> None (* This happens only because there's no evar having p *)
   | Some (goals, evm') ->
-      let res = run_list_tac tac p goals (make_autogoals ~only_classes ~st goals evm') in
+      let res = run_list_tac tac p goals (make_autogoals ~only_classes ~st hints goals evm') in
 	match get_result res with
 	| None -> raise Not_found
 	| Some (evm', fk) -> Some (evars_reset_evd ~with_conv_pbs:true evm' evm, fk)
@@ -458,7 +483,7 @@ let eauto_tac ?limit hints =
   | Some limit -> fix_limit limit (eauto_tac hints)
       
 let eauto ?(only_classes=true) ?st ?limit hints g =
-  let gl = { it = make_autogoal ~only_classes ?st None g; sigma = project g } in
+  let gl = { it = make_autogoal ~only_classes ?st (cut_of_hints hints) None g; sigma = project g } in
     match run_tac (eauto_tac ?limit hints) gl with
     | None -> raise Not_found
     | Some {it = goals; sigma = s} ->
@@ -467,7 +492,7 @@ let eauto ?(only_classes=true) ?st ?limit hints g =
 let real_eauto st ?limit hints p evd =
   let rec aux evd fails =
     let res, fails =
-      try run_on_evars ~st p evd (eauto_tac ?limit hints), fails
+      try run_on_evars ~st p evd hints (eauto_tac ?limit hints), fails
       with Not_found ->
 	List.fold_right (fun fk (res, fails) ->
 	  match res with
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index a264de318..9966fb772 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -499,3 +499,55 @@ END
 TACTIC EXTEND convert_concl_no_check
 | ["convert_concl_no_check" constr(x) ] -> [ convert_concl_no_check x DEFAULTcast ]
 END
+
+
+let pr_hints_path_atom prc _ _ a =
+  match a with
+  | PathAny -> str"."
+  | PathHints grs ->
+    prlist_with_sep pr_spc Printer.pr_global grs
+
+ARGUMENT EXTEND hints_path_atom
+  TYPED AS hints_path_atom
+  PRINTED BY pr_hints_path_atom
+| [ global_list(g) ] -> [ PathHints (List.map Nametab.global g) ]
+| [ "*" ] -> [ PathAny ]
+END
+
+let pr_hints_path prc prx pry c =
+  let rec aux = function
+  | PathAtom a -> pr_hints_path_atom prc prx pry a
+  | PathStar p -> str"(" ++ aux p ++ str")*"
+  | PathSeq (p, p') -> aux p ++ spc () ++ aux p'
+  | PathOr (p, p') -> str "(" ++ aux p ++ str"|" ++ aux p' ++ str")"
+  | PathEmpty -> str"ø"
+  | PathEpsilon -> str"ε"
+  in aux c
+
+ARGUMENT EXTEND hints_path
+  TYPED AS hints_path
+  PRINTED BY pr_hints_path
+| [ "(" hints_path(p) ")"  ] -> [ p ]
+| [ "!" hints_path(p)  ] -> [ PathStar p ]
+| [ "emp" ] -> [ PathEmpty ]
+| [ "eps" ] -> [ PathEpsilon ]
+| [ hints_path_atom(a) ] -> [ PathAtom a ]
+| [ hints_path(p) "|" hints_path(q) ] -> [ PathOr (p, q) ]
+| [ hints_path(p) ";" hints_path(q) ] -> [ PathSeq (p, q) ]
+END
+
+let pr_hintbases _prc _prlc _prt = Pptactic.pr_hintbases
+
+ARGUMENT EXTEND opthints
+  TYPED AS preident_list_opt
+  PRINTED BY pr_hintbases
+| [ ":" ne_preident_list(l) ] -> [ Some l ]
+| [ ] -> [ None ]
+END
+
+VERNAC COMMAND EXTEND HintCut
+| [ "Hint" "Cut" "[" hints_path(p) "]" opthints(dbnames) ] -> [
+  let entry = HintsCutEntry p in
+    Auto.add_hints (Vernacexpr.use_section_locality ()) 
+      (match dbnames with None -> ["core"] | Some l -> l) entry ]
+END
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index bae28c7ce..da35edbed 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -286,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,None,c)
+  (pri,true,Auto.PathAny,c)
 
 let add_hints_iff l2r lc n bl =
   Auto.add_hints true bl