coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Update copyright headers.	Maxime Dénès	2016-01-20
\|
*	Update headers.	Maxime Dénès	2015-01-12
\|
*	Fixing TestRefine test-suite file.	Pierre-Marie Pédrot	2014-09-08
\|
*	Fix the refine related test-suite files to account for the new refine.	Arnaud Spiwack	2013-12-06
\|
*	Updating headers.	herbelin	2012-08-08
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Changed encoding from ISO-8859-1 to UTF-8 for some remaining gallina files.	ppedrot	2012-06-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15431 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Updated all headers for 8.3 and trunk	herbelin	2010-07-24
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13323 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
*	Slight change of the semantics of user-given casts: they don't really	msozeau	2008-11-07
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	help the type _checking_ anymore (they don't become typing constraints) but they permit to coerce a subterm in a type. In particular, when using a VM cast we avoid unneeded, unexpected conversions using the default machine (oops!). Also remove the corresponding comment in pretyping and fix the wrong use of casts in toplevel/command: accept the trouble of using evars. This has the somewhat adverse effect that when typing casted object we now have no typing constraints (see e.g. examples in Cases.v)! Probably, this will be backtracked partially tomorrow as many contribs can rely on it and the change could make some unifications fail (in particular with deep coercions). Let's try anyway! git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11558 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correction du bug 808: il est maintenant interdit de déclarer une ↵	coq	2006-03-02
\| \| \| \| \| \|	assomption en cours de preuve. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8109 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Abandon tests syntaxe v7; remplacement des .v par des fichiers en syntaxe v8	herbelin	2005-12-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7693 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Activation du test de Refine en v7 pour mémoire avant passage à la v8	herbelin	2005-12-21
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7688 85f007b7-540e-0410-9357-904b9bb8a0f7