coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Update tutorial (fix bug #4699).	Guillaume Melquiond	2016-04-28
\|
*	Fixing tutorial.	Pierre-Marie Pédrot	2015-09-21
\| \| \| \|	The V7 to V8 translator lost part of term annotations.
*	Remove some outdated files and fix permissions.	Guillaume Melquiond	2015-07-31
\|
*	Switch the few remaining iso-latin-1 files to utf8	Pierre Letouzey	2014-12-09
\|
*	"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).
*	Prevent coq_tex from generating curly quotes. (Partial fix for bug #2964)	Guillaume Melquiond	2014-04-28
\|
*	Renaming SearchAbout into Search and Search into SearchHead.	herbelin	2013-04-17
\| \| \| \| \| \|	I hope I did not forget any place to change. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16423 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Remove the svn-specific $Id$ annotations	letouzey	2010-04-29
\| \| \| \| \| \| \| \| \| \| \|	- Many of them were broken, some of them after Pierre B's rework of mli for ocamldoc, but not only (many bad annotation, many files with no svn property about Id, etc) - Useless for those of us that work with git-svn (and a fortiori in a forthcoming git-only setting) - Even in svn, they seem to be of little interest git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12972 85f007b7-540e-0410-9357-904b9bb8a0f7
*	- Fixed various Overfull in documentation.	herbelin	2009-01-27
\| \| \| \| \| \| \| \| \| \|	- Removed useless coq-tex preprocessing of RecTutorial. - Make "Set Printing Width" applies to "Show Script" too. - Completed documentation (specially of ltac) according to CHANGES file. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11863 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Updated dates	herbelin	2009-01-13
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11782 85f007b7-540e-0410-9357-904b9bb8a0f7
*	- Suppression de Rstar/Newman peu utilisables comme biblio (encodage	herbelin	2008-07-17
\| \| \| \| \| \| \| \| \| \|	des inductifs à l'ordre supérieur par exemple) et qui sont de toutes façons accessible en contrib dans Rocq/CoC_History. - MAJ numéro de version dans Tutorial.tex git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11232 85f007b7-540e-0410-9357-904b9bb8a0f7
*	2-3 petites modifs sur la doc	notin	2008-06-10
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11091 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Maj du lien vers coq-bugs dans Coqide.	glondu	2007-12-18
\| \| \| \| \| \| \|	On devrait mettre une redirection a l'ancienne adresse... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10390 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Mention de coqide, proof general et pcoq	herbelin	2006-06-23
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8978 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Enleve les commentaires	cpaulin	2006-04-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8715 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Mise à jour des Makefile, ajout licences, corrections mineures suite à	herbelin	2006-02-23
\| \| \| \| \| \| \|	restructuration du répertoire de documentation git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8607 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