coq - The formal proof system

Age	Commit message (Expand)	Author
2019-03-14	Documentation for SProp	Gaëtan Gilbert
2019-01-29	Use \mathcal instead of \cal	Gaëtan Gilbert
2018-02-20	Extended documentation for notations referring to binders.	Hugo Herbelin
2017-11-25	Updating the current official writing of OCaml, updating Camlp4->Camlp5.	Hugo Herbelin
2017-03-23	Documenting the grammar {\| ... \|} syntax for building records.	Hugo Herbelin
2016-12-06	Fix broken documentation in presence of \zeroone{... \tt ...}.	Guillaume Melquiond
2016-04-24	Merge branch 'v8.5'	Pierre-Marie Pédrot
2016-04-12	FIX: HTML version of Chapter 4 of the Reference Manual	Matej Kosik
2016-01-14	Updating and improving the documentation of intros patterns.	Hugo Herbelin
2015-12-10	ENH: examples for 'strict positivity' were expanded	Matej Kosik
2015-12-10	CLEANUP: s/List_A/List~A/g	Matej Kosik
2015-12-10	CLEANUP: superfluous examples were removed	Matej Kosik
2015-12-10	ENH: new example: "even"	Matej Kosik
2015-12-10	ALPHA-CONVERSION: s/Length/has_length/g	Matej Kosik
2015-12-10	ENH: The beginning of Section 4.5 (Inductive declarations) was changed in ord...	Matej Kosik
2015-12-10	RefMan, ch. 4: Removing the local context of inductive definitions.	Hugo Herbelin
2015-12-10	RefMan, ch. 4: Adding discharging of inductive types.	Hugo Herbelin
2015-12-10	RefMan, ch. 4: In chapter 4 about CIC, renounced to keep a local	Hugo Herbelin
2015-12-10	RefMan, ch. 4: Reformulating introduction of the chapter on CIC, being	Hugo Herbelin
2015-07-31	Remove some outdated files and fix permissions.	Guillaume Melquiond
2015-01-05	Added more informative messages about bullets.	Pierre Courtieu
2014-08-05	Making references to Proof General and CoqIDE uniform in Reference Manual.	Hugo Herbelin
2012-09-16	Beautify tactic documentation a bit more.	gmelquio
2012-09-16	Remove superfluous spaces and commas in tactic documentation.	gmelquio
2012-08-11	Improving rendering of ldots in doc (partially done, there are too	herbelin
2012-08-11	Added support for option Local (at module level) in Tactic Notation.	herbelin
2012-08-11	Improving rendering of ...-separated lists and sequences in reference	herbelin
2012-08-08	Documenting eta-conversion.	herbelin
2012-08-08	More standard layout for \lambda in chapter CIC.	herbelin
2012-04-13	Documentation of records defined with the keywords Inductive and	aspiwack
2010-06-08	Added documentation: "Theorem id x1..xn : T" and "Set Automatic Introduction".	herbelin
2010-04-29	Remove the svn-specific $Id$ annotations	letouzey
2009-01-18	Backporting from v8.2 to trunk:	herbelin
2009-01-01	- Fixed bug #2021 (uncaught exception with injection/discriminate when	herbelin
2008-12-29	- Added support for subterm matching in SearchAbout.	herbelin
2008-10-11	Backporting 11445 from 8.2 to trunk (negative conditions in	herbelin
2008-09-14	A pass on documentation:	msozeau
2008-08-04	Évolutions diverses et variées.	herbelin
2008-06-10	- Officialisation de la notation "pattern c at -1" (cf wish 1798 sur coq-bugs)	herbelin
2008-06-08	- Extension de "generalize" en "generalize c as id at occs".	herbelin
2008-05-23	Nouvelle doc pour les modules.	soubiran
2008-04-21	Correction bug 1838 + doc modules.	soubiran
2008-04-15	- Un peu de doc, préparation du CHANGES pour la release.	herbelin
2008-02-06	- Documentation des nouvelles options d'implicites (Set Strongly Strict	herbelin
2007-04-10	Some changes to eliminate Hevea warnings.	emakarov
2007-02-07	Relecture/nettoyage chapitre Gallina; déplacement section Function	herbelin
2006-07-11	Documentation de lazymatch et des extensions de idtac et fail	herbelin
2006-07-05	Ajout taclevel	herbelin
2006-07-04	Documentation or-pattern	herbelin
2006-02-23	Nettoyage de l'archive doc et restructuration avant intégration à l'archive	herbelin