diff options
| author | Ralf Jung | 2017-02-14 12:35:39 +0100 |
|---|---|---|
| committer | Ralf Jung | 2017-02-16 16:46:41 +0100 |
| commit | 55cb913f029308e97bd262fc18d4338f404e7561 (patch) | |
| tree | 3152c0912430102a15f1a22e5d69631431d92961 /kernel/type_errors.ml | |
| parent | 29d7872c0159d2aab7264c0577a2f5a9dc7c90c9 (diff) | |
don't require printing-only notation to be productive
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions