| Age | Commit message (Collapse) | Author |
|---|
|
This module used to do retyping for the kernel in prototypes of SProp,
but was switched to only relevance inference before the merge.
|
|
Add headers to a few files which were missing them.
|
|
Rels that exist inside the environment at the time of the closure creation
are fetched in the global environment, while we only use the local list of
relevance for FRels. All the infrastructure was implicitly relying on this
kind of behaviour before the introduction of SProp.
Fixes #11150: pattern is 10x slower in Coq 8.10.0
|
|
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.
|
