diff options
author | 2016-06-03 08:06:15 +0200 | |
---|---|---|
committer | 2016-06-14 06:21:30 +0200 | |
commit | 8beceb7e73480c72b8e9d319d94ae1a9202418a5 (patch) | |
tree | 33e0ff719317943de30f8420801bb069c3a4c247 /ltac | |
parent | 4962e042f3b2d7c5b089cec2dfe4e07a46bd2231 (diff) |
Fix the pretty-printing of goal range selectors.
Diffstat (limited to 'ltac')
-rw-r--r-- | ltac/g_ltac.ml4 | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/ltac/g_ltac.ml4 b/ltac/g_ltac.ml4 index 7de394435..e4c3dca28 100644 --- a/ltac/g_ltac.ml4 +++ b/ltac/g_ltac.ml4 @@ -348,9 +348,8 @@ let pr_range_selector (i, 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 +| SelectList l -> str "[" ++ prlist_with_sep (fun () -> str ", ") pr_range_selector l ++ + str "]" ++ str ":" | SelectId id -> str "[" ++ Nameops.pr_id id ++ str "]" ++ str ":" | SelectAll -> str "all" ++ str ":" |