coq - The formal proof system

Age	Commit message (Expand)	Author
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
2010-06-07	Backporting part of r12970 to trunk (deprecation of double induction).	herbelin
2010-04-29	Remove the svn-specific $Id$ annotations	letouzey
2010-04-27	small detail about Scheme Equality	vsiles
2010-02-26	Correction du bug #2214 + maj liens web	notin
2010-01-30	Update CHANGES, add documentation for new commands/tactics and do a bit	msozeau
2009-11-08	Restructuration of command.ml + generic infrastructure for inductive schemes	herbelin
2009-11-03	Report de la révision #12208 de la v8.2 (correction du bug #2126)	notin
2009-10-08	Init/Tactics.v: tactic with nicer name 'exfalso' for 'elimtype False'	letouzey
2009-09-13	- Inductive types in the "using" option of auto/eauto/firstorder are	herbelin
2009-09-10	Added syntax "exists bindings, ..., bindings" for iterated "exists".	herbelin
2009-06-22	Report de la révision #12200 (bug #2125)	notin
2009-06-06	Applying Ian Lynagh's documentation fixes patch (see bug #2112)	herbelin
2009-05-09	- Adding "Hint Resolve ->" and "Hint Resolve <-" for declaration of equivalence	herbelin
2009-03-20	Directory 'contrib' renamed into 'plugins', to end confusion with archive of ...	letouzey
2009-01-13	- Standardized prefix use of "Local"/"Global" modifiers as decided in	herbelin
2009-01-03	Fixed two problems:	herbelin
2008-12-29	- Added support for subterm matching in SearchAbout.	herbelin
2008-12-09	About "apply in":	herbelin
2008-10-27	- Fixed many "Theorem with" bugs.	herbelin