diff options
| author | Matthieu Sozeau | 2014-06-25 18:25:46 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-06-25 20:00:10 +0200 |
| commit | 6a778ef90ed626ead64e86e1eec5c506514bb00e (patch) | |
| tree | ae405974811f922e29dd9e449f3635f4c90b902b /kernel/type_errors.mli | |
| parent | 753b8f4aaa78fe1cf8ea033d8cf45e88b5da9d13 (diff) | |
In rewrite, wrong computation of the sort of the term to be rewritten in
generated an uncaught Not_found. This raises an anomaly now and the sort is
properly computed now (fixes a bug in CoLoR).
Diffstat (limited to 'kernel/type_errors.mli')
0 files changed, 0 insertions, 0 deletions