coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Fix canonical structure resolution in unification (bug found in Ssreflect).	Matthieu Sozeau	2014-06-08
\|
*	test-suite: fix success/AdvancedCanonicalStructure.v	glondu	2010-10-05
\| \| \| \| \| \| \|	I have no idea how this test could have ever worked... (ssreflect? declarative mode?) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13501 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Automatic introduction of names given before ":" in Lemma's and	herbelin	2010-06-09
\| \| \| \| \| \| \| \| \| \|	Definition's is not so painless. It seems to however generally provide "nicer" scripts so let us keep it and update the contribs and test-suite accordingly. Also enforced that the actual introduced names to be exactly as given in the statements. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13097 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Delete trailing whitespaces in all .{v,ml} files	glondu	2009-09-17
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
*	added products and sorts as possible heads for canonical structures	corbinea	2008-02-19
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10577 85f007b7-540e-0410-9357-904b9bb8a0f7