coq - The formal proof system

Age	Commit message (Collapse)	Author
2021-01-04	Change the representation of kernel case.	Pierre-Marie Pédrot
	We store bound variable names instead of functions for both branches and predicate, and we furthermore add the parameters in the node. Let bindings are not taken into account and require an environment lookup for retrieval.
2020-11-16	Improve bad variance error message: mention expected and actual variances	Gaëtan Gilbert

2020-11-16	Infrastructure for cumulative inductive syntax (no grammar extension yet)	Gaëtan Gilbert

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-07-01	UIP in SProp	Gaëtan Gilbert

2020-04-06	Use lists instead of arrays in evar instances.	Pierre-Marie Pédrot
	This corresponds more naturally to the use we make of them, as we don't need fast indexation but we instead keep pushing terms on top of them.
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-14	infercumulativity: take less arguments	Gaëtan Gilbert

2019-12-16	Remove variance info from inductive entries, infer in indtyping	Gaëtan Gilbert
	It gets thrown away if the inductive is declared in a section anyway, and there is no user syntax to specify it.
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-09-25	Clean up InferCumulativity after its move to the kernel.	Pierre-Marie Pédrot

2019-09-25	Move cumulativity inference to the kernel.	Pierre-Marie Pédrot
	This is not quite pretty, but it is needed by the section mechanism to rebuild an inductive when closing a section. Hopefully this can be moved back at some point.