diff options
| author | Théo Zimmermann | 2016-11-30 15:00:13 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2016-11-30 16:41:47 +0100 |
| commit | 823f0ab9c34f99d9171a5332a535c20d9f0f315c (patch) | |
| tree | 53821ba9a73ebe229b1408472504e8a147d2497d /kernel/type_errors.ml | |
| parent | 3e6fa1cbdc0ec145728089000595b6ea29f37a4c (diff) | |
Fix typeclasses eauto shelving.
A file in the test-suite had to be modified.
It was supposed to reproduce a behavior in intuistionistic-nuprl
but it did not really.
This commit is not supposed to break intuistionistic-nuprl.
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions