diff options
| author | Matthieu Sozeau | 2014-08-28 12:37:43 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-08-28 19:55:01 +0200 |
| commit | 469c5bfc849e06d5a32d7aaabdf9b2fa3f451f4a (patch) | |
| tree | b227dd4e28501b2c325a99711fb4c659a6ac6ba2 /kernel/inductive.mli | |
| parent | 3fdfb3ccb7986b1e4c7685b440a62730107a639f (diff) | |
Fix bugs #3484 and #3546.
The unification oracle now prefers unfolding the eta-expanded form of a
projection over the primitive projection, and allows first-order
unification on applications of constructors of primitive records,
in case eta-conversion fails (disabled by previous patch on eta).
Diffstat (limited to 'kernel/inductive.mli')
0 files changed, 0 insertions, 0 deletions