coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Separate index for vernacular options.	Maxime Dénès	2015-02-17
*	Remove non-existing Tactic Definition command from index.	Maxime Dénès	2015-02-17
*	Documenting "induction t in ctx" when ctx contains an hyp not mentioning t.	Hugo Herbelin	2015-02-16
*	Fix documentation of generalize. (Fix for bug #4015)	Guillaume Melquiond	2015-02-10
*	Fix some documentation typo.	Guillaume Melquiond	2015-02-10
*	Fix some broken Coq scripts in the reference manual.	Guillaume Melquiond	2015-01-29
*	Reference Manual: Documenting new printing of evars and new effect of	Hugo Herbelin	2015-01-24
*	Document native_compute.	Maxime Dénès	2015-01-08
*	refman: avoid label names with whitespace (unsupported in html)	Pierre Letouzey	2014-12-09
*	Enforcing a stronger difference between the two syntaxes "simpl	Hugo Herbelin	2014-11-16
*	Fixing doc of Functional Induction.	Hugo Herbelin	2014-11-07
*	Documenting the change of semantics of the replace tactic.	Pierre-Marie Pédrot	2014-11-04
*	Addressing report #3279 (inconsistency of behavior of the -> and <-	Hugo Herbelin	2014-10-24
*	Fixing inversion after having fixed intros_replacing	Hugo Herbelin	2014-09-10
*	Removing "eqn:" for "induction" in reference manual.	Hugo Herbelin	2014-09-10
*	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