coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	refman: document vi2vo	Enrico Tassi	2014-02-26
*	fixup complement Fin	Pierre Boutillier	2014-02-24
*	Removing the [Require "file"] syntax.	Pierre-Marie Pédrot	2014-02-02
*	-schedule-vi-checking ported to spawn	Enrico Tassi	2014-01-26
*	Fixing typo in reference manual from previous commit	Hugo Herbelin	2014-01-13
*	Documenting old but useful command "Print Tables".	Hugo Herbelin	2014-01-13
*	refman: fist stab at Asynchronous Proofs	Enrico Tassi	2014-01-05
*	Reference the 'external' tactic.	Guillaume Melquiond	2014-01-01
*	micromega: removal of spurious Export; addition of Lia.v encapsulating lia an...	Frédéric Besson	2013-12-20
*	Documenting the tactic-in-term construction.	Pierre-Marie Pédrot	2013-12-11
*	Missing file in commit 1fb883.	Arnaud Spiwack	2013-12-06
*	Documentation of the Derive plugin.	Arnaud Spiwack	2013-12-04
*	Silence some warning about references in documentation.	Guillaume Melquiond	2013-12-03
*	First stab at documenting Canonical Structures	Enrico Tassi	2013-11-29
*	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