diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2015-06-25 14:04:49 +0200 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2015-06-29 22:16:07 +0200 |
| commit | 38da14404781843a6143fc4af9d503e05d8d7dd6 (patch) | |
| tree | ca11ea317485d4f37ae9dd08608ea973d5eeefe2 /library/library.mllib | |
| parent | 671e556453c1eee335cf788ebc72675f5a7483d8 (diff) | |
class_tactics: remove catch-all, use Errors.noncritical
Diffstat (limited to 'library/library.mllib')
0 files changed, 0 insertions, 0 deletions