coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	[Sphinx] Better error message for coqtop errors	Maxime Dénès	2018-03-16
\|
*	[Sphinx] Increase coqtop timeout to avoid spurious failures on CI	Maxime Dénès	2018-03-16
\|
*	[Sphinx] Add a few grammar constructions	Maxime Dénès	2018-03-12
\| \| \| \|	Code from Paul Steckler (MIT).
*	Moving Gitlab CI documentation build to the main Coq build.	Maxime Dénès	2018-03-09
\|
*	Integration of a sphinx-based documentation generator.	Maxime Dénès	2018-03-09
\| \| \| \| \| \| \| \|	The original contribution is from Clément Pit-Claudel. I updated his code and integrated it with the Coq build system. Many improvements by Paul Steckler (MIT). This commit adds the infrastructure but no content.
*	[flags] Remove XML output flag.	Emilio Jesus Gallego Arias	2017-08-01
\| \| \| \| \| \| \| \|	This is a second try at removing the hooks for the legacy xml export system which can't currently be tested. It is also not included in the API, so it should either be included in it or this PR be applied.
*	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