aboutsummaryrefslogtreecommitdiff
path: root/doc/refman/RefMan-pre.tex
AgeCommit message (Collapse)Author
2018-03-15[Sphinx] Move credits to new infrastructureMaxime Dénès
2018-01-08Merge PR #6526: Fixing various typos in the Credits chapter.Maxime Dénès
2017-09-22Avoid generated names for html pages of the reference manual (bug #4742).Guillaume Melquiond
2017-09-01Fixing various typos in the Credits chapter.Théo Zimmermann
2017-08-31Credits for version 8.7Matthieu Sozeau
2017-04-11Update RefMan-pre to mention template polymorphism.Gaetan Gilbert
2016-11-10Update CHANGES and credits for 8.6beta1.Maxime Dénès
2016-11-08Rewording from EnricoMatthieu Sozeau
2016-11-07After Emilio's comment.Matthieu Sozeau
2016-11-07More accurate contributor list.Matthieu Sozeau
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.
2016-11-07Hugo and Maxime's 2nd pass of commentsMatthieu Sozeau
2016-11-06Hugo's commentsMatthieu Sozeau
2016-11-06Maxime's commentsMatthieu Sozeau
2016-11-06Fixes from Enrico's reviewMatthieu Sozeau
2016-11-05Credits for 8.6Matthieu Sozeau
2016-01-15Thanks Hugo, but let's remain factual.Maxime Dénès
2015-12-16Updating credits.Hugo Herbelin
2015-01-21Reference Manual/Credits: expand the paragraph on the new proof engine to ↵Arnaud Spiwack
match the overall style.
2015-01-21Reference Manual/Credits: native compute is a major contribution.Arnaud Spiwack
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.
2015-01-21Reference manual/Credits: populate the "various smaller-scale improvements" ↵Arnaud Spiwack
part.
2015-01-21Reference Manual/Credits: remove a duplicate.Arnaud Spiwack
2015-01-21Reference manual: pass over the credit section for English.Arnaud Spiwack
2015-01-15Minor fixes to the refman credits to be continued.Matthieu Sozeau
2015-01-15Expand Credits for 8.5 and doc on universesMatthieu Sozeau
2015-01-15Tentatively updating credits while remaining brief.Hugo Herbelin
2015-01-11some credits for STMEnrico Tassi
2015-01-08Start credits for 8.5.Matthieu Sozeau
2014-12-09refman: switch all source files to utf8Pierre Letouzey
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.
2014-09-03sed -i.toto -e 's/Objective Caml/\{\ocaml\}/g' doc/refman/RefMan-*.texPierre Boutillier
2012-08-07Updating credits for final 8.4herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15699 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-25Fixed #2789.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15360 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-12-23Credits for 8.4: More exhaustive list of external contributors.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14852 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-12-22Credits for 8.4 + resetting COMPATIBILITY file.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14846 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-08Updating reference manual credits: gb is now nsatz.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13271 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-05-09Update of credits filesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13004 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
- 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
2008-10-27- Fixed many "Theorem with" bugs.herbelin
- 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
2008-06-09- Documentation de admit et Print Assumptions.herbelin
- 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
2008-05-28Notation concise pour la valeur par défaut des cas reconnus commeherbelin
impossibles dans un filtrage dépendant. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11014 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-05-19MAJ créditsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10948 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-04-12Cleaned doc/common/title.tex file. Increased the space under headersemakarov
in the reference manual. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9758 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-04-10Eliminated warning messages from Hevea. Most warning messages wereemakarov
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
2006-10-26MAJ crédits, fresh; documentation apply inherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9283 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-08-28MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9090 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-07-07Documentation Declare Implicit Tactic, Print Canonical Projections, ... + ↵herbelin
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
2006-06-22updated documentation for my tactics (P. orbineaucorbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8970 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-09Nouvelle MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8941 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-13MAJ 8.1-APPherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8707 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-13MAJ 8.1-APPherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8706 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-24Modification des propriétés des fichiers .tex (svn:executable)notin,no-port-forwarding,no-agent-forwarding,no-X11-forwarding,no-pty
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8609 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 19:07:02 +0000