coq - The formal proof system

Age	Commit message (Collapse)	Author
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.
2019-06-17	Update ml-style headers to new year.	Théo Zimmermann

2019-04-25	inferCumulativity: shortcut for all-Invariant inductives	Gaëtan Gilbert

2019-03-14	Repair relevance marks in-kernel.	Gaëtan Gilbert
	Prevent errors when under annotating binders.
2019-02-17	Separate variance and universe fields in inductives.	Gaëtan Gilbert
	I think the usage looks cleaner this way.
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-20	Use a closure for the domain argument of FProd.	Pierre-Marie Pédrot
	The use of a term is not needed for the fast typing algorithm of the application case, so this tweak brings the best of both worlds.
2018-11-20	Do not wrap FProd return types in a closure.	Pierre-Marie Pédrot
	There is little point to this as the type is dependent on an open value and is never computed further.
2018-11-09	Adding universe names to polymorphic entry instances.	Pierre-Marie Pédrot

2018-10-26	Remove a few circumvolutions around parameters of inductive entries	Maxime Dénès

2018-10-04	Remove FCast from CClosure.fterm.	Pierre-Marie Pédrot
	Just like in the Sixth Sense, it turns out it was dead code all along.
2018-08-28	Fix #8288: cumulativity inferance ignores args to bound variables	Gaëtan Gilbert
	(NB: only variables whose binder is inside the constructor argument, ie Inductive foo := C : forall A : Type -> Type, A Type -> foo. does not trigger the bug because A becomes a RelKey.)
2018-03-09	Merge PR #6769: Split closure cache and remove whd_both	Maxime Dénès

2018-03-04	Pass the constant cache as a separate argument in kernel reduction.	Pierre-Marie Pédrot

2018-02-27	Update headers following #6543.	Théo Zimmermann

2018-02-16	Cleaner treatment of parameters in inferCumulativity	Gaëtan Gilbert
	No using a mutable counter to skip them, instead we keep them in the environment.
2018-02-16	Fix reduction flags in inferCumulativity	Gaëtan Gilbert
	The only difference is when we have a rel local definition in the initial environment, which isn't actually possible. However that depends on the specific way we treat parameters.
2018-02-11	inferCumulativity: add comment to explain [if not is_arity].	Gaëtan Gilbert

2018-02-11	Use specialized function for inductive subtyping inference.	Gaëtan Gilbert
	This ensures by construction that we never infer constraints outside the variance model.