coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Doc: [revgoals].	Arnaud Spiwack	2014-09-08
*	Little fix in documentation of inversion.	Hugo Herbelin	2014-09-07
*	Cbn in refman	Pierre Boutillier	2014-09-03
*	"allows to", like "allowing to", is improper	Jason Gross	2014-08-25
*	Adding a new intro-pattern for "apply in" on the fly. Using syntax	Hugo Herbelin	2014-08-18
*	Slight simplification of naming of tactics in equality.ml (hopefully).	Hugo Herbelin	2014-08-18
*	Experimentally adding an option for automatically erasing an	Hugo Herbelin	2014-08-05
*	Adding a syntax "enough" for the variant of "assert" with the order of	Hugo Herbelin	2014-08-05
*	Typos.	Hugo Herbelin	2014-07-31
*	Document swap tactic.	Arnaud Spiwack	2014-07-25
*	Document cycle tactic.	Arnaud Spiwack	2014-07-25
*	Warns about inconsistency of generated name in evars and goals.	Arnaud Spiwack	2014-07-25
*	More on injection over a projectable "existT". - Fixing syntax "injection ......	Hugo Herbelin	2014-05-31
*	Fix for bug #3107.	Guillaume Melquiond	2014-04-04
*	fixing Function doc	Julien Forest	2014-04-04
*	Fix Bug 3131 + Really drop mentions of info in refman.	Pierre Boutillier	2014-04-02
*	Documenting the tactic-in-term construction.	Pierre-Marie Pédrot	2013-12-11
*	Silence some warning about references in documentation.	Guillaume Melquiond	2013-12-03
*	Doc: solve the bad interaction between Declare Implicit Tactic and refine.	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
*	Manual fixed w.r.t. STM	gareuselesinge	2013-08-08
*	Documenting the Remove Hints command.	ppedrot	2013-08-01
*	Revising r16550 about providing intro patterns for applying injection:	herbelin	2013-07-09
*	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 previous commit.	ppedrot	2013-05-12
*	Fix typo in manual	gareuselesinge	2013-05-06
*	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
*	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
*	Port rewrites of tactic documentation from branch 8.4.	gmelquio	2012-09-15
*	Improving rendering of ldots in doc (partially done, there are too	herbelin	2012-08-11
*	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
*	Open Local Scope ---> Local Open Scope, same with Notation and alii	letouzey	2012-07-05
*	Uniformisation in the documentation: remove the use of 'coinductive' in	aspiwack	2012-04-13
*	Document the [unify] tactic.	msozeau	2012-02-18
*	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
*	Proof using ...	gareuselesinge	2011-12-12
*	Documentation for Arguments + simpl	gareuselesinge	2011-12-06