| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2020-03-18 | Update headers in the whole code base. | Théo Zimmermann | |
| Add headers to a few files which were missing them. | |||
| 2020-01-16 | Move the per-architecture check of marshalled Uint63s to Values. | Pierre-Marie Pédrot | |
| 2019-11-01 | Add primitive floats to checker | Pierre Roux | |
| 2019-10-04 | Merge Direct and Indirect nodes in Opaqueproof. | Pierre-Marie Pédrot | |
| 2019-06-17 | Update ml-style headers to new year. | Théo Zimmermann | |
| 2019-02-04 | Primitive integers | Maxime Dénès | |
| This work makes it possible to take advantage of a compact representation for integers in the entire system, as opposed to only in some reduction machines. It is useful for heavily computational applications, where even constructing terms is not possible without such a representation. Concretely, it replaces part of the retroknowledge machinery with a primitive construction for integers in terms, and introduces a kind of FFI which maps constants to operators (on integers). Properties of these operators are expressed as explicit axioms, whereas they were hidden in the retroknowledge-based approach. This has been presented at the Coq workshop and some Coq Working Groups, and has been used by various groups for STM trace checking, computational analysis, etc. Contributions by Guillaume Bertholon and Pierre Roux <Pierre.Roux@onera.fr> Co-authored-by: Benjamin Grégoire <Benjamin.Gregoire@inria.fr> Co-authored-by: Vincent Laporte <Vincent.Laporte@fondation-inria.fr> | |||
| 2018-11-21 | More informative error on vo validation failure | Gaëtan Gilbert | |
| Now that the checker shares code with the kernel using md5 cic.mli doesn't work. We could md5 declarations.ml but this would miss changes to constr (and cic.mli already missed changes to names, univs). Instead we just print a bit of information (the last seen type name/annotation) when validate fails. This should help debugging when forgetting to update values.ml without the full verbosity of -debug. As such there is no need to -debug in the makefile validate target (NB: CI has an independent implementation of the validate rule since the vos are installed there). | |||
| 2018-07-20 | Fix #8043: Unsafe assignment in checker. | Pierre-Marie Pédrot | |
| We use a dedicated mutable constructor to perform a Landin knot. | |||
| 2018-02-27 | Update headers following #6543. | Théo Zimmermann | |
| 2018-01-10 | Add interfaces for checker and remove dead code. | Maxime Dénès | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |