From e4c505927b0ebe06f87ecc14567431822e8e0b5c Mon Sep 17 00:00:00 2001
From: letouzey
Date: Mon, 5 Sep 2011 16:46:50 +0000
Subject: Util.error now creates UserError(_,msg) instead of UserError(str,str)

 This only affects display of errors when flag -debug is used,
 and it avoids strange message like "Error: in msg: msg"

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

(limited to 'lib')

diff --git a/lib/util.ml b/lib/util.ml
index 688d415840..f7be7b0d73 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -16,7 +16,7 @@ let anomaly string = raise (Anomaly(string, str string))
 let anomalylabstrm string pps = raise (Anomaly(string,pps))
 
 exception UserError of string * std_ppcmds (* User errors *)
-let error string = raise (UserError(string, str string))
+let error string = raise (UserError("_", str string))
 let errorlabstrm l pps = raise (UserError(l,pps))
 
 exception AlreadyDeclared of std_ppcmds (* for already declared Schemes *)
-- 
cgit v1.2.3