coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Add option Set/Unset Extraction Conservative Types.	aspiwack	2012-08-24
*	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
*	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
*	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
*	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
*	Removed the quasi-useless gtk2rc file and the documentation that went with it...	ppedrot	2012-04-27
*	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
*	Document the [unify] tactic.	msozeau	2012-02-18
*	Documentation for Grab Existential Variables.	aspiwack	2012-02-07
*	Corrected a careless cut-and-paste in Gallina description which dated back to...	ppedrot	2012-02-01
*	Coqtop and coqc: cleaning description of options in RefMan and manpages.	pboutill	2012-01-21
*	Added documentation for "r foo" in Ltac debugger.	herbelin	2012-01-20
*	Added documentation for "Set Parsing Explicit" + fixed mistakenly	herbelin	2012-01-20
*	Added the btauto tactic to the documentation.	ppedrot	2012-01-19
*	Reference Manual: misc fixes (spelling, index, updating pre-8.0 syntax).	herbelin	2011-12-26
*	Credits for 8.4: More exhaustive list of external contributors.	herbelin	2011-12-23
*	Credits for 8.4 + resetting COMPATIBILITY file.	herbelin	2011-12-22
*	Fixed a Not_found bug when declaring in a section some implicit	herbelin	2011-12-18
*	Command Arguments: standardizing format of error messages and American spelling.	herbelin	2011-12-17
*	Proof using ...	gareuselesinge	2011-12-12
*	Documentation of Arguments + implicits	gareuselesinge	2011-12-06
*	Documentation for Arguments + notation scopes	gareuselesinge	2011-12-06
*	Documentation for Arguments + simpl	gareuselesinge	2011-12-06
*	Fixing bugs in doc about when "with" is needed or not to give bindings	herbelin	2011-12-04
*	Documentation of appcontext	letouzey	2011-11-29
*	doc: two minor fixes to make my latex happy	letouzey	2011-11-28