coq - The formal proof system

Age	Commit message (Expand)	Author
2019-09-25	Move cumulativity inference to the kernel.	Pierre-Marie Pédrot
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
2019-02-17	Separate variance and universe fields in inductives.	Gaëtan Gilbert
2019-02-04	Primitive integers	Maxime Dénès
2018-11-20	Use a closure for the domain argument of FProd.	Pierre-Marie Pédrot
2018-11-20	Do not wrap FProd return types in a closure.	Pierre-Marie Pédrot
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
2018-08-28	Fix #8288: cumulativity inferance ignores args to bound variables	Gaëtan Gilbert
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
2018-02-16	Fix reduction flags in inferCumulativity	Gaëtan Gilbert
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