aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing/pptactic.ml
diff options
context:
space:
mode:
authorGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-03-30 09:47:57 +0000
committerGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-03-30 09:47:57 +0000
commit1e1b6828c29b1344f50f94f9d3a6fce27a885656 (patch)
treee0b7c5a490f8f650262d6a1457b5c64668bd76a2 /parsing/pptactic.ml
parent534cbe4f02392c45567ea30d02b53751482ed767 (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 'parsing/pptactic.ml')
-rw-r--r--parsing/pptactic.ml27
1 files changed, 17 insertions, 10 deletions
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 *)