diff options
author | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-06-11 08:30:07 +0200 |
---|---|---|
committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-06-11 08:32:48 +0200 |
commit | d095d43f09162f3365392f91ebdd48fcf83d9147 (patch) | |
tree | 624580df096a42c75f7623cc48629f668ea1b784 /library/declare.ml | |
parent | 4de7d7fb63a68b766126ae467be1e9bc00b92948 (diff) |
Fixing a try with in apply that has become too weak in 8.5.
Don't know however what should be the right guard to this try. Now
using catchable_exception, but even in 8.4, Failure was caught, which
is strange.
Diffstat (limited to 'library/declare.ml')
0 files changed, 0 insertions, 0 deletions