diff options
| author | Arnaud Spiwack | 2014-08-05 17:55:48 +0200 |
|---|---|---|
| committer | Arnaud Spiwack | 2014-11-01 22:43:57 +0100 |
| commit | 967883e29a46a0fff9da8e56974468531948b174 (patch) | |
| tree | 9c9a814a92c2a7fb5006d478e6d20e16bcf74d7a /printing | |
| parent | 3c8797a7e0d6536e28b8a8e7f4256241fc79dfc8 (diff) | |
Add [Info] command.
Called with [Info n tac], runs [tac] and prints its info trace unfolding [n] level of tactic names ([0] for no unfolding at all).
Diffstat (limited to 'printing')
| -rw-r--r-- | printing/ppvernac.ml | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index b6ab7a2382..466606a9b8 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -771,14 +771,20 @@ let rec pr_vernac = function hov 2 (str"Include" ++ spc() ++ prlist_with_sep (fun () -> str " <+ ") pr_m mexprs) (* Solving *) - | VernacSolve (i,tac,deftac) -> + | VernacSolve (i,info,tac,deftac) -> let pr_goal_selector = function | SelectNth i -> int i ++ str":" | SelectId id -> pr_id id ++ str":" | SelectAll -> str"all" ++ str":" | SelectAllParallel -> str"par" in + let pr_info = + match info with + | None -> mt () + | Some i -> str"Info"++spc()++int i++spc() + in (if i = Proof_global.get_default_goal_selector () then mt() else pr_goal_selector i) ++ + pr_info ++ pr_raw_tactic tac ++ (if deftac then str ".." else mt ()) | VernacSolveExistential (i,c) -> |