aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/misc
diff options
context:
space:
mode:
authorGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2013-03-12 23:59:40 +0000
committerGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2013-03-12 23:59:40 +0000
commit69b2a2dddad32ccc8dc4a1bad707101e768f4f32 (patch)
tree01ee51768408e326f88b384dbedd35272a62d577 /test-suite/misc
parent701381d9280fa6948a4ab8ab4ad36c8674bad903 (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