diff options
| author | Hugo Herbelin | 2015-10-24 12:01:26 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2015-10-24 12:14:24 +0200 |
| commit | 1b029b2163386f20179a61f6bdb68e5532f4c306 (patch) | |
| tree | fa58a62145fa61d9823a79a04dba8571317ff4c4 /kernel/type_errors.mli | |
| parent | 3df7e2a89ae931207781c6f5cbc9e196235b1dc3 (diff) | |
Fixing a loop in checking hints with holes.
For instance, "Hint Resolve (fst _ _)." was looping (bug in 841bc461).
Diffstat (limited to 'kernel/type_errors.mli')
0 files changed, 0 insertions, 0 deletions