diff options
| author | Cyprien Mangin | 2016-06-03 08:06:15 +0200 |
|---|---|---|
| committer | Cyprien Mangin | 2016-06-14 06:21:30 +0200 |
| commit | 8beceb7e73480c72b8e9d319d94ae1a9202418a5 (patch) | |
| tree | 33e0ff719317943de30f8420801bb069c3a4c247 | |
| parent | 4962e042f3b2d7c5b089cec2dfe4e07a46bd2231 (diff) | |
Fix the pretty-printing of goal range selectors.
| -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 ":" |