diff options
| author | Hugo Herbelin | 2016-06-12 15:56:06 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2016-06-12 16:03:39 +0200 |
| commit | 59e1618ccda6bbc9c627df93db7aaa3ea5930ccf (patch) | |
| tree | ee9a21287ab6febe15dfd528dafe1ece01f6190d /pretyping/pretype_errors.ml | |
| parent | 78102fedf6b1dca94cf2695bb1ba2000d4f76db9 (diff) | |
Protecting eta-expansion in evarconv.ml against ill-typed problems.
This can happen with the "with" clause (see e.g. #4782), but also with
recursive calls in first-order unification (e.g. "?n a a b = f a" when
a matching between "b" and "a" is tried before expanding f).
Diffstat (limited to 'pretyping/pretype_errors.ml')
0 files changed, 0 insertions, 0 deletions