From 8beceb7e73480c72b8e9d319d94ae1a9202418a5 Mon Sep 17 00:00:00 2001
From: Cyprien Mangin
Date: Fri, 3 Jun 2016 08:06:15 +0200
Subject: Fix the pretty-printing of goal range selectors.

---
 ltac/g_ltac.ml4 | 5 ++---
 1 file 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 ":"
 
-- 
cgit v1.2.3