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

1 files changed, 9 insertions, 9 deletions

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]