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/modops.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/modops.ml')
0 files changed, 0 insertions, 0 deletions