From bf12eb93f3f6a6a824a10878878fadd59745aae0 Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Sat, 29 Dec 2012 10:57:43 +0100
Subject: Imported Upstream version 8.4pl1dfsg

---
 tactics/extraargs.ml4 | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tactics/extraargs.ml4')

diff --git a/tactics/extraargs.ml4 b/tactics/extraargs.ml4
index d3403a18..613779c2 100644
--- a/tactics/extraargs.ml4
+++ b/tactics/extraargs.ml4
@@ -194,7 +194,7 @@ let pr_in_hyp  pr_id (lo,concl) :  Pp.std_ppcmds =
     | None,false -> str "in" ++ spc () ++ str "*" ++ spc () ++ str "|-"
     | Some l,_ ->
 	str "in" ++
-	  Util.prlist (fun id -> spc () ++ pr_id id) l ++
+         spc () ++ Util.prlist_with_sep Util.pr_comma pr_id l ++
 	  match concl with
 	    | true -> spc () ++ str "|-" ++ spc () ++ str "*"
 	    | _ -> mt ()
-- 
cgit v1.2.3