diff options
| author | Hugo Herbelin | 2016-09-10 11:31:01 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2016-09-10 11:34:08 +0200 |
| commit | 43104a0b94e42fb78764b5d1365ca1e85a158508 (patch) | |
| tree | 68943411671327facf236b25c6cabd63b96f90d0 /kernel | |
| parent | 7a037b8c1de11b18d47b01e5b0262090f32bfc40 (diff) | |
Fixing #5077 (failure on typing a fixpoint with evars in its type).
Typing.type_of was using conversion for types of fixpoints while it
could have used unification.
Diffstat (limited to 'kernel')
0 files changed, 0 insertions, 0 deletions