coq - The formal proof system

Age	Commit message (Collapse)	Author
2018-01-20	Adding a test for coqchk bug #6619.	Pierre-Marie Pédrot

2017-08-21	Ensuring all .v files end with a newline to make "sed -i" work better on them.	Hugo Herbelin

2017-07-31	Change the option for cumulativity	Amin Timany

2017-06-16	Clean up universes of constants and inductives	Amin Timany

2017-06-16	Move (part of) tests from checker to success	Amin Timany
	Due to some unknown problem coqchk fails on some inductive types when it is compiled with ocaml4.02.3+32bit and camlp5-4.16 which is the case for Travis tests.
2017-06-16	Checker add test for non-trivial constraints	Amin Timany

2017-06-16	Change the option to Set Inductive Cumulativity	Amin Timany
	This requires to change the status of Inductive (we have also changed CoInductive and Variant) from keyword to identifier.
2017-06-16	Correct coqchk reduction	Amin Timany

2017-05-30	Add test-suite checks for coqchk with constraints	Jason Gross

2015-07-07	Checker: Fix bug #4282	Matthieu Sozeau
	Adapt to new [projection] abstract type comprising a constant and a boolean.
2014-12-26	new test for coqchk	Enrico Tassi