coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Added missing documentation of Set Printing Existential Instances.	herbelin	2013-02-21
*	Documenting the 'Printing Transparent/All Dependencies' command.	ppedrot	2012-10-30
*	RefMan-tac: fix a few glitches concerning the documentation of eqn:	letouzey	2012-10-23
*	Move reflexivity, symmetry, and transitivity, next to f_equal, in the documen...	gmelquio	2012-09-16
*	Some more fixes to tactic documentation.	gmelquio	2012-09-16
*	Beautify tactic documentation a bit more.	gmelquio	2012-09-16
*	Remove superfluous spaces and commas in tactic documentation.	gmelquio	2012-09-16
*	Fix index generation for the pdf document.	gmelquio	2012-09-16
*	Fix failure to compile doc/stdlib/Library.tex.	gmelquio	2012-09-15
*	Port rewrites of tactic documentation from branch 8.4.	gmelquio	2012-09-15
*	Obsolete syntax in documentation of Solve Obligation commands.	ppedrot	2012-09-05
*	Add option Set/Unset Extraction Conservative Types.	aspiwack	2012-08-24
*	Remove a script unused since 2006 (cf commit r8626)	letouzey	2012-08-23
*	Extraction: document Separate Extraction and KeepSingleton	letouzey	2012-08-23
*	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
*	Updating version numbers.	herbelin	2012-08-08
*	Documenting eta-conversion.	herbelin	2012-08-08
*	More standard layout for \lambda in chapter CIC.	herbelin	2012-08-08
*	Typo in r15654	herbelin	2012-08-07
*	Updating credits for final 8.4	herbelin	2012-08-07
*	Document the command Add/Remove Search Blacklist	letouzey	2012-08-03
*	documentation of bullets (forward port from v8.4).	courtieu	2012-07-25
*	Vector equalities first stuff	pboutill	2012-07-20
*	isolate instances about Permutation and PermutationA which may slow rewrite	letouzey	2012-07-10
*	The tactic remember now accepts a final eqn:H option (grant wish #2489)	letouzey	2012-07-09
*	induction/destruct : nicer syntax for generating equations (solves #2741)	letouzey	2012-07-09
*	Legacy Ring and Legacy Field migrated to contribs	letouzey	2012-07-05
*	Open Local Scope ---> Local Open Scope, same with Notation and alii	letouzey	2012-07-05
*	ZArith + other : favor the use of modern names instead of compat notations	letouzey	2012-07-05
*	make sure that documentation compilation works after adding files for	bertot	2012-06-12
*	place all files specific to camlp4 syntax extensions in grammar/	letouzey	2012-05-29
*	Fixed #2789.	ppedrot	2012-05-25
*	Addedum to documentation of bullets: I now use the dedicated coq_example	aspiwack	2012-05-10
*	Documentation for Unfocused, braces and bullets.	aspiwack	2012-05-10
*	Rephrasing section on Sorts in CIC chapter, accordingly to discussions	herbelin	2012-05-08
*	Ref. man., ch. CIC: clarifying the redundancy coming from having both	herbelin	2012-05-08
*	Fixup r15251 second time	pboutill	2012-05-03
*	Removed the quasi-useless gtk2rc file and the documentation that went with it...	ppedrot	2012-04-27
*	MSetRBT : implementation of MSets via Red-Black trees	letouzey	2012-04-13
*	Uniformisation in the documentation: remove the use of 'coinductive' in	aspiwack	2012-04-13
*	Documentation of records defined with the keywords Inductive and	aspiwack	2012-04-13
*	Restores pdf bookmarks in the reference manual.	aspiwack	2012-04-13
*	lib directory is cut in 2 cma.	pboutill	2012-04-12
*	Slight change in the semantics of arguments scopes: scopes can no	herbelin	2012-03-26
*	Documentation of last commit concerning Backtracking	letouzey	2012-03-23
*	Remove old proof-managment commands Suspend/Resume	letouzey	2012-03-23
*	RefMan: Environment variables description update	pboutill	2012-03-19
*	RefMan update about match syntax.	pboutill	2012-02-29