diff options
| author |  Cyprien Mangin <cyprien.mangin@m4x.org> | 2016-06-03 08:04:38 +0200 |
|---|---|---|
| committer | Cyprien Mangin <cyprien.mangin@m4x.org> | 2016-06-14 06:21:30 +0200 |
| commit | 5822bdc9689620db3f9b7e5ea159d024cf213ba9 (patch) | |
| tree | 0fae337d395c9bfe589e8a7aae99f32f6baf822f /proofs | |
| 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 'proofs')
| -rw-r--r-- | proofs/pfedit.ml | 1 | ||||
| -rw-r--r-- | proofs/proof_global.ml | 6 |
2 files changed, 7 insertions, 0 deletions
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index 2863384b5..bf1da8ac0 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -115,6 +115,7 @@ let solve ?with_end_tac gi info_lvl tac pr = in let tac = match gi with | Vernacexpr.SelectNth i -> Proofview.tclFOCUS i i tac + | Vernacexpr.SelectList l -> Proofview.tclFOCUSLIST l tac | Vernacexpr.SelectId id -> Proofview.tclFOCUSID id tac | Vernacexpr.SelectAll -> tac in diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 36277bf58..be353b10a 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -664,9 +664,15 @@ let _ = let default_goal_selector = ref (Vernacexpr.SelectNth 1) let get_default_goal_selector () = !default_goal_selector +let print_range_selector (i, j) = + if i = j then string_of_int i + else string_of_int i ^ "-" ^ string_of_int j + let print_goal_selector = function | Vernacexpr.SelectAll -> "all" | Vernacexpr.SelectNth i -> string_of_int i + | Vernacexpr.SelectList l -> "[" ^ + String.concat ", " (List.map print_range_selector l) ^ "]" | Vernacexpr.SelectId id -> Id.to_string id let parse_goal_selector = function |