gistfile1.txt

diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index d26853b..7a60587 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -211,10 +211,11 @@ let nb_empty_evars s =
 
 let pr_ev evs ev = Printer.pr_constr_env (Goal.V82.env evs ev) (Evarutil.nf_evar evs (Goal.V82.concl evs ev))
 
-let pr_depth l = prlist_with_sep (fun () -> str ".") pr_int (List.rev l)
+let pr_depth l = prlist_with_sep (fun () -> str ".") (fun (i,j) -> if j==0 then
+  pr_int i else pr_int i ++ str"/" ++ pr_int j )  (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 * int) list; auto_last_tac: std_ppcmds Lazy.t;
 		  auto_path : global_reference option list;
 		  auto_cut : hints_path }
 type autogoal = goal * autoinfo
@@ -338,16 +339,29 @@ let hints_tac hints =
       let rec aux i foundone = function
 	| (tac, _, b, name, pp) :: tl ->
 	  let derivs = path_derivate info.auto_cut name in
+	    	   if !typeclasses_debug then (
+          msgnl (str"deriv: " ++ Pp.hov 0 (Eauto.pr_hints_path () () () derivs));
+          msgnl (str"info.auto_cut: " ++ Pp.h 0 (Eauto.pr_hints_path () () () info.auto_cut));
+          msgnl (str"name: " ++ Eauto.pr_hints_path_atom () () () name));
 	  let res = 
             try
-		if path_matches derivs [] then None else Some (tac tacgl)
+		if path_matches derivs [] then Some None else Some (Some (tac tacgl))
 	    with e when catchable e -> None 
 	  in
 	    (match res with
-	       | None -> aux i foundone tl
-	       | Some {it = gls; sigma = s'} ->
+	       | Some None ->
 	    	   if !typeclasses_debug then
-		     msgnl (pr_depth (i :: info.auto_depth) ++ str": " ++ Lazy.force pp
+		     msgnl (pr_depth ((i, 0) :: info.auto_depth) ++ str": cutting at " ++ Eauto.pr_hints_path_atom ()()() name);
+                   aux (succ i) foundone tl
+	       | None ->
+	    	   if !typeclasses_debug then
+		     msgnl (pr_depth ((i, 0) :: info.auto_depth)
+                     ++ str": tactic application failed with: " ++
+                     Lazy.force pp);
+                   aux (succ i) foundone tl
+	       | Some (Some {it = gls; sigma = s'}) ->
+	    	   if !typeclasses_debug then
+		     msgnl (pr_depth ((i, 0) :: 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 " ++ Lazy.force pp);
@@ -372,7 +386,7 @@ let hints_tac hints =
 		   let gls' = list_map_i
 		     (fun j (evar, g) ->
 			let info =
-			  { info with auto_depth = j :: i :: info.auto_depth; auto_last_tac = pp;
+			  { info with auto_depth = (i,j) :: info.auto_depth; auto_last_tac = pp;
 			      is_evar = evar;
 			      hints =
 			      if b && not (Environ.eq_named_context_val (Goal.V82.hyps s' g) (Goal.V82.hyps s' gl))
@@ -467,7 +481,7 @@ let make_autogoals ?(only_classes=true) ?(st=full_transparent_state) hints gs ev
   let cut = cut_of_hints hints in
   { it = list_map_i (fun i g -> 
     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' }
+      (gl, { auto with auto_depth = [(i,0)]})) 1 gs; sigma = evm' }
 
 let get_result r = 
   match r with
diff --git a/tactics/eauto.mli b/tactics/eauto.mli
index 68ec42f..4bea749 100644
--- a/tactics/eauto.mli
+++ b/tactics/eauto.mli
@@ -36,3 +36,6 @@ val eauto_with_bases :
   open_constr list -> Auto.hint_db list -> Proof_type.tactic
 
 val autounfold : hint_db_name list -> Tacticals.clause -> tactic
+
+val pr_hints_path : 'a -> 'a -> 'a -> Auto.hints_path -> Pp.std_ppcmds
+val pr_hints_path_atom : 'a -> 'a -> 'a -> Auto.hints_path_atom -> Pp.std_ppcmds