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-08-21	Ensuring all .v files end with a newline to make "sed -i" work better on them.	Hugo Herbelin

2017-05-01	remove unneeded -emacs flag to coq-prog-args	Paul Steckler

2015-10-07	Univs: add Strict Universe Declaration option (on by default)	Matthieu Sozeau
	This option disallows "declare at first use" semantics for universe variables (in @{}), forcing the declaration of _all_ universes appearing in a definition when introducing it with syntax Definition/Inductive foo@{i j k} .. The bound universes at the end of a definition/inductive must be exactly those ones, no extras allowed currently. Test-suite files using the old semantics just disable the option.
2014-10-07	Fix test-suite file 3352 which was containing the wrong test.	Matthieu Sozeau

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.