diff options
| author | Cyprien Mangin | 2016-06-03 08:04:38 +0200 |
|---|---|---|
| committer | Cyprien Mangin | 2016-06-14 06:21:30 +0200 |
| commit | 5822bdc9689620db3f9b7e5ea159d024cf213ba9 (patch) | |
| tree | 0fae337d395c9bfe589e8a7aae99f32f6baf822f /ltac | |
| parent | 19330a458b907b5e66a967adbfe572d92194913c (diff) | |
Add goal range selectors.
You can now write [[1, 3-5]:tac.] to apply [tac] on the subgoals
numbered 1 and 3 to 5.
Diffstat (limited to 'ltac')
| -rw-r--r-- | ltac/g_ltac.ml4 | 13 |
1 files changed, 13 insertions, 0 deletions
diff --git a/ltac/g_ltac.ml4 b/ltac/g_ltac.ml4 index 3579fc10f6..7de3944351 100644 --- a/ltac/g_ltac.ml4 +++ b/ltac/g_ltac.ml4 @@ -295,9 +295,15 @@ GEXTEND Gram tactic: [ [ tac = tactic_expr -> tac ] ] ; + + range_selector: + [ [ n = natural ; "-" ; m = natural -> (n, m) + | n = natural -> (n, n) ] ] + ; selector: [ [ n=natural; ":" -> Vernacexpr.SelectNth n | test_bracket_ident; "["; id = ident; "]"; ":" -> Vernacexpr.SelectId id + | "[" ; l = LIST1 range_selector SEP "," ; "]" ; ":" -> Vernacexpr.SelectList l | IDENT "all" ; ":" -> Vernacexpr.SelectAll ] ] ; tactic_mode: @@ -336,8 +342,15 @@ let vernac_solve n info tcom b = p,status) in if not status then Feedback.feedback Feedback.AddedAxiom +let pr_range_selector (i, j) = + if i = j then int i + else int i ++ str "-" ++ int j + let pr_ltac_selector = function | SelectNth i -> int i ++ str ":" +(* Special case to distinguish between 1: and 1-1: *) +| SelectList [(i, j)] when i = j -> int i ++ str "-" ++ int j +| SelectList l -> prlist_with_sep (fun () -> str ", ") pr_range_selector l | SelectId id -> str "[" ++ Nameops.pr_id id ++ str "]" ++ str ":" | SelectAll -> str "all" ++ str ":" |