coq - The formal proof system

Age	Commit message (Collapse)	Author
2018-03-29	[Sphinx] Move chapter 18 to new infrastructure	Maxime Dénès

2018-03-16	[Sphinx] Add chapter 11	Maxime Dénès
	Thanks to Enrico Tassi, Assia Mahboubi, Laurence Rideau and Yves Bertot for porting this chapter.
2018-03-09	doc and changes for coercion from prop/type	charguer

2017-09-22	Avoid generated names for html pages of the reference manual (bug #4742).	Guillaume Melquiond

2015-11-07	Fixing documention of Add Printing Coercion.	Hugo Herbelin

2015-02-17	Separate index for vernacular options.	Maxime Dénès

2014-12-09	refman: switch all source files to utf8	Pierre 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.
2012-08-11	Improving rendering of ldots in doc (partially done, there are too	herbelin
	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
2010-07-25	Documentation of Set Automatic Coercions Import.	herbelin
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13327 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-26	Applying François' patches about Canonical Projections (see #2302 and #2334).	herbelin
	Printer pr_cs_pattern is kept in recordops only. Also updated CHANGES. Fixed spelling of "uniform inheritance condition" in doc too (see git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13204 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-08	Added documentation: "Theorem id x1..xn : T" and "Set Automatic Introduction".	herbelin
	Updated documentation in many ways: - merged binder and binderlet as done for a while in implementation - fixed a few technical problems (bad indexation of {x:A\|P x}, missing spaces in html code in many situations due to missing curly brackets around TeX macros - e.g. around \ldots -, missing dots at end of sentences, ...) - renamed "statement" commands into "assertion" commands and "declaration" commands into "assumption" commands - moved Goal and Save out of the Gallina chapter - avoid some recovering in the Gallina and proof mode chapters - slight smoothing of some hard-to-read paragraphs of the manual git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13091 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-01-13	- Standardized prefix use of "Local"/"Global" modifiers as decided in	herbelin
	late 2008 Coq WG. - Updated Copyright file wrt JProver. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11781 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-01-05	Standardisation du format des références croisées vers Figure, Section, ↵	herbelin
	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
2006-02-23	Nettoyage de l'archive doc et restructuration avant intégration à l'archive	herbelin
	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