From 5923919582bbfa207d5141d5059bd3916e501843 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sat, 22 Nov 2008 13:09:40 +0000
Subject: - Fixed minor bug #1994 in the tactic chapter of the manual [doc] -
 Improved warning when found several path to the same file in path  
 [mltop.ml4, system.ml] - Add support for "rewrite" on specific equality to
 true (i.e. eq_true)   [Datatypes.v, tactics]

PS: compilation test made over 11611 to shunt the archive-breaking 11612 and 11614



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

(limited to 'lib')

diff --git a/lib/system.ml b/lib/system.ml
index 4f21c87463..7ca62dcc8f 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -116,7 +116,8 @@ let where_in_path warn path filename =
 	    msg_warning
 	      (str filename ++ str " has been found in" ++ spc () ++
 	       hov 0 (str "[ " ++
-	         hv 0 (prlist_with_sep pr_semicolon (fun (lpe,_) -> str lpe) l)
+	         hv 0 (prlist_with_sep (fun () -> spc() ++ pr_semicolon())
+		   (fun (lpe,_) -> str lpe) l)
 	         ++ str " ];") ++ fnl () ++
 	       str "loading " ++ str f);
 	  (lpe, f) in
-- 
cgit v1.2.3