coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Fix ltac's progress tactical: requires progress in each goal.	aspiwack	2013-11-04
*	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-11-02
*	add "Print Ring" and "Print Field" vernacular commands	gareuselesinge	2013-08-30
*	Updating documentation of the ring/field tactics.	amahboub	2013-08-23
*	Manual fixed w.r.t. STM	gareuselesinge	2013-08-08
*	Documenting the Remove Hints command.	ppedrot	2013-08-01
*	Documenting the previous commit: Existing Instance with priority.	ppedrot	2013-08-01
*	Revising r16550 about providing intro patterns for applying injection:	herbelin	2013-07-09
*	Documenting a potential source of incompleteness in the ring tactic,	amahboub	2013-06-17
*	Fixing #3056	ppedrot	2013-06-06
*	Document changes and add missing documentation for Program options.	msozeau	2013-06-06
*	Start documenting new [rewrite_strat] tactic that applies rewriting	msozeau	2013-06-04
*	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-06-02
*	Documenting the "appcontext" by default.	ppedrot	2013-05-29
*	Documenting the previous commit.	ppedrot	2013-05-12
*	Fix typo in manual	gareuselesinge	2013-05-06
*	Renaming SearchAbout into Search and Search into SearchHead.	herbelin	2013-04-17
*	Small doc fix : module subtyping cannot force access of opaques	letouzey	2013-04-04
*	Revised infrastructure for lazy loading of opaque proofs	letouzey	2013-04-02
*	Typo in refman (fix #2962)	letouzey	2013-03-25
*	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-21
*	Allowing (Co)Fixpoint to be defined local and Let-style.	ppedrot	2013-03-11
*	Documentation of the "Local Definition" command.	ppedrot	2013-03-11
*	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