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