From 1e1b6828c29b1344f50f94f9d3a6fce27a885656 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Fri, 30 Mar 2012 09:47:57 +0000
Subject: 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
---
 proofs/refiner.ml  | 4 ----
 proofs/refiner.mli | 1 -
 proofs/tacexpr.ml  | 8 +++++---
 3 files changed, 5 insertions(+), 8 deletions(-)

(limited to 'proofs')

diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 19c09571f0..221c46a926 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 75fd6d3d65..9d3d37c223 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 a044f563f7..cec6fd4199 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
-- 
cgit v1.2.3