diff options
author | 2015-10-24 12:01:26 +0200 | |
---|---|---|
committer | 2015-10-24 12:14:24 +0200 | |
commit | 1b029b2163386f20179a61f6bdb68e5532f4c306 (patch) | |
tree | fa58a62145fa61d9823a79a04dba8571317ff4c4 /kernel/mod_typing.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/mod_typing.mli')
0 files changed, 0 insertions, 0 deletions