diff options
| author | letouzey | 2013-03-17 00:04:17 +0000 |
|---|---|---|
| committer | letouzey | 2013-03-17 00:04:17 +0000 |
| commit | 60902645ba29f967883fdfe8aa46ef6f4a80ac7d (patch) | |
| tree | 017ac51b44d98e703d9cd4fff76ff6859e2d3753 /lib/errors.mli | |
| parent | de861c582eb09324ef10f64c1b2107f16a41439a (diff) | |
Avoid a few overzealous "when Errors.noncritical"
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16309 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'lib/errors.mli')
0 files changed, 0 insertions, 0 deletions