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

22 files changed, 460 insertions, 211 deletions

diff --git a/CHANGES b/CHANGES
index 1fcca5888..e2113ccff 100644
--- a/CHANGES
+++ b/CHANGES
@@ -12,6 +12,13 @@ Vernacular commands
 Tactics
 
 - Tactics btauto, a reflexive boolean tautology solver.
+- Still no general "info" tactical, but new specific tactics
+  info_auto, info_eauto, info_trivial which provides information
+  on the proofs found by auto/eauto/trivial. Display of these
+  details could also be activated by Set Info Auto/Eauto/Trivial.
+- Details on everything tried by auto/eauto/trivial during
+  a proof search could be obtained by "debug auto", "debug eauto",
+  "debug trivial" or by a global "Set Debug Auto/Eauto/Trivial".
 
 Program
 
diff --git a/lib/explore.ml b/lib/explore.ml
index 407bf1e91..e353c9070 100644
--- a/lib/explore.ml
+++ b/lib/explore.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Format
+open Pp
 
 (*s Definition of a search problem. *)
 
@@ -14,20 +14,20 @@ module type SearchProblem = sig
   type state
   val branching : state -> state list
   val success : state -> bool
-  val pp : state -> unit
+  val pp : state -> std_ppcmds
 end
 
 module Make = functor(S : SearchProblem) -> struct
 
   type position = int list
 
-  let pp_position p =
+  let msg_with_position p pp =
     let rec pp_rec = function
-      | [] -> ()
-      | [i] -> printf "%d" i
-      | i :: l -> pp_rec l; printf ".%d" i
+      | [] -> mt ()
+      | [i] -> int i
+      | i :: l -> pp_rec l ++ str "." ++ int i
     in
-    open_hbox (); pp_rec p; close_box ()
+    msg_debug (h 0 (pp_rec p) ++ pp)
 
   (*s Depth first search. *)
 
@@ -40,7 +40,7 @@ module Make = functor(S : SearchProblem) -> struct
 
   let debug_depth_first s =
     let rec explore p s =
-      pp_position p; S.pp s;
+      msg_with_position p (S.pp s);
       if S.success s then s else explore_many 1 p (S.branching s)
     and explore_many i p = function
       | [] -> raise Not_found
@@ -83,7 +83,7 @@ module Make = functor(S : SearchProblem) -> struct
 	  explore q
       | s :: l ->
 	  let ps = i::p in
-	  pp_position ps; S.pp s;
+	  msg_with_position ps (S.pp s);
 	  if S.success s then s else enqueue (succ i) p (push (ps,s) q) l
     in
     enqueue 1 [] empty [s]
diff --git a/lib/explore.mli b/lib/explore.mli
index e64459f10..a292fd83e 100644
--- a/lib/explore.mli
+++ b/lib/explore.mli
@@ -27,7 +27,7 @@ module type SearchProblem = sig
 
   val success : state -> bool
 
-  val pp : state -> unit
+  val pp : state -> Pp.std_ppcmds
 
 end
 
diff --git a/lib/pp.ml4 b/lib/pp.ml4
index 4fc53270c..ff1973846 100644
--- a/lib/pp.ml4
+++ b/lib/pp.ml4
@@ -275,17 +275,15 @@ let pp_dirs ft =
 (* pretty print on stdout and stderr *)
 
 (* Special chars for emacs, to detect warnings inside goal output *)
-let emacs_warning_start_string = String.make 1 (Char.chr 254)
-let emacs_warning_end_string = String.make 1 (Char.chr 255)
+let emacs_quote_start = String.make 1 (Char.chr 254)
+let emacs_quote_end = String.make 1 (Char.chr 255)
 
-let warnstart() =
-  if not !print_emacs then mt() else str emacs_warning_start_string
+let emacs_quote strm =
+  if !print_emacs then
+    [< str emacs_quote_start; hov 0 strm; str emacs_quote_end >]
+  else hov 0 strm
 
-let warnend() =
-  if not !print_emacs then mt() else str emacs_warning_end_string
-
-let warnbody strm =
-  [< warnstart() ; hov 0 (str "Warning: " ++ strm) ; warnend() >]
+let warnbody strm = emacs_quote (str "Warning: " ++ strm)
 
 (* pretty printing functions WITHOUT FLUSH *)
 let pp_with ft strm =
@@ -334,6 +332,9 @@ let msgerr x = msg_with !err_ft x
 let msgerrnl x = msgnl_with !err_ft x
 let msg_warning x = msg_warning_with !err_ft x
 
+(* Same specific display in emacs as warning, but without the "Warning:" *)
+let msg_debug x = msgnl (emacs_quote x)
+
 let string_of_ppcmds c =
   msg_with Format.str_formatter c;
   Format.flush_str_formatter ()
diff --git a/lib/pp.mli b/lib/pp.mli
index 2fd62d55a..112d97655 100644
--- a/lib/pp.mli
+++ b/lib/pp.mli
@@ -114,6 +114,9 @@ val msgerr : std_ppcmds -> unit
 val msgerrnl : std_ppcmds -> unit
 val msg_warning : std_ppcmds -> unit
 
+(** Same specific display in emacs as warning, but without the "Warning:" **)
+val msg_debug : std_ppcmds -> unit
+
 val string_of_ppcmds : std_ppcmds -> string
 
 (** {6 Location management. } *)
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 7dc166750..ddff97128 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -435,6 +435,16 @@ GEXTEND Gram
     [ [ "using"; l = LIST1 constr SEP "," -> l
       | -> [] ] ]
   ;
+  trivial:
+    [ [ IDENT "trivial" -> Off
+      | IDENT "info_trivial" -> Info
+      | IDENT "debug"; IDENT "trivial" -> Debug ] ]
+  ;
+  auto:
+    [ [ IDENT "auto" -> Off
+      | IDENT "info_auto" -> Info
+      | IDENT "debug"; IDENT "auto" -> Debug ] ]
+  ;
   eliminator:
     [ [ "using"; el = constr_with_bindings -> el ] ]
   ;
@@ -597,15 +607,13 @@ GEXTEND Gram
         -> TacDecompose (l,c)
 
       (* Automation tactic *)
-      | IDENT "trivial"; lems = auto_using; db = hintbases ->
-	  TacTrivial (lems,db)
-      | IDENT "auto"; n = OPT int_or_var; lems = auto_using; db = hintbases ->
-	  TacAuto (n,lems,db)
-
-      | IDENT "auto"; IDENT "decomp"; p = OPT natural;
-          lems = auto_using -> TacDAuto (None,p,lems)
-      | IDENT "auto"; n = OPT int_or_var; IDENT "decomp"; p = OPT natural;
-          lems = auto_using -> TacDAuto (n,p,lems)
+      | d = trivial; lems = auto_using; db = hintbases -> TacTrivial (d,lems,db)
+      | d = auto; n = OPT int_or_var; lems = auto_using; db = hintbases ->
+          TacAuto (d,n,lems,db)
+      | d = auto; IDENT "decomp"; p = OPT natural; lems = auto_using ->
+          TacDAuto (d,None,p,lems)
+      | d = auto; n = OPT int_or_var; IDENT "decomp"; p = OPT natural;
+          lems = auto_using -> TacDAuto (d,n,p,lems)
 
       (* Context management *)
       | IDENT "clear"; "-"; l = LIST1 id_or_meta -> TacClear (true, l)
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index 465d0b76a..1e0f2aef2 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -516,6 +516,11 @@ let pr_auto_using prc = function
   | l -> spc () ++
       hov 2 (str "using" ++ spc () ++ prlist_with_sep pr_comma prc l)
 
+let string_of_debug = function
+  | Off -> ""
+  | Debug -> "debug "
+  | Info -> "info_"
+
 let pr_then () = str ";"
 
 let ltop = (5,E)
@@ -624,8 +629,8 @@ let rec pr_atom0 = function
   | TacAssumption -> str "assumption"
   | TacAnyConstructor (false,None) -> str "constructor"
   | TacAnyConstructor (true,None) -> str "econstructor"
-  | TacTrivial ([],Some []) -> str "trivial"
-  | TacAuto (None,[],Some []) -> str "auto"
+  | TacTrivial (d,[],Some []) -> str (string_of_debug d ^ "trivial")
+  | TacAuto (d,None,[],Some []) -> str (string_of_debug d ^ "auto")
   | TacReflexivity -> str "reflexivity"
   | TacClear (true,[]) -> str "clear"
   | t -> str "(" ++ pr_atom1 t ++ str ")"
@@ -738,16 +743,18 @@ and pr_atom1 = function
       hov 1 (str "lapply" ++ pr_constrarg c)
 
   (* Automation tactics *)
-  | TacTrivial ([],Some []) as x -> pr_atom0 x
-  | TacTrivial (lems,db) ->
-      hov 0 (str "trivial" ++
+  | TacTrivial (_,[],Some []) as x -> pr_atom0 x
+  | TacTrivial (d,lems,db) ->
+      hov 0 (str (string_of_debug d ^ "trivial") ++
              pr_auto_using pr_constr lems ++ pr_hintbases db)
-  | TacAuto (None,[],Some []) as x -> pr_atom0 x
-  | TacAuto (n,lems,db) ->
-      hov 0 (str "auto" ++ pr_opt (pr_or_var int) n ++
+  | TacAuto (_,None,[],Some []) as x -> pr_atom0 x
+  | TacAuto (d,n,lems,db) ->
+      hov 0 (str (string_of_debug d ^ "auto") ++
+	     pr_opt (pr_or_var int) n ++
              pr_auto_using pr_constr lems ++ pr_hintbases db)
-  | TacDAuto (n,p,lems) ->
-      hov 1 (str "auto" ++ pr_opt (pr_or_var int) n ++ str "decomp" ++
+  | TacDAuto (d,n,p,lems) ->
+      hov 1 (str (string_of_debug d ^ "auto") ++
+	     pr_opt (pr_or_var int) n ++ str "decomp" ++
              pr_opt int p ++ pr_auto_using pr_constr lems)
 
   (* Context management *)
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
index 389118c34..df2597208 100644
--- a/parsing/q_coqast.ml4
+++ b/parsing/q_coqast.ml4
@@ -273,6 +273,11 @@ let mlexpr_of_message_token = function
   | Tacexpr.MsgInt n -> <:expr< Tacexpr.MsgInt $mlexpr_of_int n$ >>
   | Tacexpr.MsgIdent id -> <:expr< Tacexpr.MsgIdent $mlexpr_of_hyp id$ >>
 
+let mlexpr_of_debug = function
+  | Tacexpr.Off -> <:expr< Tacexpr.Off >>
+  | Tacexpr.Debug -> <:expr< Tacexpr.Debug >>
+  | Tacexpr.Info -> <:expr< Tacexpr.Info >>
+
 let rec mlexpr_of_atomic_tactic = function
   (* Basic tactics *)
   | Tacexpr.TacIntroPattern pl ->
@@ -399,15 +404,17 @@ let rec mlexpr_of_atomic_tactic = function
   | Tacexpr.TacTransitivity c -> <:expr< Tacexpr.TacTransitivity $mlexpr_of_option mlexpr_of_constr c$ >>
 
   (* Automation tactics *)
-  | Tacexpr.TacAuto (n,lems,l) ->
+  | Tacexpr.TacAuto (debug,n,lems,l) ->
+      let d = mlexpr_of_debug debug in
       let n = mlexpr_of_option (mlexpr_of_or_var mlexpr_of_int) n in
       let lems = mlexpr_of_list mlexpr_of_constr lems in
       let l = mlexpr_of_option (mlexpr_of_list mlexpr_of_string) l in
-      <:expr< Tacexpr.TacAuto $n$ $lems$ $l$ >>
-  | Tacexpr.TacTrivial (lems,l) ->
+      <:expr< Tacexpr.TacAuto $d$ $n$ $lems$ $l$ >>
+  | Tacexpr.TacTrivial (debug,lems,l) ->
+      let d = mlexpr_of_debug debug in
       let l = mlexpr_of_option (mlexpr_of_list mlexpr_of_string) l in
       let lems = mlexpr_of_list mlexpr_of_constr lems in
-      <:expr< Tacexpr.TacTrivial $lems$ $l$ >>
+      <:expr< Tacexpr.TacTrivial $d$ $lems$ $l$ >>
 
   | _ -> failwith "Quotation of atomic tactic expressions: TODO"
 
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 13b3dabdf..4d5cbe223 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -1415,7 +1415,7 @@ let prove_with_tcc tcc_lemma_constr eqs : tactic =
 (* 		 let ids = List.filter (fun id -> not (List.mem id ids)) ids' in  *)
 (* 		 rewrite *)
 (* 	      ) *)
-	      Eauto.gen_eauto false (false,5) [] (Some [])
+	      Eauto.gen_eauto (false,5) [] (Some [])
 	    ]
 	    gls
 
@@ -1493,7 +1493,6 @@ let new_prove_with_tcc is_mes acc_inv hrec tcc_hyps eqs : tactic =
 			   (
 			    tclCOMPLETE(
 				    Eauto.eauto_with_bases
-				      false
 				      (true,5)
 				      [Evd.empty,Lazy.force refl_equal]
 				      [Auto.Hint_db.empty empty_transparent_state false]
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 7613c6765..8eb7d0e8f 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -1322,7 +1322,6 @@ let open_new_goal (build_proof:tactic -> tactic -> unit) using_lemmas ref_ goal_
 			  (eapply_with_bindings (mkVar (List.nth !lid !h_num), NoBindings))
 			  e_assumption;
 		      Eauto.eauto_with_bases
-			false
 			(true,5)
 			[Evd.empty,Lazy.force refl_equal]
 			[Auto.Hint_db.empty empty_transparent_state false]
diff --git a/plugins/rtauto/proof_search.ml b/plugins/rtauto/proof_search.ml
index 2448a2d39..d772279f1 100644
--- a/plugins/rtauto/proof_search.ml
+++ b/plugins/rtauto/proof_search.ml
@@ -510,8 +510,8 @@ let pp_gl gl= cut () ++
 
 let pp =
   function
-      Incomplete(gl,ctx) -> msgnl (pp_gl gl)
-    | _ -> msg (str "<complete>")
+      Incomplete(gl,ctx) -> pp_gl gl ++ fnl ()
+    | _ -> str "<complete>"
 
 let pp_info () =
   let count_info =
diff --git a/plugins/rtauto/proof_search.mli b/plugins/rtauto/proof_search.mli
index b236aa721..275e94cde 100644
--- a/plugins/rtauto/proof_search.mli
+++ b/plugins/rtauto/proof_search.mli
@@ -38,7 +38,7 @@ val branching: state -> state list
 
 val success: state -> bool
 
-val pp: state -> unit
+val pp: state -> Pp.std_ppcmds
 
 val pr_form : form -> unit
 
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 19c09571f..221c46a92 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -416,10 +416,6 @@ let tclEVARS sigma gls = tclIDTAC {gls with sigma=sigma}
 let pp_info = ref (fun _ _ _ -> assert false)
 let set_info_printer f = pp_info := f
 
-let tclINFO (tac : tactic) gls =
-  msgnl (hov 0 (str "Warning: info is currently not working"));
-  tac gls
-
 (* Check that holes in arguments have been resolved *)
 
 let check_evars env sigma extsigma gl =
diff --git a/proofs/refiner.mli b/proofs/refiner.mli
index 75fd6d3d6..9d3d37c22 100644
--- a/proofs/refiner.mli
+++ b/proofs/refiner.mli
@@ -137,7 +137,6 @@ val tclTIMEOUT       : int -> tactic -> tactic
 val tclWEAK_PROGRESS : tactic -> tactic
 val tclPROGRESS      : tactic -> tactic
 val tclNOTSAMEGOAL   : tactic -> tactic
-val tclINFO          : tactic -> tactic
 
 (** [tclIFTHENELSE tac1 tac2 tac3 gls] first applies [tac1] to [gls] then,
    if it succeeds, applies [tac2] to the resulting subgoals,
diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml
index a044f563f..cec6fd419 100644
--- a/proofs/tacexpr.ml
+++ b/proofs/tacexpr.ml
@@ -29,6 +29,8 @@ type split_flag = bool     (* true = exists           false = split *)
 type hidden_flag = bool    (* true = internal use     false = user-level *)
 type letin_flag = bool     (* true = use local def    false = use Leibniz *)
 
+type debug = Debug | Info | Off (* for trivial / auto / eauto ... *)
+
 type glob_red_flag =
   | FBeta
   | FIota
@@ -173,9 +175,9 @@ type ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_atomic_tactic_expr =
   | TacLApply of 'constr
 
   (* Automation tactics *)
-  | TacTrivial of 'constr list * string list option
-  | TacAuto of int or_var option * 'constr list * string list option
-  | TacDAuto of int or_var option * int option * 'constr list
+  | TacTrivial of debug * 'constr list * string list option
+  | TacAuto of debug * int or_var option * 'constr list * string list option
+  | TacDAuto of debug * int or_var option * int option * 'constr list
 
   (* Context management *)
   | TacClear of bool * 'id list
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