coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Fix some typos.	Guillaume Melquiond	2015-10-13
\|
*	"allows to", like "allowing to", is improper	Jason Gross	2014-08-25
\| \| \| \| \| \| \| \| \| \| \|	It's possible that I should have removed more "allows", as many instances of "foo allows to bar" could have been replaced by "foo bars" (e.g., "[Qed] allows to check and save a complete proof term" could be "[Qed] checks and saves a complete proof term"), but not always (e.g., "the optional argument allows to ignore universe polymorphism" should not be "the optional argument ignores universe polymorphism" but "the optional argument allows the caller to instruct Coq to ignore universe polymorphism" or something similar).
*	Hopefully a fix for #2176 (redirection not understood with some shells)	herbelin	2010-09-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13437 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fixed bug 2030 (bad syntax for "test" in doc compilation) [see 11824	herbelin	2009-01-21
\| \| \| \| \| \| \| \|	from v8.2 branch]. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11825 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Propriétés svn pour les filtres latex	notin	2009-01-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11807 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Backporting from v8.2 to trunk:	herbelin	2009-01-18
\| \| \| \| \| \| \| \| \| \|	- Filtering of doc compilation messages (11793,11795,11796). - Fixing bug #1925 and cleaning around bug #1894 (11796, 11801). - Adding some tests. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11802 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Nettoyage de l'archive doc et restructuration avant intégration à l'archive	herbelin	2006-02-23
	principale de Coq et publication des sources (HH) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8606 85f007b7-540e-0410-9357-904b9bb8a0f7