coq - The formal proof system

Age	Commit message (Collapse)	Author
2021-03-26	Split the return type away from the signature of primitive operations.	Guillaume Melquiond
	This avoids having to drop the last element of the signature in the common case.
2021-02-26	Signed primitive integers	Ana
	Signed primitive integers defined on top of the existing unsigned ones with two's complement. The module Sint63 includes the theory of signed primitive integers that differs from the unsigned case. Additions to the kernel: les (signed <=), lts (signed <), compares (signed compare), divs (signed division), rems (signed remainder), asr (arithmetic shift right) (The s suffix is not used when importing the Sint63 module.) The printing and parsing of primitive ints was updated and the int63_syntax_plugin was removed (we use Number Notation instead). A primitive int is parsed / printed as unsigned or signed depending on the scope. In the default (Set Printing All) case, it is printed in hexadecimal.
2020-10-08	Remove occurrences of Parray.reroot.	Guillaume Melquiond

2020-07-06	Primitive persistent arrays	Maxime Dénès
	Persistent arrays expose a functional interface but are implemented using an imperative data structure. The OCaml implementation is based on Jean-Christophe Filliâtre's. Co-authored-by: Benjamin Grégoire <Benjamin.Gregoire@inria.fr> Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
2020-04-22	Remove # keywords in Primitive	Pierre Roux

2020-03-18	Update headers in the whole code base.	Théo Zimmermann
	Add headers to a few files which were missing them.
2019-11-01	Add "==", "<", "<=" in PrimFloat.v	Erik Martin-Dorel
	* Add a related test-suite in compare.v (generated by a bash script) Co-authored-by: Pierre Roux <pierre.roux@onera.fr>
2019-11-01	Add next_{up,down} primitive float functions	Pierre Roux

2019-11-01	Implement classify on primitive float	Pierre Roux

2019-11-01	Change return type of primitive float comparison	Pierre Roux
	Replace `option comparison` with `float_comparison` (:= `FEq \| FLt \| FGt \| FNotComparable`) as suggested by Guillaume Melquiond to avoid boxing and an extra match when using primitive float comparison.
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-11-01	Declare type of primitives in CPrimitives	Pierre Roux
	Rather than in typeops
2019-06-17	Update ml-style headers to new year.	Théo Zimmermann

2019-03-11	Nicer error for bad primitive types (through type_errors etc)	Gaëtan Gilbert

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-02-27	Update headers following #6543.	Théo Zimmermann

2017-08-12	Moving file primitive.ml to cPrimitive.ml to avoid conflict with OCaml.	Hugo Herbelin
	Indeed OCaml has a similar file and this conflicts, at least in debugger.