coq - The formal proof system

Age	Commit message (Expand)	Author
2013-12-11	Documenting the tactic-in-term construction.	Pierre-Marie Pédrot
2013-12-03	Silence some warning about references in documentation.	Guillaume Melquiond
2013-11-02	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-08-30	add "Print Ring" and "Print Field" vernacular commands	gareuselesinge
2013-08-08	Manual fixed w.r.t. STM	gareuselesinge
2013-08-01	Documenting the Remove Hints command.	ppedrot
2013-07-09	Revising r16550 about providing intro patterns for applying injection:	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-12	Documenting the previous commit.	ppedrot
2013-05-06	Fix typo in manual	gareuselesinge
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
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	Port rewrites of tactic documentation from branch 8.4.	gmelquio
2012-08-11	Improving rendering of ldots in doc (partially done, there are too	herbelin
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	Open Local Scope ---> Local Open Scope, same with Notation and alii	letouzey
2012-04-13	Uniformisation in the documentation: remove the use of 'coinductive' in	aspiwack
2012-02-18	Document the [unify] tactic.	msozeau
2012-01-19	Added the btauto tactic to the documentation.	ppedrot
2011-12-26	Reference Manual: misc fixes (spelling, index, updating pre-8.0 syntax).	herbelin
2011-12-12	Proof using ...	gareuselesinge
2011-12-06	Documentation for Arguments + simpl	gareuselesinge
2011-12-04	Fixing bugs in doc about when "with" is needed or not to give bindings	herbelin
2011-10-07	A new tactic is_var to check whether a term is a goal/section variable	letouzey
2011-09-26	Added support for referring to subterms of the goal by pattern.	herbelin
2011-09-23	auto with nocore : disable the use of the core database (wish #2188)	letouzey
2011-09-02	Bug 2589: Documentation patch of Hendrik Tews	pboutill
2011-09-01	Several bug reports came from confusions between generalize and set.	pboutill
2010-12-24	Precision in documentation of "decide equality"	glondu
2010-12-23	Remove the two-argument variant of "decide equality"	glondu
2010-12-23	More precise documentation for instantiate	glondu
2010-12-02	Documentation for tactic constr_eq	glondu
2010-12-02	Add tactic has_evar (#2433)	glondu
2010-12-02	Add tactic is_evar (Closes: #2433)	glondu
2010-11-03	Fix typo in "Hint Extern" doc	glondu
2010-07-27	Minor fixes:	msozeau
2010-06-18	Documentation of clear dependent and revert dependent	letouzey
2010-06-08	Added documentation: "Theorem id x1..xn : T" and "Set Automatic Introduction".	herbelin