diff options
| author | letouzey | 2011-09-05 16:46:50 +0000 |
|---|---|---|
| committer | letouzey | 2011-09-05 16:46:50 +0000 |
| commit | e4c505927b0ebe06f87ecc14567431822e8e0b5c (patch) | |
| tree | b466d6987134703e2e5e87ad2c6ed6e7bd628455 /lib/util.ml | |
| parent | bdf8b4edb650c847f83d520d31f23f14c58233b6 (diff) | |
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
Diffstat (limited to 'lib/util.ml')
| -rw-r--r-- | lib/util.ml | 2 |
1 files changed, 1 insertions, 1 deletions
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 *) |