diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-03-30 09:47:57 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-03-30 09:47:57 +0000 |
| commit | 1e1b6828c29b1344f50f94f9d3a6fce27a885656 (patch) | |
| tree | e0b7c5a490f8f650262d6a1457b5c64668bd76a2 /proofs | |
| parent | 534cbe4f02392c45567ea30d02b53751482ed767 (diff) | |
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
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/refiner.ml | 4 | ||||
| -rw-r--r-- | proofs/refiner.mli | 1 | ||||
| -rw-r--r-- | proofs/tacexpr.ml | 8 |
3 files changed, 5 insertions, 8 deletions
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 |