coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Ajout possibilité d'options à trois mots.	herbelin	2007-04-29
\| \| \| \| \| \| \| \| \| \|	Suppression au passage syntaxe "Set table field ref", synonyme de "Add table field ref" et de "Unset table field ref", synonyme de "Remove table field ref". Changement de la syntaxe "Test tabel field val" en ""Test tabel field for val". git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9810 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Documentation de Existential et de Show Existential (fixes bug #1294)	notin	2007-04-26
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9799 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fixed some typos.	glondu	2007-04-18
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9789 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Corrected a LaTeX typo.	emakarov	2007-04-17
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9784 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
*	Removed from headers.hva the code to make index point to the section	emakarov	2007-04-16
\| \| \| \| \| \| \| \| \|	labels and not other environment labels (such as enumerate or theorem). This facility was added to Hevea, which is available at http://hevea.inria.fr/distri/unstable/hevea-2007-04-16.tar.gz git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9772 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
*	Standardisation format biblio	herbelin	2007-04-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9757 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Some changes to eliminate Hevea warnings.	emakarov	2007-04-10
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9754 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Split refman/headers.tex into headers.sty and headers.hva.	emakarov	2007-04-10
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9753 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
*	Mise en place d'un rafinement de compute.	jforest	2007-04-05
\| \| \| \| \| \| \| \| \| \|	On peut desormais utiliser: compute delta [f g ...] pour cbv beta iota zera delta [f g ...] et compute delta - [f g ...] pour cbv beta iota zera delta - [f g ...] git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9749 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Corrected a typo in doc/refman/Setoid.tex.	emakarov	2007-04-04
\| \| \| \| \| \| \| \| \| \| \|	Redefined the \index command in doc/refman/headers.tex only for Hevea. Now all sectioning commands (from \part to \subparagraph) store the value of their counter in the command \@indexlabel. It is this command that is used inside the new \index. Thus, the index shows only the the most recent sectioning command, but not \index, \theorem, etc. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9745 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correction du bug #1441	notin	2007-03-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9712 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correction bug #1439 (comportement de replace by)	notin	2007-03-13
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9699 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Application suggestion #1430 de Yevgeniy pour TEXINPUTS	herbelin	2007-03-07
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9687 85f007b7-540e-0410-9357-904b9bb8a0f7
*	doc: typo/english: "is left associating" -> "is left-associative".	lmamane	2007-02-22
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9671 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Documentation of tactical "t1 \|\| t2": t2 is executed if t1 fails to	lmamane	2007-02-22
\| \| \| \| \| \| \|	progress, not only if it fails (i.e. gives an error). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9670 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Compilation de la FAQ	notin	2007-02-18
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9657 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Réintroduction de l'entrée "integer" dans ltac (apparemment disparue lors	herbelin	2007-02-15
\| \| \| \| \| \| \|	du passage de l'ancienne à la nouvelle syntaxe) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9650 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Réactivation du filtrage d'ordre 2 dans ltac qui avait cessé de	herbelin	2007-02-13
\| \| \| \| \| \| \| \|	fonctionner entre la V7.3 et la V8.0 (notation : "@ ?meta id1 ... idn") git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9644 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Meilleur anglais (cf 9619)	herbelin	2007-02-07
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9620 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
*	Suppression RefMan-cas.tex inutilisé	herbelin	2007-02-07
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9613 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Field rewrites only with polynomial	thery	2007-02-07
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9607 85f007b7-540e-0410-9357-904b9bb8a0f7
*	doc de ring/field + option infinite -> completeness	barras	2007-02-07
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9602 85f007b7-540e-0410-9357-904b9bb8a0f7
*	doc for field	thery	2007-02-06
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9596 85f007b7-540e-0410-9357-904b9bb8a0f7
*	complement du commit 9591	bgregoir	2007-02-05
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9592 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Report 9545 de 8.1 vers trunk	herbelin	2007-02-01
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9581 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Petite relecture partie ring	herbelin	2007-02-01
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9580 85f007b7-540e-0410-9357-904b9bb8a0f7
*	report de r9574: doc de field	barras	2007-01-31
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9575 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fix typo.	msozeau	2007-01-31
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9565 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fix order of wf and measure arguments, patch Program doc.	msozeau	2007-01-31
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9561 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Explication du intros until n	notin	2007-01-26
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9543 85f007b7-540e-0410-9357-904b9bb8a0f7
*	doc de ring	bgregoir	2007-01-24
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9532 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correction adresse CoRN dans FAQ (suite)	herbelin	2007-01-17
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9492 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correction adresse CoRN dans FAQ (cf #1317)	herbelin	2007-01-17
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9491 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Doc for Combined Scheme.	msozeau	2006-12-23
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9462 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correction typo règle réduction du fix chapitre CCI	herbelin	2006-12-08
\| \| \| \| \| \| \|	Maj mode emacs coqide dans faq git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9412 85f007b7-540e-0410-9357-904b9bb8a0f7
*	add a comment about Show Existentials and a question about case_eq	jnarboux	2006-12-01
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9408 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Typo + ajout Qcanon.v	herbelin	2006-11-11
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9366 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Add doc on obligation solving commands.	msozeau	2006-11-02
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9332 85f007b7-540e-0410-9357-904b9bb8a0f7
*	MAJ nouvelles théories	herbelin	2006-10-28
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9312 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Documentation de "Set Printing Universes", "Print Universes" (anciennement	herbelin	2006-10-28
\| \| \| \| \| \| \| \|	"Dump Universes"), "Universe inconsistency", et description brève des univers algébriques. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9306 85f007b7-540e-0410-9357-904b9bb8a0f7
*	added doc for declarative language	corbinea	2006-10-26
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9286 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
*	Mise en forme des theories	notin	2006-10-17
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9245 85f007b7-540e-0410-9357-904b9bb8a0f7
*	typo doc + bug legacy field	barras	2006-10-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9243 85f007b7-540e-0410-9357-904b9bb8a0f7
*	revision de la semantique de rewrite ... in <clause>. details dans la doc	letouzey	2006-10-05
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9211 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout String	herbelin	2006-10-04
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9207 85f007b7-540e-0410-9357-904b9bb8a0f7