| Age | Commit message (Collapse) | Author |
|---|
|
Beware of 0. = -0. issue for primitive floats
The IEEE 754 declares that 0. and -0. are treated equal but we cannot
say that this is true with Leibniz equality.
Therefore we must patch the equality and the total comparison inside the
kernel to prevent inconsistency.
|
|
Opening up a lambda should always lift the substitution attached to it.
|
|
Most of these files were introduced after #6543 but used older headers
copied from somewhere else.
|
|
|
|
Prevent errors when under annotating binders.
|
|
Kernel should be mostly correct, higher levels do random stuff at
times.
|
