coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Update RefMan-pre to mention template polymorphism.	Gaetan Gilbert	2017-04-11
\|
*	Update CHANGES and credits for 8.6beta1.	Maxime Dénès	2016-11-10
\|
*	Rewording from Enrico	Matthieu Sozeau	2016-11-08
\|
*	After Emilio's comment.	Matthieu Sozeau	2016-11-07
\|
*	More accurate contributor list.	Matthieu Sozeau	2016-11-07
\| \| \| \| \| \|	Command used: git log v8.5..HEAD --pretty=format:"%an," \| sort -k 2 \| uniq with some manual postprocessing for login names, particles and multiple first names.
*	Hugo and Maxime's 2nd pass of comments	Matthieu Sozeau	2016-11-07
\|
*	Hugo's comments	Matthieu Sozeau	2016-11-06
\|
*	Maxime's comments	Matthieu Sozeau	2016-11-06
\|
*	Fixes from Enrico's review	Matthieu Sozeau	2016-11-06
\|
*	Credits for 8.6	Matthieu Sozeau	2016-11-05
\|
*	Thanks Hugo, but let's remain factual.	Maxime Dénès	2016-01-15
\|
*	Updating credits.	Hugo Herbelin	2015-12-16
\|
*	Reference Manual/Credits: expand the paragraph on the new proof engine to ↵	Arnaud Spiwack	2015-01-21
\| \| \| \|	match the overall style.
*	Reference Manual/Credits: native compute is a major contribution.	Arnaud Spiwack	2015-01-21
\| \| \|	It is, at the very least, listed as such in the overview. So, I moved it to the relevant part and expanded the description with a sentence or two.
*	Reference manual/Credits: populate the "various smaller-scale improvements" ↵	Arnaud Spiwack	2015-01-21
\| \| \| \|	part.
*	Reference Manual/Credits: remove a duplicate.	Arnaud Spiwack	2015-01-21
\|
*	Reference manual: pass over the credit section for English.	Arnaud Spiwack	2015-01-21
\|
*	Minor fixes to the refman credits to be continued.	Matthieu Sozeau	2015-01-15
\|
*	Expand Credits for 8.5 and doc on universes	Matthieu Sozeau	2015-01-15
\|
*	Tentatively updating credits while remaining brief.	Hugo Herbelin	2015-01-15
\|
*	some credits for STM	Enrico Tassi	2015-01-11
\|
*	Start credits for 8.5.	Matthieu Sozeau	2015-01-08
\|
*	refman: switch all source files to utf8	Pierre Letouzey	2014-12-09
\| \| \| \| \| \|	Putting utf8 everywhere helps the maintainance of the online refman. And anyway, this is the way to go. We should also chase and migrate the few remaining iso-latin-1 files elsewhere in the sources.
*	sed -i.toto -e 's/Objective Caml/\{\ocaml\}/g' doc/refman/RefMan-*.tex	Pierre Boutillier	2014-09-03
\|
*	Updating credits for final 8.4	herbelin	2012-08-07
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15699 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fixed #2789.	ppedrot	2012-05-25
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15360 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Credits for 8.4: More exhaustive list of external contributors.	herbelin	2011-12-23
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14852 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Credits for 8.4 + resetting COMPATIBILITY file.	herbelin	2011-12-22
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14846 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Updating reference manual credits: gb is now nsatz.	herbelin	2010-07-08
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13271 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Update of credits files	herbelin	2010-05-09
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13004 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 many "Theorem with" bugs.	herbelin	2008-10-27
\| \| \| \| \| \| \| \| \| \| \|	- Fixed doc of assert as. - Doc of apply in + update credits. - Nettoyage partiel de Even.v en utilisant "Theorem with". - Added check that name is not in use for "generalize as". git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11511 85f007b7-540e-0410-9357-904b9bb8a0f7
*	- Documentation de admit et Print Assumptions.	herbelin	2008-06-09
\| \| \| \| \| \| \| \| \| \| \| \|	- Relecture, mise à jour, correction d'erreurs et petite réorganisation du chapitre sur les commandes vernaculaires. - Correction bug #1865 (rafraichissement des univers algébriques). - Suppression de la dépendance du initial.coq en les noms longs des fichiers de façons à ce que les dépendances ne soient que purement logique. - Encore un (petit) bug undo ide. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11077 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Notation concise pour la valeur par défaut des cas reconnus comme	herbelin	2008-05-28
\| \| \| \| \| \| \| \|	impossibles dans un filtrage dépendant. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11014 85f007b7-540e-0410-9357-904b9bb8a0f7
*	MAJ crédits	herbelin	2008-05-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10948 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Cleaned doc/common/title.tex file. Increased the space under headers	emakarov	2007-04-12
\| \| \| \| \| \| \|	in the reference manual. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9758 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Eliminated warning messages from Hevea. Most warning messages were	emakarov	2007-04-10
\| \| \| \| \| \| \| \| \| \| \| \| \| \|	from commands about headers; where appropriate, surrounded those by %BEGIN LATEX ... %END LATEX. Removed some \newcommands that were ignored. Removed redefinitions of \land, \lor, \lnot: there are nicely handled by Hevea. Split headers.tex file into headers.sty (for LaTeX) and headers.hva (for Hevea). This allowed removing comments like %BEGIN LATEX and %HEVEA and also commands \makeatletter, \makeatother. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9752 85f007b7-540e-0410-9357-904b9bb8a0f7
*	MAJ crédits, fresh; documentation apply in	herbelin	2006-10-26
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9283 85f007b7-540e-0410-9357-904b9bb8a0f7
*	MAJ	herbelin	2006-08-28
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9090 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Documentation Declare Implicit Tactic, Print Canonical Projections, ... + ↵	herbelin	2006-07-07
\| \| \| \| \| \|	légère restructuration autour de Proof with et Hint Rewrite + maj crédits git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9030 85f007b7-540e-0410-9357-904b9bb8a0f7
*	updated documentation for my tactics (P. orbineau	corbinea	2006-06-22
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8970 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Nouvelle MAJ	herbelin	2006-06-09
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8941 85f007b7-540e-0410-9357-904b9bb8a0f7
*	MAJ 8.1-APP	herbelin	2006-04-13
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8707 85f007b7-540e-0410-9357-904b9bb8a0f7
*	MAJ 8.1-APP	herbelin	2006-04-13
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8706 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Modification des propriétés des fichiers .tex (svn:executable)	notin,no-port-forwarding,no-agent-forwarding,no-X11-forwarding,no-pty	2006-02-24
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8609 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