coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Documenting the grammar {\| ... \|} syntax for building records.	Hugo Herbelin	2017-03-23
*	Fix broken documentation in presence of \zeroone{... \tt ...}.	Guillaume Melquiond	2016-12-06
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-04-24
\|\
\| *	FIX: HTML version of Chapter 4 of the Reference Manual	Matej Kosik	2016-04-12
* \|	Updating and improving the documentation of intros patterns.	Hugo Herbelin	2016-01-14
\|/
*	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-12-10
*	Remove some outdated files and fix permissions.	Guillaume Melquiond	2015-07-31
*	Added more informative messages about bullets.	Pierre Courtieu	2015-01-05
*	Making references to Proof General and CoqIDE uniform in Reference Manual.	Hugo Herbelin	2014-08-05
*	Beautify tactic documentation a bit more.	gmelquio	2012-09-16
*	Remove superfluous spaces and commas in tactic documentation.	gmelquio	2012-09-16
*	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-11
*	Documenting eta-conversion.	herbelin	2012-08-08
*	More standard layout for \lambda in chapter CIC.	herbelin	2012-08-08
*	Documentation of records defined with the keywords Inductive and	aspiwack	2012-04-13
*	Added documentation: "Theorem id x1..xn : T" and "Set Automatic Introduction".	herbelin	2010-06-08
*	Remove the svn-specific $Id$ annotations	letouzey	2010-04-29
*	Backporting from v8.2 to trunk:	herbelin	2009-01-18
*	- Fixed bug #2021 (uncaught exception with injection/discriminate when	herbelin	2009-01-01
*	- Added support for subterm matching in SearchAbout.	herbelin	2008-12-29
*	Backporting 11445 from 8.2 to trunk (negative conditions in	herbelin	2008-10-11
*	A pass on documentation:	msozeau	2008-09-14
*	Évolutions diverses et variées.	herbelin	2008-08-04
*	- Officialisation de la notation "pattern c at -1" (cf wish 1798 sur coq-bugs)	herbelin	2008-06-10
*	- Extension de "generalize" en "generalize c as id at occs".	herbelin	2008-06-08
*	Nouvelle doc pour les modules.	soubiran	2008-05-23
*	Correction bug 1838 + doc modules.	soubiran	2008-04-21
*	- Un peu de doc, préparation du CHANGES pour la release.	herbelin	2008-04-15
*	- Documentation des nouvelles options d'implicites (Set Strongly Strict	herbelin	2008-02-06
*	Some changes to eliminate Hevea warnings.	emakarov	2007-04-10
*	Relecture/nettoyage chapitre Gallina; déplacement section Function	herbelin	2007-02-07
*	Documentation de lazymatch et des extensions de idtac et fail	herbelin	2006-07-11
*	Ajout taclevel	herbelin	2006-07-05
*	Documentation or-pattern	herbelin	2006-07-04
*	Nettoyage de l'archive doc et restructuration avant intégration à l'archive	herbelin	2006-02-23