coq - The formal proof system

Age	Commit message (Collapse)	Author
2021-03-26	Document as critical.	Guillaume Melquiond

2021-02-17	Add an entry to file critical-bugs.	Guillaume Melquiond

2020-11-20	Make sure accumulators do not exceed the minor heap (partly fix #11170).	Guillaume Melquiond
	Accumulators can grow arbitrarily large, even when well-typed. So, this commit makes sure they are allocated on the major heap when they are too large. If so, fields need to be filled with caml_initialize, in case they point to the minor heap.
2020-11-12	Add documentation about the soundness bug.	Pierre-Marie Pédrot

2020-06-09	Update dev/doc/critical-bugs	Pierre Roux

2020-01-22	Fix #11421 computation of Set+2	Gaëtan Gilbert

2019-12-27	Add critical-bugs entry, tests-suite file, and code comment.	Guillaume Melquiond

2019-11-26	Fix #11039: proof of False with template poly and nonlinear universes	Gaëtan Gilbert
	Using the parameter universes in the constructor causes implicit equality constraints, so those universes may not be template polymorphic. A couple types in the stdlib were erroneously marked template, which is now detected. Removing the marking doesn't actually change behaviour though. Also fixes #10504.
2019-11-07	The "univ poly can capture global univs" checker side bug is fixed	Gaëtan Gilbert
	(by the checker refactor AFAICT) + fix commit for the coqtop side fix (it got rebased at some point) Close #10705
2019-10-16	Fix a De Bruijn bug in the computation of term relevance in the kernel.	Pierre-Marie Pédrot
	Opening up a lambda should always lift the substitution attached to it.
2019-09-25	Adding documentation for the move of sections data to kernel.	Pierre-Marie Pédrot

2019-08-30	Adding a critical-bugs entry. Description from Hugo Herbelin.	Pierre-Marie Pédrot

2019-04-29	Merge PR #9925: [vm] Protect accu and coq_env	Maxime Dénès
	Ack-by: Zimmi48 Reviewed-by: maximedenes Ack-by: proux01 Reviewed-by: vbgl
2019-04-15	Update critical-bugs	Pierre Roux

2019-04-05	[native compiler] Fix critical bug with primitive projections	Maxime Dénès
	Since e1e7888, stuck projections were not computed correctly. Fixes #9684
2019-03-26	Fix reproduction info for some past critical bugs	Gaëtan Gilbert
	- test-suite/bugs/closed/xx.v renamed to .../bug_xx.v - test-suite/failure/inductive4.v is now .../inductive.v - repro for #4157 now added to the repo (it was in an unmerged commit on @herbelin's repo) - commit message of 244d7a9aa contains a repro for its bug (I didn't bother adding to the test suite as a return of the bug could just as well use different strings so the specific repro wouldn't test anything useful)
2019-03-26	Incorrect details in critical bug info (prop_set_proof_irrelevance)	Gaëtan Gilbert

2018-09-13	Add entry for universe polymorphism critical bug	Gaëtan Gilbert

2018-06-25	Critical bugs: added #3243 and Gonthier's bug in lazy machine.	Hugo Herbelin
	Both reminded by Enrico.
2018-06-15	Very first try at listing the critical bugs of the history of Coq.	Hugo Herbelin
	I let open several questions about fixes to the kernel which maybe were not critical. I skipped what seemed to have been bugs in beta-releases. Need double-checks, decision about the format, etc.