coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Documenting how to support some special unicode characters in coqdoc	Hugo Herbelin	2015-09-26
\| \| \| \|	(thanks to coq-club, Sep 2015).
*	Clarifying the doc of coqdoc --utf8 as discussed on coq-club on August 19, 2015.	Hugo Herbelin	2015-09-26
\|
*	Fix various typos in documentation	Matěj Grabovský	2015-03-31
\| \| \| \|	Closes #57.
*	Fix index of reference manual.	Guillaume Melquiond	2015-01-29
\|
*	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.
*	refman: fix broken urls	Pierre Letouzey	2014-12-09
\|
*	refman/coqdoc.tex: fix two erroneous \url	Pierre Letouzey	2014-12-09
\|
*	Reference Manual: misc fixes (spelling, index, updating pre-8.0 syntax).	herbelin	2011-12-26
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14864 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Documenting the use of ##, %%, $$ in coqdoc.	herbelin	2010-04-09
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12909 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Applied Cédric Auger's patch to fix use of "#&xxx;" in html printing	herbelin	2010-04-09
\| \| \| \| \| \| \| \| \| \| \| \|	rules (bug report #2293). Restored the sequential extension of the printing rules tables (that commit #12905 replaced by a per-file modification of the printing rules table). Note however that the table grows in the order of compilation of files by coqdoc, which does not necessarily coincide with the order of coqc compilation dependencies of the files. Added documentation of coqdoc option "--external". git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12908 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Update coqdoc documentation, CHANGES and add a fix for the proofbox (patch	msozeau	2009-09-08
\| \| \| \| \| \| \|	by Chris Casinghino). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12311 85f007b7-540e-0410-9357-904b9bb8a0f7
*	- MAJ entêtes des fichiers produits par coq_makefile	herbelin	2007-05-16
\| \| \| \| \| \| \| \|	- Correction de bugs dans la reconnaissance d'un "*)" potentiel dans les lignes correspondant au mécanisme "section" de coqdoc git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9826 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Changed many refman/*.tex files. Put \label and \index commands that ↵	emakarov	2007-04-17
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	immediately follow sectioning commands insides those sectioning commands. If \label{...} is placed after \section{...}, then, when clicking on the link in the HTML file produced by Hevea, we are moved to the correct section, but the section header is just above the screen. Hevea manual recommends writing \section{...\label{...}} and similarly for index. On the other hand, writing commands inside the argument of sectioning commands is potentially dangerous because these arguments are reproduced not only to produce the section header but also to produce headers and/or table of contents entries. Thus, \index{...} and \labels{...} may be executed several times. Indeed, if we put a \typeout{...} instruction inside the argument to a sectioning command then it will be executed, besides the section itself, in the table of contents and once for every appearance of the header. However, it seems that the \label command are not executed several times unless they are prefixed with \protect, and \index command is not executed multiple times even then. So maybe it's OK to put \label and \index inside sectioning commands. When hyperref package is used, the \newlabel command left in .aux file has an extra group {...} which includes another \label command! This may lead to trouble when we use \nameref (?). However, the most reliable way would be to use the optional argument of sectioning commands. Then the text only goes to the optional argument and the text plus \label plus \index goes to the main argument. The optional argument is used for headers and table of contents. This works fine with Hevea as well. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9781 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
*	Ajout de la doc de l'option -stdout de coqdoc	notin	2006-04-27
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8749 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