coq - The formal proof system

Age	Commit message (Expand)	Author
2013-11-04	Fix ltac's progress tactical: requires progress in each goal.	aspiwack
2013-11-02	Doc: solve the bad interaction between Declare Implicit Tactic and refine.	aspiwack
2013-11-02	Documentation for the backtracking features.	aspiwack
2013-11-02	Adds a tactic give_up.	aspiwack
2013-11-02	A tactic shelve_unifiable.	aspiwack
2013-11-02	Adds a shelve tactic.	aspiwack
2013-11-02	Document "all:" and "Set Default Goal Selector".	aspiwack
2013-08-30	add "Print Ring" and "Print Field" vernacular commands	gareuselesinge
2013-08-23	Updating documentation of the ring/field tactics.	amahboub
2013-08-08	Manual fixed w.r.t. STM	gareuselesinge
2013-08-01	Documenting the Remove Hints command.	ppedrot
2013-08-01	Documenting the previous commit: Existing Instance with priority.	ppedrot
2013-07-09	Revising r16550 about providing intro patterns for applying injection:	herbelin
2013-06-17	Documenting a potential source of incompleteness in the ring tactic,	amahboub
2013-06-06	Fixing #3056	ppedrot
2013-06-06	Document changes and add missing documentation for Program options.	msozeau
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