info_trivial, info_auto, info_eauto, and debug (trivial|auto)

 To mitigate the lack of a general "info" tactical, let's
 introduce some specialized tactics info_trivial, info_auto
 and info_eauto that display the basic tactics used when
 solving a goal.

 We also add tactics "debug trivial" and "debug auto" which
 display every basic tactics attempted by trivial or auto.

 Triggering the "info" or "debug" mode for auto, eauto, trivial
 can also be done now via global options, such as Set Debug Auto
 or Set Info Eauto. In case both debug and info modes are
 activated, the debug mode takes precedence.

 NB: it would be nice to name these tactics "info xxx" instead
 of "info_xxx", but I don't see how to implement a "info eauto"
 in eauto.ml4 (hence by TACTIC EXTEND) while keeping
 a generic "info foo" tactic in g_ltac.ml4 (useful to display
 a nice message about the unavailability of the general info).

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

7 files changed, 376 insertions, 155 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index cfef521c8..cedec80a1 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -879,14 +879,14 @@ let add_hints local dbnames0 h =
 
 let pr_autotactic =
   function
-  | Res_pf (c,clenv) -> (str"apply " ++ pr_lconstr c)
-  | ERes_pf (c,clenv) -> (str"eapply " ++ pr_lconstr c)
-  | Give_exact c -> (str"exact " ++ pr_lconstr c)
+  | Res_pf (c,clenv) -> (str"apply " ++ pr_constr c)
+  | ERes_pf (c,clenv) -> (str"eapply " ++ pr_constr c)
+  | Give_exact c -> (str"exact " ++ pr_constr c)
   | Res_pf_THEN_trivial_fail (c,clenv) ->
-      (str"apply " ++ pr_lconstr c ++ str" ; trivial")
+      (str"apply " ++ pr_constr c ++ str" ; trivial")
   | Unfold_nth c -> (str"unfold " ++  pr_evaluable_reference c)
   | Extern tac ->
-      (str "(external) " ++ Pptactic.pr_glob_tactic (Global.env()) tac)
+      (str "(*external*) " ++ Pptactic.pr_glob_tactic (Global.env()) tac)
 
 let pr_hint (id, v) =
   (pr_autotactic v.code ++ str"(level " ++ int v.pri ++ str", id " ++ int id ++ str ")" ++ spc ())
@@ -1099,6 +1099,131 @@ let conclPattern concl pat tac gl =
 	with PatternMatchingFailure -> error "conclPattern" in
     !forward_interp_tactic constr_bindings tac gl
 
+(***********************************************************)
+(** A debugging / verbosity framework for trivial and auto *)
+(***********************************************************)
+
+(** The following options allow to trigger debugging/verbosity
+    without having to adapt the scripts.
+    Note: if Debug and Info are both activated, Debug take precedence. *)
+
+let global_debug_trivial = ref false
+let global_debug_auto = ref false
+let global_info_trivial = ref false
+let global_info_auto = ref false
+
+let add_option ls refe =
+  let _ = Goptions.declare_bool_option
+    { Goptions.optsync  = true;
+      Goptions.optdepr  = false;
+      Goptions.optname  = String.concat " " ls;
+      Goptions.optkey   = ls;
+      Goptions.optread  = (fun () -> !refe);
+      Goptions.optwrite = (:=) refe }
+  in ()
+
+let _ =
+  add_option ["Debug";"Trivial"] global_debug_trivial;
+  add_option ["Debug";"Auto"] global_debug_auto;
+  add_option ["Info";"Trivial"] global_info_trivial;
+  add_option ["Info";"Auto"] global_info_auto
+
+let no_dbg () = (Off,0,ref [])
+
+let mk_trivial_dbg debug =
+  let d =
+    if debug = Debug || !global_debug_trivial then Debug
+    else if debug = Info || !global_info_trivial then Info
+    else Off
+  in (d,0,ref [])
+
+(** Note : we start the debug depth of auto at 1 to distinguish it
+   for trivial (whose depth is 0). *)
+
+let mk_auto_dbg debug =
+  let d =
+    if debug = Debug || !global_debug_auto then Debug
+    else if debug = Info || !global_info_auto then Info
+    else Off
+  in (d,1,ref [])
+
+let incr_dbg = function (dbg,depth,trace) -> (dbg,depth+1,trace)
+
+(** A tracing tactic for debug/info trivial/auto *)
+
+let tclLOG (dbg,depth,trace) pp tac =
+  match dbg with
+    | Off -> tac
+    | Debug ->
+       (* For "debug (trivial/auto)", we directly output messages *)
+      let s = String.make depth '*' in
+      begin fun gl ->
+	try
+	  let out = tac gl in
+	  msg_debug (str s ++ spc () ++ pp () ++ str ". (*success*)");
+	  out
+	with e ->
+	  msg_debug (str s ++ spc () ++ pp () ++ str ". (*fail*)");
+	  raise e
+      end
+    | Info ->
+      (* For "info (trivial/auto)", we store a log trace *)
+      begin fun gl ->
+	try
+	  let out = tac gl in
+	  trace := (depth, Some pp) :: !trace;
+	  out
+	with e ->
+	  trace := (depth, None) :: !trace;
+	  raise e
+      end
+
+(** For info, from the linear trace information, we reconstitute the part
+    of the proof tree we're interested in. The last executed tactic
+    comes first in the trace (and it should be a successful one).
+    [depth] is the root depth of the tree fragment we're visiting.
+    [keep] means we're in a successful tree fragment (the very last
+    tactic has been successful). *)
+
+let rec cleanup_info_trace depth acc = function
+  | [] -> acc
+  | (d,Some pp) :: l -> cleanup_info_trace d ((d,pp)::acc) l
+  | l -> cleanup_info_trace depth acc (erase_subtree depth l)
+
+and erase_subtree depth = function
+  | [] -> []
+  | (d,_) :: l -> if d = depth then l else erase_subtree depth l
+
+let pr_info_atom (d,pp) =
+  msg_debug (str (String.make d ' ') ++ pp () ++ str ".")
+
+let pr_info_trace = function
+  | (Info,_,{contents=(d,Some pp)::l}) ->
+      List.iter pr_info_atom (cleanup_info_trace d [(d,pp)] l)
+  | _ -> ()
+
+let pr_info_nop = function
+  | (Info,_,_) -> msg_debug (str "idtac.")
+  | _ -> ()
+
+let pr_dbg_header = function
+  | (Off,_,_) -> ()
+  | (Debug,0,_) -> msg_debug (str "(* debug trivial : *)")
+  | (Debug,_,_) -> msg_debug (str "(* debug auto : *)")
+  | (Info,0,_) -> msg_debug (str "(* info trivial : *)")
+  | (Info,_,_) -> msg_debug (str "(* info auto : *)")
+
+let tclTRY_dbg d tac =
+  tclORELSE0
+    (fun gl ->
+      pr_dbg_header d;
+      let out = tac gl in
+      pr_info_trace d;
+      out)
+    (fun gl ->
+      pr_info_nop d;
+      tclIDTAC gl)
+
 (**************************************************************************)
 (*                           The Trivial tactic                           *)
 (**************************************************************************)
@@ -1122,17 +1247,20 @@ let exists_evaluable_reference env = function
   | EvalConstRef _ -> true
   | EvalVarRef v -> try ignore(lookup_named v env); true with Not_found -> false
 
-let rec trivial_fail_db mod_delta db_list local_db gl =
+let dbg_intro dbg = tclLOG dbg (fun () -> str "intro") intro
+let dbg_assumption dbg = tclLOG dbg (fun () -> str "assumption") assumption
+
+let rec trivial_fail_db dbg mod_delta db_list local_db gl =
   let intro_tac =
-    tclTHEN intro
+    tclTHEN (dbg_intro dbg)
       (fun g'->
 	 let hintl = make_resolve_hyp (pf_env g') (project g') (pf_last_hyp g')
-	 in trivial_fail_db mod_delta db_list (Hint_db.add_list hintl local_db) g')
+	 in trivial_fail_db dbg mod_delta db_list (Hint_db.add_list hintl local_db) g')
   in
   tclFIRST
-    (assumption::intro_tac::
-     (List.map (fun tac -> tclCOMPLETE tac)
-       (trivial_resolve mod_delta db_list local_db (pf_concl gl)))) gl
+    ((dbg_assumption dbg)::intro_tac::
+     (List.map tclCOMPLETE
+       (trivial_resolve dbg mod_delta db_list local_db (pf_concl gl)))) gl
 
 and my_find_search_nodelta db_list local_db hdc concl =
   List.map (fun hint -> (None,hint))
@@ -1173,7 +1301,7 @@ and my_find_search_delta db_list local_db hdc concl =
 	  in List.map (fun x -> (Some flags,x)) l)
       	(local_db::db_list)
 
-and tac_of_hint db_list local_db concl (flags, ({pat=p; code=t})) =
+and tac_of_hint dbg db_list local_db concl (flags, ({pat=p; code=t})) =
   let tactic = 
     match t with
     | Res_pf (c,cl) -> unify_resolve_gen flags (c,cl)
@@ -1182,23 +1310,26 @@ and tac_of_hint db_list local_db concl (flags, ({pat=p; code=t})) =
     | Res_pf_THEN_trivial_fail (c,cl) ->
       tclTHEN
         (unify_resolve_gen flags (c,cl))
-        (trivial_fail_db (flags <> None) db_list local_db)
-    | Unfold_nth c -> 
+	(* With "(debug) trivial", we shouldn't end here, and
+	   with "debug auto" we don't display the details of inner trivial *)
+        (trivial_fail_db (no_dbg ()) (flags <> None) db_list local_db)
+    | Unfold_nth c ->
       (fun gl ->
        if exists_evaluable_reference (pf_env gl) c then
 	 tclPROGRESS (h_reduce (Unfold [all_occurrences_expr,c]) onConcl) gl
        else tclFAIL 0 (str"Unbound reference") gl)
     | Extern tacast -> conclPattern concl p tacast
-  in tactic
+  in
+  tclLOG dbg (fun () -> pr_autotactic t) tactic
 
-and trivial_resolve mod_delta db_list local_db cl =
+and trivial_resolve dbg mod_delta db_list local_db cl =
   try
     let head =
       try let hdconstr,_ = head_constr_bound cl in
 	    Some (head_of_constr_reference hdconstr)
       with Bound -> None
     in
-      List.map (tac_of_hint db_list local_db cl)
+      List.map (tac_of_hint dbg db_list local_db cl)
 	(priority
 	    (my_find_search mod_delta db_list local_db head cl))
   with Not_found -> []
@@ -1215,52 +1346,59 @@ let make_db_list dbnames =
   in
   List.map lookup dbnames
 
-let trivial lems dbnames gl =
+let trivial ?(debug=Off) lems dbnames gl =
   let db_list = make_db_list dbnames in
-  tclTRY (trivial_fail_db false db_list (make_local_hint_db false lems gl)) gl
+  let d = mk_trivial_dbg debug in
+  tclTRY_dbg d
+    (trivial_fail_db d false db_list (make_local_hint_db false lems gl)) gl
 
-let full_trivial lems gl =
+let full_trivial ?(debug=Off) lems gl =
   let dbnames = Hintdbmap.dom !searchtable in
   let dbnames = list_remove "v62" dbnames in
   let db_list = List.map (fun x -> searchtable_map x) dbnames in
-  tclTRY (trivial_fail_db false db_list (make_local_hint_db false lems gl)) gl
+  let d = mk_trivial_dbg debug in
+  tclTRY_dbg d
+    (trivial_fail_db d false db_list (make_local_hint_db false lems gl)) gl
 
-let gen_trivial lems = function
-  | None -> full_trivial lems
-  | Some l -> trivial lems l
+let gen_trivial ?(debug=Off) lems = function
+  | None -> full_trivial ~debug lems
+  | Some l -> trivial ~debug lems l
 
-let h_trivial lems l =
-  Refiner.abstract_tactic (TacTrivial (List.map snd lems,l))
-    (gen_trivial lems l)
+let h_trivial ?(debug=Off) lems l =
+  Refiner.abstract_tactic (TacTrivial (debug,List.map snd lems,l))
+    (gen_trivial ~debug lems l)
 
 (**************************************************************************)
 (*                       The classical Auto tactic                        *)
 (**************************************************************************)
 
-let possible_resolve mod_delta db_list local_db cl =
+let possible_resolve dbg mod_delta db_list local_db cl =
   try
     let head =
       try let hdconstr,_ = head_constr_bound cl in
 	    Some (head_of_constr_reference hdconstr)
       with Bound -> None
     in
-      List.map (tac_of_hint db_list local_db cl)
+      List.map (tac_of_hint dbg db_list local_db cl)
 	(my_find_search mod_delta db_list local_db head cl)
   with Not_found -> []
 
-let decomp_unary_term_then (id,_,typc) kont1 kont2 gl =
+let dbg_case dbg id =
+  tclLOG dbg (fun () -> str "case " ++ pr_id id) (simplest_case (mkVar id))
+
+let decomp_unary_term_then dbg (id,_,typc) kont1 kont2 gl =
   try
     let ccl = applist (head_constr typc) in
     match Hipattern.match_with_conjunction ccl with
     | Some (_,args) ->
-	tclTHEN (simplest_case (mkVar id)) (kont1 (List.length args)) gl
+	tclTHEN (dbg_case dbg id) (kont1 (List.length args)) gl
     | None ->
 	kont2 gl
   with UserError _ -> kont2 gl
 
-let decomp_empty_term (id,_,typc) gl =
+let decomp_empty_term dbg (id,_,typc) gl =
   if Hipattern.is_empty_type typc then
-    simplest_case (mkVar id) gl
+    dbg_case dbg id gl
   else
     errorlabstrm "Auto.decomp_empty_term" (str "Not an empty type.")
 
@@ -1272,32 +1410,32 @@ let extend_local_db gl decl db =
    empty type) then call the continuation tactic with hint db extended
    with the obtained not-further-decomposable hypotheses *)
 
-let rec decomp_and_register_decl p kont (id,_,_ as decl) db gl =
+let rec decomp_and_register_decl dbg p kont (id,_,_ as decl) db gl =
   if p = 0 then
     kont (extend_local_db gl decl db) gl
   else
     tclORELSE0
-      (decomp_empty_term decl)
-      (decomp_unary_term_then decl (intros_decomp (p-1) kont [] db)
+      (decomp_empty_term dbg decl)
+      (decomp_unary_term_then dbg decl (intros_decomp dbg (p-1) kont [] db)
 	(kont (extend_local_db gl decl db))) gl
 
 (* Introduce [n] hypotheses, then decompose then with maximum depth [p] and
    call the continuation tactic [kont] with the hint db extended
    with the so-obtained not-further-decomposable hypotheses *)
 
-and intros_decomp p kont decls db n =
+and intros_decomp dbg p kont decls db n =
   if n = 0 then
-    decomp_and_register_decls p kont decls db
+    decomp_and_register_decls dbg p kont decls db
   else
-    tclTHEN intro (onLastDecl (fun d ->
-      (intros_decomp p kont (d::decls) db (n-1))))
+    tclTHEN (dbg_intro dbg) (onLastDecl (fun d ->
+      (intros_decomp dbg p kont (d::decls) db (n-1))))
 
 (* Decompose hypotheses [hyps] with maximum depth [p] and
    call the continuation tactic [kont] with the hint db extended
    with the so-obtained not-further-decomposable hypotheses *)
 
-and decomp_and_register_decls p kont decls =
-  List.fold_left (decomp_and_register_decl p) kont decls
+and decomp_and_register_decls dbg p kont decls =
+  List.fold_left (decomp_and_register_decl dbg p) kont decls
 
 
 (* decomp is an natural number giving an indication on decomposition
@@ -1307,53 +1445,60 @@ and decomp_and_register_decls p kont decls =
 
 exception Uplift of tactic list
 
-let search_gen p n mod_delta db_list local_db =
-  let rec search n local_db =
+let search_gen d p n mod_delta db_list local_db =
+  let rec search d n local_db =
     if n=0 then (fun gl -> error "BOUND 2") else
-      tclORELSE0 assumption
-	(tclORELSE0 (intros_decomp p (search n) [] local_db 1)
-	   (fun gl -> tclFIRST
-	      (List.map (fun ntac -> tclTHEN ntac (search (n-1) local_db))
-		 (possible_resolve mod_delta db_list local_db (pf_concl gl))) gl))
+      tclORELSE0 (dbg_assumption d)
+	(tclORELSE0 (intros_decomp d p (search d n) [] local_db 1)
+	   (fun gl ->
+	     let d' = incr_dbg d in
+	     tclFIRST
+	       (List.map
+		  (fun ntac -> tclTHEN ntac (search d' (n-1) local_db))
+		  (possible_resolve d mod_delta db_list local_db (pf_concl gl))) gl))
   in
-  search n local_db
+  search d n local_db
 
-let search = search_gen 0
+let search dbg = search_gen dbg 0
 
 let default_search_depth = ref 5
 
-let delta_auto mod_delta n lems dbnames gl =
+let delta_auto ?(debug=Off) mod_delta n lems dbnames gl =
   let db_list = make_db_list dbnames in
-  tclTRY (search n mod_delta db_list (make_local_hint_db false lems gl)) gl
+  let d = mk_auto_dbg debug in
+  tclTRY_dbg d
+    (search d n mod_delta db_list (make_local_hint_db false lems gl)) gl
 
-let auto = delta_auto false
+let auto ?(debug=Off) n = delta_auto ~debug false n
 
-let new_auto = delta_auto true
+let new_auto ?(debug=Off) n = delta_auto ~debug true n
 
 let default_auto = auto !default_search_depth [] []
 
-let delta_full_auto mod_delta n lems gl =
+let delta_full_auto ?(debug=Off) mod_delta n lems gl =
   let dbnames = Hintdbmap.dom !searchtable in
   let dbnames = list_remove "v62" dbnames in
   let db_list = List.map (fun x -> searchtable_map x) dbnames in
-  tclTRY (search n mod_delta db_list (make_local_hint_db false lems gl)) gl
+  let d = mk_auto_dbg debug in
+  tclTRY_dbg d
+    (search d n mod_delta db_list (make_local_hint_db false lems gl)) gl
 
-let full_auto = delta_full_auto false
-let new_full_auto = delta_full_auto true
+let full_auto ?(debug=Off) n = delta_full_auto ~debug false n
+let new_full_auto ?(debug=Off) n = delta_full_auto ~debug true n
 
 let default_full_auto gl = full_auto !default_search_depth [] gl
 
-let gen_auto n lems dbnames =
+let gen_auto ?(debug=Off) n lems dbnames =
   let n = match n with None -> !default_search_depth | Some n -> n in
   match dbnames with
-  | None -> full_auto n lems
-  | Some l -> auto n lems l
+  | None -> full_auto ~debug n lems
+  | Some l -> auto ~debug n lems l
 
 let inj_or_var = Option.map (fun n -> ArgArg n)
 
-let h_auto n lems l =
-  Refiner.abstract_tactic (TacAuto (inj_or_var n,List.map snd lems,l))
-    (gen_auto n lems l)
+let h_auto ?(debug=Off) n lems l =
+  Refiner.abstract_tactic (TacAuto (debug,inj_or_var n,List.map snd lems,l))
+    (gen_auto ~debug n lems l)
 
 (**************************************************************************)
 (*                  The "destructing Auto" from Eduardo                   *)
@@ -1363,23 +1508,26 @@ let h_auto n lems l =
    one look for an immediate solution *)
 let default_search_decomp = ref 20
 
-let destruct_auto p lems n gl =
-  decomp_and_register_decls p (fun local_db gl ->
-    search_gen p n false (List.map searchtable_map ["core";"extcore"])
+let destruct_auto d p lems n gl =
+  decomp_and_register_decls d p (fun local_db gl ->
+    search_gen d p n false (List.map searchtable_map ["core";"extcore"])
       (add_hint_lemmas false lems local_db gl) gl)
     (pf_hyps gl)
     (Hint_db.empty empty_transparent_state false)
     gl
 
-let dautomatic des_opt lems n = tclTRY (destruct_auto des_opt lems n)
+let dautomatic ?(debug=Off) des_opt lems n =
+  let d = mk_auto_dbg debug in
+  tclTRY_dbg d (destruct_auto d des_opt lems n)
 
-let dauto (n,p) lems =
+let dauto ?(debug=Off) (n,p) lems =
   let p = match p with Some p -> p | None -> !default_search_decomp in
   let n = match n with Some n -> n | None -> !default_search_depth in
-  dautomatic p lems n
+  dautomatic ~debug p lems n
 
 let default_dauto = dauto (None,None) []
 
-let h_dauto (n,p) lems =
-  Refiner.abstract_tactic (TacDAuto (inj_or_var n,p,List.map snd lems))
-    (dauto (n,p) lems)
+let h_dauto ?(debug=Off) (n,p) lems =
+  Refiner.abstract_tactic
+    (TacDAuto (debug,inj_or_var n,p,List.map snd lems))
+    (dauto ~debug (n,p) lems)
diff --git a/tactics/auto.mli b/tactics/auto.mli
index 95de089e0..69a526e5a 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.mli
@@ -219,48 +219,61 @@ val conclPattern : constr -> constr_pattern option -> Tacexpr.glob_tactic_expr -
 
 val make_db_list : hint_db_name list -> hint_db list
 
-val auto : int -> open_constr list -> hint_db_name list -> tactic
+val auto : ?debug:Tacexpr.debug ->
+  int -> open_constr list -> hint_db_name list -> tactic
 
 (** Auto with more delta. *)
 
-val new_auto : int -> open_constr list -> hint_db_name list -> tactic
+val new_auto : ?debug:Tacexpr.debug ->
+  int -> open_constr list -> hint_db_name list -> tactic
 
 (** auto with default search depth and with the hint database "core" *)
 val default_auto : tactic
 
 (** auto with all hint databases except the "v62" compatibility database *)
-val full_auto : int -> open_constr list -> tactic
+val full_auto : ?debug:Tacexpr.debug ->
+  int -> open_constr list -> tactic
 
 (** auto with all hint databases except the "v62" compatibility database
    and doing delta *)
-val new_full_auto : int -> open_constr list -> tactic
+val new_full_auto : ?debug:Tacexpr.debug ->
+  int -> open_constr list -> tactic
 
 (** auto with default search depth and with all hint databases
    except the "v62" compatibility database *)
 val default_full_auto : tactic
 
 (** The generic form of auto (second arg [None] means all bases) *)
-val gen_auto : int option -> open_constr list -> hint_db_name list option -> tactic
+val gen_auto : ?debug:Tacexpr.debug ->
+  int option -> open_constr list -> hint_db_name list option -> tactic
 
 (** The hidden version of auto *)
-val h_auto   : int option -> open_constr list -> hint_db_name list option -> tactic
+val h_auto   : ?debug:Tacexpr.debug ->
+  int option -> open_constr list -> hint_db_name list option -> tactic
 
 (** Trivial *)
-val trivial : open_constr list -> hint_db_name list -> tactic
-val gen_trivial : open_constr list -> hint_db_name list option -> tactic
-val full_trivial : open_constr list -> tactic
-val h_trivial : open_constr list -> hint_db_name list option -> tactic
+
+val trivial : ?debug:Tacexpr.debug ->
+  open_constr list -> hint_db_name list -> tactic
+val gen_trivial : ?debug:Tacexpr.debug ->
+  open_constr list -> hint_db_name list option -> tactic
+val full_trivial : ?debug:Tacexpr.debug ->
+  open_constr list -> tactic
+val h_trivial : ?debug:Tacexpr.debug ->
+  open_constr list -> hint_db_name list option -> tactic
 
 val pr_autotactic : 'a auto_tactic -> Pp.std_ppcmds
 
 (** Destructing Auto *)
 
 (** DAuto *)
-val dauto : int option * int option -> open_constr list -> tactic
+val dauto :  ?debug:Tacexpr.debug ->
+  int option * int option -> open_constr list -> tactic
 val default_search_decomp : int ref
 val default_dauto : tactic
 
-val h_dauto : int option * int option -> open_constr list -> tactic
+val h_dauto : ?debug:Tacexpr.debug ->
+  int option * int option -> open_constr list -> tactic
 
 (** Hook for changing the initialization of auto *)
 
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index 4923aa720..a0187434a 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -28,6 +28,7 @@ open Clenv
 open Auto
 open Glob_term
 open Hiddentac
+open Tacexpr
 
 let eauto_unif_flags = { auto_unif_flags with Unification.modulo_delta = full_transparent_state }
 
@@ -172,7 +173,14 @@ type search_state = {
   tacres : goal list sigma;
   last_tactic : std_ppcmds Lazy.t;
   dblist : Auto.hint_db list;
-  localdb :  Auto.hint_db list }
+  localdb :  Auto.hint_db list;
+  prev : prev_search_state
+}
+
+and prev_search_state = (* for info eauto *)
+  | Unknown
+  | Init
+  | State of search_state
 
 module SearchProblem = struct
 
@@ -212,6 +220,7 @@ module SearchProblem = struct
     if s.depth = 0 then
       []
     else
+      let ps = if s.prev = Unknown then Unknown else State s in
       let lg = s.tacres in
       let nbgl = List.length (sig_it lg) in
       assert (nbgl > 0);
@@ -226,7 +235,8 @@ module SearchProblem = struct
 	in
 	List.map (fun (res,pp) -> { depth = s.depth; tacres = res;
 				    last_tactic = pp; dblist = s.dblist;
-				    localdb = List.tl s.localdb }) l
+				    localdb = List.tl s.localdb;
+				    prev = ps}) l
       in
       let intro_tac =
 	List.map
@@ -238,7 +248,7 @@ module SearchProblem = struct
              let ldb = Hint_db.add_list hintl (List.hd s.localdb) in
 	     { depth = s.depth; tacres = res;
 	       last_tactic = pp; dblist = s.dblist;
-	       localdb = ldb :: List.tl s.localdb })
+	       localdb = ldb :: List.tl s.localdb; prev = ps })
 	  (filter_tactics s.tacres [Tactics.intro,lazy (str "intro")])
       in
       let rec_tacs =
@@ -249,73 +259,122 @@ module SearchProblem = struct
 	  (fun (lgls as res, pp) ->
 	     let nbgl' = List.length (sig_it lgls) in
 	     if nbgl' < nbgl then
-	       { depth = s.depth; tacres = res; last_tactic = pp;
+	       { depth = s.depth; tacres = res; last_tactic = pp; prev = ps;
 		 dblist = s.dblist; localdb = List.tl s.localdb }
 	     else
 	       { depth = pred s.depth; tacres = res;
-		 dblist = s.dblist; last_tactic = pp;
+		 dblist = s.dblist; last_tactic = pp; prev = ps;
 		 localdb =
 		   list_addn (nbgl'-nbgl) (List.hd s.localdb) s.localdb })
 	  l
       in
       List.sort compare (assumption_tacs @ intro_tac @ rec_tacs)
 
-  let pp s =
-    msg (hov 0 (str " depth=" ++ int s.depth ++ spc () ++
-		  (Lazy.force s.last_tactic) ++ str "\n"))
+  let pp s = hov 0 (str " depth=" ++ int s.depth ++ spc () ++
+		      (Lazy.force s.last_tactic))
 
 end
 
 module Search = Explore.Make(SearchProblem)
 
-let make_initial_state n gl dblist localdb =
+(** Utilities for debug eauto / info eauto *)
+
+let global_debug_eauto = ref false
+let global_info_eauto = ref false
+
+let _ =
+  Goptions.declare_bool_option
+    { Goptions.optsync  = true;
+      Goptions.optdepr  = false;
+      Goptions.optname  = "Debug Eauto";
+      Goptions.optkey   = ["Debug";"Eauto"];
+      Goptions.optread  = (fun () -> !global_debug_eauto);
+      Goptions.optwrite = (:=) global_debug_eauto }
+
+let _ =
+  Goptions.declare_bool_option
+    { Goptions.optsync  = true;
+      Goptions.optdepr  = false;
+      Goptions.optname  = "Info Eauto";
+      Goptions.optkey   = ["Info";"Eauto"];
+      Goptions.optread  = (fun () -> !global_info_eauto);
+      Goptions.optwrite = (:=) global_info_eauto }
+
+let mk_eauto_dbg d =
+  if d = Debug || !global_debug_eauto then Debug
+  else if d = Info || !global_info_eauto then Info
+  else Off
+
+let pr_info_nop = function
+  | Info -> msg_debug (str "idtac.")
+  | _ -> ()
+
+let pr_dbg_header = function
+  | Off -> ()
+  | Debug -> msg_debug (str "(* debug eauto : *)")
+  | Info -> msg_debug (str "(* info eauto : *)")
+
+let pr_info dbg s =
+  if dbg <> Info then ()
+  else
+    let rec loop s =
+      match s.prev with
+	| Unknown | Init -> s.depth
+	| State sp ->
+	  let mindepth = loop sp in
+	  let indent = String.make (mindepth - sp.depth) ' ' in
+	  msg_debug (str indent ++ Lazy.force s.last_tactic ++ str ".");
+	  mindepth
+    in
+    ignore (loop s)
+
+(** Eauto main code *)
+
+let make_initial_state dbg n gl dblist localdb =
   { depth = n;
     tacres = tclIDTAC gl;
     last_tactic = lazy (mt());
     dblist = dblist;
-    localdb = [localdb] }
-
-let e_depth_search debug p db_list local_db gl =
-  try
-    let tac = if debug then Search.debug_depth_first else Search.depth_first in
-    let s = tac (make_initial_state p gl db_list local_db) in
-    s.tacres
-  with Not_found -> error "eauto: depth first search failed."
-
-let e_breadth_search debug n db_list local_db gl =
-  try
-    let tac =
-      if debug then Search.debug_breadth_first else Search.breadth_first
-    in
-    let s = tac (make_initial_state n gl db_list local_db) in
-    s.tacres
-  with Not_found -> error "eauto: breadth first search failed."
+    localdb = [localdb];
+    prev = if dbg=Info then Init else Unknown;
+  }
 
 let e_search_auto debug (in_depth,p) lems db_list gl =
   let local_db = make_local_hint_db ~ts:full_transparent_state true lems gl in
-  if in_depth then
-    e_depth_search debug p db_list local_db gl
-  else
-    e_breadth_search debug p db_list local_db gl
+  let d = mk_eauto_dbg debug in
+  let tac = match in_depth,d with
+    | (true,Debug) -> Search.debug_depth_first
+    | (true,_) -> Search.depth_first
+    | (false,Debug) -> Search.debug_breadth_first
+    | (false,_) -> Search.breadth_first
+  in
+  try
+    pr_dbg_header d;
+    let s = tac (make_initial_state d p gl db_list local_db) in
+    pr_info d s;
+    s.tacres
+  with Not_found ->
+    pr_info_nop d;
+    error "eauto: search failed"
 
 open Evd
 
-let eauto_with_bases debug np lems db_list =
+let eauto_with_bases ?(debug=Off) np lems db_list =
   tclTRY (e_search_auto debug np lems db_list)
 
-let eauto debug np lems dbnames =
+let eauto ?(debug=Off) np lems dbnames =
   let db_list = make_db_list dbnames in
   tclTRY (e_search_auto debug np lems db_list)
 
-let full_eauto debug n lems gl =
+let full_eauto ?(debug=Off) n lems gl =
   let dbnames = current_db_names () in
   let dbnames =  list_remove "v62" dbnames in
   let db_list = List.map searchtable_map dbnames in
   tclTRY (e_search_auto debug n lems db_list) gl
 
-let gen_eauto d np lems = function
-  | None -> full_eauto d np lems
-  | Some l -> eauto d np lems l
+let gen_eauto ?(debug=Off) np lems = function
+  | None -> full_eauto ~debug np lems
+  | Some l -> eauto ~debug np lems l
 
 let make_depth = function
   | None -> !default_search_depth
@@ -363,7 +422,7 @@ END
 TACTIC EXTEND eauto
 | [ "eauto" int_or_var_opt(n) int_or_var_opt(p) auto_using(lems)
     hintbases(db) ] ->
-    [ gen_eauto false (make_dimension n p) lems db ]
+    [ gen_eauto (make_dimension n p) lems db ]
 END
 
 TACTIC EXTEND new_eauto
@@ -371,20 +430,25 @@ TACTIC EXTEND new_eauto
     hintbases(db) ] ->
     [ match db with
       | None -> new_full_auto (make_depth n) lems
-      | Some l ->
-	  new_auto (make_depth n) lems l ]
+      | Some l -> new_auto (make_depth n) lems l ]
 END
 
 TACTIC EXTEND debug_eauto
 | [ "debug" "eauto" int_or_var_opt(n) int_or_var_opt(p) auto_using(lems)
     hintbases(db) ] ->
-    [ gen_eauto true (make_dimension n p) lems db ]
+    [ gen_eauto ~debug:Debug (make_dimension n p) lems db ]
+END
+
+TACTIC EXTEND info_eauto
+| [ "info_eauto" int_or_var_opt(n) int_or_var_opt(p) auto_using(lems)
+    hintbases(db) ] ->
+    [ gen_eauto ~debug:Info (make_dimension n p) lems db ]
 END
 
 TACTIC EXTEND dfs_eauto
 | [ "dfs" "eauto" int_or_var_opt(p) auto_using(lems)
       hintbases(db) ] ->
-    [ gen_eauto false (true, make_depth p) lems db ]
+    [ gen_eauto (true, make_depth p) lems db ]
 END
 
 let cons a l = a :: l
diff --git a/tactics/eauto.mli b/tactics/eauto.mli
index 68ec42f4e..5e656139b 100644
--- a/tactics/eauto.mli
+++ b/tactics/eauto.mli
@@ -27,11 +27,11 @@ val registered_e_assumption : tactic
 
 val e_give_exact : ?flags:Unification.unify_flags -> constr -> tactic
 
-val gen_eauto : bool -> bool * int -> open_constr list ->
+val gen_eauto : ?debug:Tacexpr.debug -> bool * int -> open_constr list ->
   hint_db_name list option -> tactic
 
 val eauto_with_bases :
-  bool ->
+  ?debug:Tacexpr.debug ->
   bool * int ->
   open_constr list -> Auto.hint_db list -> Proof_type.tactic
 
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 81c79f931..b55a9f01f 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -175,8 +175,8 @@ let _ =
         "intros", TacIntroPattern [];
         "assumption", TacAssumption;
         "cofix", TacCofix None;
-        "trivial", TacTrivial ([],None);
-        "auto", TacAuto(None,[],None);
+        "trivial", TacTrivial (Off,[],None);
+        "auto", TacAuto(Off,None,[],None);
         "left", TacLeft(false,NoBindings);
         "eleft", TacLeft(true,NoBindings);
         "right", TacRight(false,NoBindings);
@@ -714,12 +714,12 @@ let rec intern_atomic lf ist x =
                  (clause_app (intern_hyp_location ist) cls),b)
 
   (* Automation tactics *)
-  | TacTrivial (lems,l) -> TacTrivial (List.map (intern_constr ist) lems,l)
-  | TacAuto (n,lems,l) ->
-      TacAuto (Option.map (intern_or_var ist) n,
+  | TacTrivial (d,lems,l) -> TacTrivial (d,List.map (intern_constr ist) lems,l)
+  | TacAuto (d,n,lems,l) ->
+      TacAuto (d,Option.map (intern_or_var ist) n,
         List.map (intern_constr ist) lems,l)
-  | TacDAuto (n,p,lems) ->
-      TacDAuto (Option.map (intern_or_var ist) n,p,
+  | TacDAuto (d,n,p,lems) ->
+      TacDAuto (d,Option.map (intern_or_var ist) n,p,
         List.map (intern_constr ist) lems)
 
   (* Derived basic tactics *)
@@ -1785,14 +1785,6 @@ and eval_tactic ist = function
   | TacDo (n,tac) -> tclDO (interp_int_or_var ist n) (interp_tactic ist tac)
   | TacTimeout (n,tac) -> tclTIMEOUT (interp_int_or_var ist n) (interp_tactic ist tac)
   | TacTry tac -> tclTRY (interp_tactic ist tac)
-  | TacInfo tac ->
-      let t = (interp_tactic ist tac) in
-	tclINFO
-	  begin
-	    match tac with
-		TacAtom (_,_) -> t
-	      | _ -> abstract_tactic_expr (TacArg (dloc,Tacexp tac)) t
-	  end
   | TacRepeat tac -> tclREPEAT (interp_tactic ist tac)
   | TacOrelse (tac1,tac2) ->
         tclORELSE (interp_tactic ist tac1) (interp_tactic ist tac2)
@@ -1800,6 +1792,12 @@ and eval_tactic ist = function
   | TacSolve l -> tclSOLVE (List.map (interp_tactic ist) l)
   | TacComplete tac -> tclCOMPLETE (interp_tactic ist tac)
   | TacArg a -> interp_tactic ist (TacArg a)
+  | TacInfo tac ->
+      msg_warning
+	(str "The general \"info\" tactic is currently not working.\n" ++
+	 str "Some specific verbose tactics may exist instead, such as\n" ++
+	 str "info_trivial, info_auto, info_eauto.");
+      eval_tactic ist tac
 
 and force_vrec ist gl = function
   | VRec (lfun,body) -> val_interp {ist with lfun = !lfun} gl body
@@ -2273,16 +2271,16 @@ and interp_atomic ist gl tac =
           (interp_pure_open_constr ist env sigma c) clp
 
   (* Automation tactics *)
-  | TacTrivial (lems,l) ->
-      Auto.h_trivial
+  | TacTrivial (debug,lems,l) ->
+      Auto.h_trivial ~debug
 	(interp_auto_lemmas ist env sigma lems)
 	(Option.map (List.map (interp_hint_base ist)) l)
-  | TacAuto (n,lems,l) ->
-      Auto.h_auto (Option.map (interp_int_or_var ist) n)
+  | TacAuto (debug,n,lems,l) ->
+      Auto.h_auto ~debug (Option.map (interp_int_or_var ist) n)
 	(interp_auto_lemmas ist env sigma lems)
 	(Option.map (List.map (interp_hint_base ist)) l)
-  | TacDAuto (n,p,lems) ->
-      Auto.h_dauto (Option.map (interp_int_or_var ist) n,p)
+  | TacDAuto (debug,n,p,lems) ->
+      Auto.h_dauto ~debug (Option.map (interp_int_or_var ist) n,p)
       (interp_auto_lemmas ist env sigma lems)
 
   (* Derived basic tactics *)
@@ -2646,9 +2644,9 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with
   | TacLetTac (id,c,clp,b) -> TacLetTac (id,subst_glob_constr subst c,clp,b)
 
   (* Automation tactics *)
-  | TacTrivial (lems,l) -> TacTrivial (List.map (subst_glob_constr subst) lems,l)
-  | TacAuto (n,lems,l) -> TacAuto (n,List.map (subst_glob_constr subst) lems,l)
-  | TacDAuto (n,p,lems) -> TacDAuto (n,p,List.map (subst_glob_constr subst) lems)
+  | TacTrivial (d,lems,l) -> TacTrivial (d,List.map (subst_glob_constr subst) lems,l)
+  | TacAuto (d,n,lems,l) -> TacAuto (d,n,List.map (subst_glob_constr subst) lems,l)
+  | TacDAuto (d,n,p,lems) -> TacDAuto (d,n,p,List.map (subst_glob_constr subst) lems)
 
   (* Derived basic tactics *)
   | TacSimpleInductionDestruct (isrec,h) as x -> x
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 2bb9c1cbe..f7b8419c9 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -54,7 +54,6 @@ let tclREPEAT_MAIN   = Refiner.tclREPEAT_MAIN
 let tclFIRST         = Refiner.tclFIRST
 let tclSOLVE         = Refiner.tclSOLVE
 let tclTRY           = Refiner.tclTRY
-let tclINFO          = Refiner.tclINFO
 let tclCOMPLETE      = Refiner.tclCOMPLETE
 let tclAT_LEAST_ONCE = Refiner.tclAT_LEAST_ONCE
 let tclFAIL          = Refiner.tclFAIL
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index 42c70eef4..7c13894ec 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -46,7 +46,6 @@ val tclREPEAT_MAIN   : tactic -> tactic
 val tclFIRST         : tactic list -> tactic
 val tclSOLVE         : tactic list -> tactic
 val tclTRY           : tactic -> tactic
-val tclINFO          : tactic -> tactic
 val tclCOMPLETE      : tactic -> tactic
 val tclAT_LEAST_ONCE : tactic -> tactic
 val tclFAIL          : int -> std_ppcmds -> tactic