| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2019-11-01 | Add primitive float computation in Coq kernel | Guillaume Bertholon | |
| 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. | |||
| 2019-08-18 | [api] Move `Keys` to pretyping | Emilio Jesus Gallego Arias | |
| This file is unrelated to library, but to pretyping/unification. This commit, along with others already submitted go towards the goal of `library` containing only the handling of library objects. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |