coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	RefMan, ch. 4: Reference Manual: more on the "in pattern" clause and	Hugo Herbelin	2015-12-10
\| \| \| \|	"@qualid pattern".
*	Preprend Fail to all the expected failures in the documentation.	Guillaume Melquiond	2015-03-05
\| \| \| \| \| \| \|	This commit also removes comments from Coq examples, as they cause extraneous delayed prompts that clutter the output because coq_tex cannot remove them. Some documentation errors were also fixed in the process, since they are easier to spot now that only unexpected failures stand out.
*	Remove some "Warning:" from the reference manual.	Guillaume Melquiond	2015-01-29
\|
*	Fix some documentation typos.	Guillaume Melquiond	2015-01-08
\|
*	"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).
*	Improving rendering of ldots in doc (partially done, there are too	herbelin	2012-08-11
\| \| \| \| \| \|	much of them). Improving doc of conversion clauses. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15733 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Uniformisation in the documentation: remove the use of 'coinductive' in	aspiwack	2012-04-13
\| \| \| \| \| \|	favour of 'co-inductive'. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15162 85f007b7-540e-0410-9357-904b9bb8a0f7
*	RefMan update about match syntax.	pboutill	2012-02-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15002 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Typo in doc	glondu	2008-07-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11292 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Standardisation du format des références croisées vers Figure, Section, ↵	herbelin	2008-01-05
\| \| \| \| \| \| \| \| \| \| \|	Chapter Remplacement pageref par ref parce que pageref n'a pas de sens pour la version HTML git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10421 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
*	Relecture/nettoyage chapitre Gallina; déplacement section Function	herbelin	2007-02-07
\| \| \| \| \| \| \| \| \|	dans extensions de Gallina. Divers. (report revisions 9614 et 9594 de la branche 8.1 vers le trunk) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9615 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Documentation or-pattern	herbelin	2006-07-04
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9005 85f007b7-540e-0410-9357-904b9bb8a0f7
*	nouveaux parametres	cpaulin	2006-06-05
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8896 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