From c80629095a5e2d4e86098d7a2462028ef291c585 Mon Sep 17 00:00:00 2001
From: ppedrot
Date: Thu, 23 May 2013 13:44:05 +0000
Subject: Fixing #3042

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16530 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 lib/pp.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'lib')

diff --git a/lib/pp.ml b/lib/pp.ml
index 427c60b8f6..c3cef6cda3 100644
--- a/lib/pp.ml
+++ b/lib/pp.ml
@@ -404,7 +404,7 @@ let pr_nth n =
 
 (* [prlist pr [a ; ... ; c]] outputs [pr a ++ ... ++ pr c] *)
 
-let prlist elem l = List.fold_left (++) Glue.empty (List.rev (List.map elem l))
+let prlist pr l = List.fold_left (fun x e -> x ++ pr e) Glue.empty l
 
 (* unlike all other functions below, [prlist] works lazily.
    if a strict behavior is needed, use [prlist_strict] instead.
-- 
cgit v1.2.3