diff options
| author | Enrico Tassi | 2016-06-16 15:24:56 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2016-06-16 16:02:48 +0200 |
| commit | 6aac2c78ad5dec79c6ed16a50accde57c37398a9 (patch) | |
| tree | 53968b5035fd9b70d4431130cf12621f314cb187 /proofs | |
| parent | a452e436af72ccc1b8342ac6b666f0ff202cc20a (diff) | |
| parent | 791f3254cba602672b834ec3484d308db074b684 (diff) | |
Merge 'pr/191' into trunk
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/pfedit.ml | 1 | ||||
| -rw-r--r-- | proofs/proof_global.ml | 8 |
2 files changed, 8 insertions, 1 deletions
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..61fe347504 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -664,15 +664,21 @@ 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 | "all" -> Vernacexpr.SelectAll | i -> - let err_msg = "A selector must be \"all\" or a natural number." in + let err_msg = "The default selector must be \"all\" or a natural number." in begin try let i = int_of_string i in if i < 0 then Errors.error err_msg; |