coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Ensuring all .v files end with a newline to make "sed -i" work better on them.	Hugo Herbelin	2017-08-21
*	Bump year in headers.	Pierre-Marie Pédrot	2017-07-04
*	Fix bug #4923: Warning: appcontext is deprecated.	Pierre-Marie Pédrot	2016-07-18
*	Making parentheses mandatory in tactic scopes.	Pierre-Marie Pédrot	2016-03-04
*	Update copyright headers.	Maxime Dénès	2016-01-20
*	The "on_last_hyp" tactic now behaves as it should.	Cyprien Mangin	2015-06-12
*	Update headers.	Maxime Dénès	2015-01-12
*	Updating headers.	herbelin	2012-08-08
*	Kills the useless tactic annotations "in \|- *"	letouzey	2012-07-05
*	Fixed bug #2398: destruct ex2/sig2/sigT2 in Program, patch by Paolo Herms.	msozeau	2011-06-07
*	Add a flag to hide obligations in Program-generated terms under an	msozeau	2011-02-28
*	In Program obligation, do not use auto on non-proposition goals by	msozeau	2011-02-17
*	Updated all headers for 8.3 and trunk	herbelin	2010-07-24
*	Correction program_simplify. Devrait corriger certaines contribs.	aspiwack	2010-05-28
*	Remove the svn-specific $Id$ annotations	letouzey	2010-04-29
*	Here comes the commit, announced long ago, of the new tactic engine.	aspiwack	2010-04-22
*	Minor fixes.	msozeau	2010-03-05
*	Fix [Existing Class] impl and add documentation. Fix computation of the	msozeau	2010-02-10
*	Add [Next Obligation with tactic] support (wish #1953).	msozeau	2010-01-26
*	Integrate a few improvements on typeclasses and Program from the equations br...	msozeau	2009-10-28
*	Delete trailing whitespaces in all .{v,ml} files	glondu	2009-09-17
*	Stop using [obligation_tactic] from Program.Tactics as the default	msozeau	2009-09-15
*	Misc fixes:	msozeau	2009-09-10
*	Experimental support for automatic destruction of recursive calls and	msozeau	2009-04-08
*	Finish fix for the treatment of [inverse] in [setoid_rewrite], making a	msozeau	2008-12-16
*	Fix for bug #1973 provided by Brian Campbell.	msozeau	2008-10-22
*	Fix a bug reintroduced in [setoid_reflexivity] etc...	msozeau	2008-09-09
*	More debugging of [Equations], now able to discharge even the heavily	msozeau	2008-09-07
*	Initial implementation of a new command to define (dependent) functions by	msozeau	2008-09-02
*	Fixes in dependent induction tactic to keep names, allow giving	msozeau	2008-08-21
*	Fixes in generalize_eqs/dependent induction to allow the user to specify	msozeau	2008-07-28
*	Rename obligations_tactic to obligation_tactic and fix bugs #1893.	msozeau	2008-06-22
*	Temporary fix for bug #1876, printing fails because of unresolved	msozeau	2008-06-13
*	- Extension de "generalize" en "generalize c as id at occs".	herbelin	2008-06-08
*	Minor fixes. Use expanded type in class_tactics for Morphism search, to	msozeau	2008-04-02
*	Improve error handling and messages for typeclasses.	msozeau	2008-03-28
*	Interpret patterns for hypotheses types in match goal in type_scope (if not a	msozeau	2008-03-25
*	Debug implementation of dependent induction/dependent destruction and documen...	msozeau	2008-01-31
*	Work on dependent induction tactic and friends, finish the test-suite example	msozeau	2008-01-30
*	Fix bug #1778, better typeclass error messages. Move Obligations Tactic to a ...	msozeau	2008-01-18
*	Fix a naming bug reported by Arnaud Spiwack, allow instance search to create ...	msozeau	2008-01-05
*	Better resolution of implicit parameters in typeclass binders, add extensiona...	msozeau	2008-01-02
*	Merged revisions 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,...	msozeau	2007-12-31
*	Addition of more general tactics for equality. Functional extensionality and ...	msozeau	2007-10-24
*	Add more equality tactics. Upgrade program_simpl for discrimination of conjun...	msozeau	2007-08-26
*	Move Program tactics into a proper theories/ directory as they are general pu...	msozeau	2007-08-07