aboutsummaryrefslogtreecommitdiff
path: root/Makefile.common
diff options
context:
space:
mode:
authorMatthieu Sozeau2015-06-28 15:23:00 +0200
committerMatthieu Sozeau2015-06-28 15:27:38 +0200
commit02663c526a3fd347fad803eb664d22e6b5c088ad (patch)
tree32ac40ac32acbd4a5363fa1fb912672a66c090f4 /Makefile.common
parent902ce91fd6006e6df57a8d5133676981967d49b4 (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 'Makefile.common')
0 files changed, 0 insertions, 0 deletions