diff options
| author | Matej Košík | 2017-04-10 16:03:27 +0200 |
|---|---|---|
| committer | Matej Košík | 2017-04-10 16:03:27 +0200 |
| commit | c6f7619e1d8c2971041610f31b4be3e468f68593 (patch) | |
| tree | 8ffb803784d3be7abd274151596cce81477d90a6 /kernel/type_errors.ml | |
| parent | 538d8edf708ba049e60e6bc32902ba5fdca720bb (diff) | |
Revert "comments: corrected in the Context module"
This reverts commit 538d8edf708ba049e60e6bc32902ba5fdca720bb.
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions