diff options
| author | Matthieu Sozeau | 2015-06-28 15:23:00 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2015-06-28 15:27:38 +0200 |
| commit | 02663c526a3fd347fad803eb664d22e6b5c088ad (patch) | |
| tree | 32ac40ac32acbd4a5363fa1fb912672a66c090f4 /kernel/nativecode.ml | |
| parent | 902ce91fd6006e6df57a8d5133676981967d49b4 (diff) | |
Fix incompleteness of conversion used by evarconv
In case we need to backtrack on universe inconsistencies when converting
two (incompatible) instances of the same constant and unfold them.
Bug reported by Amin Timany.
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions