diff options
author | 2011-09-05 16:46:50 +0000 | |
---|---|---|
committer | 2011-09-05 16:46:50 +0000 | |
commit | e4c505927b0ebe06f87ecc14567431822e8e0b5c (patch) | |
tree | b466d6987134703e2e5e87ad2c6ed6e7bd628455 /doc | |
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 'doc')
0 files changed, 0 insertions, 0 deletions