diff options
| author | Hugo Herbelin | 2016-05-15 10:40:16 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2016-06-16 17:43:29 +0200 |
| commit | 63ac502a4ea7f5c81346deeecfcf0d69d063a130 (patch) | |
| tree | 0ed99e6fa129b8a7413859b7b57073ca5d2dc388 /kernel/type_errors.ml | |
| parent | 818422ad1ff602d692f712733517e26db013bfa8 (diff) | |
Fixing printing of Register retroknowledge.
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions