coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Fix bug when a sort is ascribed to a Record	Matthieu Sozeau	2016-03-15
\| \| \| \|	Forcefully equating it to the inferred level is not always desirable or possible.
*	Kills the useless tactic annotations "in \|- *"	letouzey	2012-07-05
\| \| \| \| \| \| \|	Most of these heavyweight annotations were introduced a long time ago by the automatic 7.x -> 8.0 translator git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15518 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
*	Correction bug #1507 (report révision 9807 de v8.1 vers trunk)	herbelin	2007-04-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9809 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
*	Ajout test bug #935	herbelin	2005-03-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6859 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout bug #255	herbelin	2004-09-24
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6127 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Il ne doit plus y avoir de preuves non terminées à la sortie du fichier	herbelin	2003-01-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3538 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Un bug dans le script	herbelin	2001-11-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2225 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Sur la cumulativité dans les tactiques	herbelin	2001-11-21
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2223 85f007b7-540e-0410-9357-904b9bb8a0f7