diff options
author | 2013-03-12 23:59:40 +0000 | |
---|---|---|
committer | 2013-03-12 23:59:40 +0000 | |
commit | 69b2a2dddad32ccc8dc4a1bad707101e768f4f32 (patch) | |
tree | 01ee51768408e326f88b384dbedd35272a62d577 /test-suite/misc | |
parent | 701381d9280fa6948a4ab8ab4ad36c8674bad903 (diff) |
Restrict (try...with...) to avoid catching critical exn (part 3)
NB: this "try...with" plus the test at the next line
(if !interning_grammar || env.unb then ...)
were actually catching too many errors (for instance
error_not_enough_arguments).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16278 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite/misc')
0 files changed, 0 insertions, 0 deletions