diff options
| -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 7de3944351..e4c3dca28d 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 ":" |