diff options
| author | Arnaud Spiwack | 2014-07-31 16:08:27 +0200 |
|---|---|---|
| committer | Arnaud Spiwack | 2014-08-01 19:18:58 +0200 |
| commit | 2925c97c852efd66656edebedba543c7c8335b73 (patch) | |
| tree | befa69018bc1e698b5cc73b616cf44c704ecd9d9 /printing/pptactic.ml | |
| parent | a7a3f6510643b4fa4bc3299c5111c44b4887873d (diff) | |
New tactical [> t1…tn] to apply tactics t1…tn to the corresponding goal.
Differs from the usual t;[t1…tn] in two ways:
* It can be used without a preceding tactic
* It counts every focused subgoal, rather than considering independently the goals generated by the application of the preceding tactic on individual goals.
In other words t;[t1…tn] is [> t;[>t1…tn].. ].
Diffstat (limited to 'printing/pptactic.ml')
| -rw-r--r-- | printing/pptactic.ml | 21 |
1 files changed, 18 insertions, 3 deletions
diff --git a/printing/pptactic.ml b/printing/pptactic.ml index 2aadde7c16..0039a81bfe 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -505,15 +505,28 @@ let pr_seq_body pr tl = prlist_with_sep (fun () -> spc () ++ str "| ") pr tl ++ str " ]") +let pr_dispatch pr tl = + hv 0 (str "[>" ++ + prlist_with_sep (fun () -> spc () ++ str "| ") pr tl ++ + str " ]") + let pr_opt_tactic pr = function | TacId [] -> mt () | t -> pr t +let pr_tac_extend_gen pr tf tm tl = + prvect_with_sep mt (fun t -> pr t ++ spc () ++ str "| ") tf ++ + pr_opt_tactic pr tm ++ str ".." ++ + prvect_with_sep mt (fun t -> spc () ++ str "| " ++ pr t) tl + let pr_then_gen pr tf tm tl = hv 0 (str "[ " ++ - prvect_with_sep mt (fun t -> pr t ++ spc () ++ str "| ") tf ++ - pr_opt_tactic pr tm ++ str ".." ++ - prvect_with_sep mt (fun t -> spc () ++ str "| " ++ pr t) tl ++ + pr_tac_extend_gen pr tf tm tl ++ + str " ]") + +let pr_tac_extend pr tf tm tl = + hv 0 (str "[>" ++ + pr_tac_extend_gen pr tf tm tl ++ str " ]") let pr_hintbases = function @@ -851,6 +864,8 @@ let rec pr_tac inherited tac = hov 1 (pr_tac (lseq,E) t1 ++ pr_then () ++ spc () ++ pr_tac (lseq,L) t2), lseq + | TacDispatch tl -> pr_dispatch (pr_tac ltop) tl , lseq + | TacExtendTac (tf,t,tr) -> pr_tac_extend (pr_tac ltop) tf t tr , lseq | TacThens3parts (t1,tf,t2,tl) -> hov 1 (pr_tac (lseq,E) t1 ++ pr_then () ++ spc () ++ pr_then_gen (pr_tac ltop) tf t2 tl), |