coq - The formal proof system

Age	Commit message (Collapse)	Author
2020-01-07	Fix test-suite fo non maximal implicit arguments	SimonBoulier

2019-01-30	[toplevel] Deprecate the `-compile` flag in favor of `coqc`.	Emilio Jesus Gallego Arias
	This PR deprecates the use of `coqtop` as a compiler. There is no point on having two binaries with the same purpose; after the experiment in #8690, IMHO we have a lot to gain in terms of code organization by splitting the compiler and the interactive binary. We adapt the documentation and adapt the test-suite. Note that we don't make `coqc` a true binary yet, but here we take care only of the user-facing part. The conversion of the binary will take place in #8690 and will bring code simplification, including a unified handling of arguments.
2018-03-30	Change Implicit Arguments to Arguments in test-suite	Jasper Hugunin

2013-01-21	Last test-suite not in Symmetric Patterns syntax	pboutill
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16132 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-09-17	Delete trailing whitespaces in all .{v,ml} files	glondu
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-03-04	illegal tactic application was having Ltac interpreter loop	barras
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11963 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-04-14	Ajout d'un test de complexité de injection (cf bug 1173)	herbelin
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9769 85f007b7-540e-0410-9357-904b9bb8a0f7