coq - The formal proof system

Age	Commit message (Expand)	Author
2013-06-04	Start documenting new [rewrite_strat] tactic that applies rewriting	msozeau
2013-06-02	A constructive proof of Fan theorem where paths are represented by predicates.	herbelin
2013-06-02	Making the behavior of "injection ... as ..." more natural:	herbelin
2013-06-02	Fixing a typo in the documentation of discriminate.	herbelin
2013-05-29	Documenting the "appcontext" by default.	ppedrot
2013-05-12	Documenting the previous commit.	ppedrot
2013-05-06	Fix typo in manual	gareuselesinge
2013-04-17	Renaming SearchAbout into Search and Search into SearchHead.	herbelin
2013-04-04	Small doc fix : module subtyping cannot force access of opaques	letouzey
2013-04-02	Revised infrastructure for lazy loading of opaque proofs	letouzey
2013-03-25	Typo in refman (fix #2962)	letouzey
2013-03-21	Using hnf instead of "intro H" for forcing reduction to a product.	herbelin
2013-03-21	Fixing an old pecularity of "red": head betaiota redexes are now	herbelin
2013-03-11	Allowing (Co)Fixpoint to be defined local and Let-style.	ppedrot
2013-03-11	Documentation of the "Local Definition" command.	ppedrot
2013-02-21	Added missing documentation of Set Printing Existential Instances.	herbelin
2012-10-30	Documenting the 'Printing Transparent/All Dependencies' command.	ppedrot
2012-10-23	RefMan-tac: fix a few glitches concerning the documentation of eqn:	letouzey
2012-09-16	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-15	Fix failure to compile doc/stdlib/Library.tex.	gmelquio
2012-09-15	Port rewrites of tactic documentation from branch 8.4.	gmelquio
2012-09-05	Obsolete syntax in documentation of Solve Obligation commands.	ppedrot
2012-08-24	Add option Set/Unset Extraction Conservative Types.	aspiwack
2012-08-23	Remove a script unused since 2006 (cf commit r8626)	letouzey
2012-08-23	Extraction: document Separate Extraction and KeepSingleton	letouzey
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	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-07	Typo in r15654	herbelin
2012-08-07	Updating credits for final 8.4	herbelin
2012-08-03	Document the command Add/Remove Search Blacklist	letouzey
2012-07-25	documentation of bullets (forward port from v8.4).	courtieu
2012-07-20	Vector equalities first stuff	pboutill
2012-07-10	isolate instances about Permutation and PermutationA which may slow rewrite	letouzey
2012-07-09	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-05	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-06-12	make sure that documentation compilation works after adding files for	bertot
2012-05-29	place all files specific to camlp4 syntax extensions in grammar/	letouzey
2012-05-25	Fixed #2789.	ppedrot
2012-05-10	Addedum to documentation of bullets: I now use the dedicated coq_example	aspiwack