From 5822bdc9689620db3f9b7e5ea159d024cf213ba9 Mon Sep 17 00:00:00 2001
From: Cyprien Mangin
Date: Fri, 3 Jun 2016 08:04:38 +0200
Subject: Add goal range selectors.

You can now write [[1, 3-5]:tac.] to apply [tac] on the subgoals
numbered 1 and 3 to 5.
---
 proofs/pfedit.ml       | 1 +
 proofs/proof_global.ml | 6 ++++++
 2 files changed, 7 insertions(+)

(limited to 'proofs')

diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 2863384b59..bf1da8ac05 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 36277bf58d..be353b10ae 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
-- 
cgit v1.2.3