coq - The formal proof system

Age	Commit message (Collapse)	Author
2018-10-04	rename test files (do not start by a digit)	Vincent Laporte

2017-07-27	test-suite: more use of the new command Extraction TestCompile	Pierre Letouzey

2017-06-14	Prelude : no more autoload of plugins extraction and recdef	Pierre Letouzey
	The user now has to manually load them, respectively via: Require Extraction Require Import FunInd The "Import" in the case of FunInd is to ensure that the tactics functional induction and functional inversion are indeed in scope. Note that the Recdef.v file is still there as well (it contains complements used when doing Function with measures), and it also triggers a load of FunInd.v. This change is correctly documented in the refman, and the test-suite has been adapted.
2014-06-10	Add many more cases to the test-suite	Jason Gross
	I'd add more, but I'm tired and it's late and I should sleep. Maybe I'll pick up at 3279 (working down) another day. Bug 3344 is broken; [Fail Defined.] says that [Defined] has not failed, even though it raises an anomaly. So there's no way I can think of to test it. I've left it in the [opened] directory anyway.