coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Remove useless MonoList.v	glondu	2009-09-17
*	Delete trailing whitespaces in all .{v,ml} files	glondu	2009-09-17
*	Fix compilation errors due to last commit.	msozeau	2009-09-15
*	Stop using [obligation_tactic] from Program.Tactics as the default	msozeau	2009-09-15
*	Added the following lemmas to homogenize Reals a bit:	gmelquio	2009-09-11
*	- Resolve type class constraints before trying to find unresolved	msozeau	2009-09-11
*	Misc fixes:	msozeau	2009-09-10
*	Znumtheory + Zdiv enriched with stuff from ZMicromega, misc improvements	letouzey	2009-09-09
*	Fix the bug-ridden code used to choose leibniz or generalized	msozeau	2009-09-08
*	Remove unnecessary redefinitions of [Fix_sub] and [Fix_F_sub], as	msozeau	2009-09-03
*	Fix notation for ~x in theories/Unicode/Utf8.v	glondu	2009-08-31
*	New tactic to rewrite decidability lemmas when one knows which side	herbelin	2009-08-24
*	adds a property on map	bertot	2009-08-19
*	adds lemmas on interactions between existsb, forallb, and app	bertot	2009-08-19
*	Fixed extra space in printing notation { x & P } + minor other things	herbelin	2009-08-11
*	changed deprecated setoid into relation	amahboub	2009-08-05
*	- Add more precise error localisation when one of the application fails	herbelin	2009-08-04
*	Added "etransitivity".	herbelin	2009-08-03
*	OrderedTypeEx.N_as_OT use Nlt, various minor improvements in N/ZArith	letouzey	2009-07-24
*	List: add a iff-based lemma about In and ++	letouzey	2009-07-24
*	Remove the barely-used/obsolete/undocumented syntax "conditional <tac> rewrite"	letouzey	2009-07-24
*	Better comparison functions in OrderedTypeEx	letouzey	2009-07-22
*	Use unfold directly in unfold_equations. Fixes test-suite.	msozeau	2009-07-20
*	Typo in a comment	letouzey	2009-07-20
*	Simplify eauto and fix it for compatibility, allowing full delta during	msozeau	2009-07-14
*	Use the proper unification flags in e_exact. This makes exact fail a bit	msozeau	2009-07-09
*	Miscellaneous practical commits:	herbelin	2009-06-29
*	made several occurrences of (eapply ...; eauto) not rely on the lack of patte...	barras	2009-06-22
*	Do a fixpoint on the result of typeclass search to force the	msozeau	2009-06-08
*	- Added two new introduction patterns with the following temptative syntaxes:	herbelin	2009-06-07
*	Very-small-step policy changes to the library.	herbelin	2009-06-06
*	Use Type instead of Set.	msozeau	2009-06-02
*	Stop using a "Manual Implicit Arguments" flag and support them as soon	msozeau	2009-05-27
*	Many fixes in unification:	msozeau	2009-05-20
*	Minor fixes in typeclasses:	msozeau	2009-05-16
*	adds a theorem to reason at the level of Z	bertot	2009-05-07
*	Improvements in typeclasses eauto and generalized rewriting:	msozeau	2009-05-05
*	Fixes for bugs in r12110:	msozeau	2009-04-28
*	Backporting 12112 from v8.2 branch to trunk (fixing documentation bugs	herbelin	2009-04-28
*	- Implementation of a new typeclasses eauto procedure based on success	msozeau	2009-04-27
*	Backporting 12080 (fixing bug #2091 on bad rollback in the "where"	herbelin	2009-04-24
*	Rename [Morphism] into [Proper] and [respect] into [proper] to comply	msozeau	2009-04-21
*	Fix wrong pattern in Morphisms. Fix bug scripts to reflect the fact that	msozeau	2009-04-20
*	Just export RelationClasses for [Equivalence] through Setoid.	msozeau	2009-04-18
*	Only export the notations of Morphism as well as Equivalence through	msozeau	2009-04-17
*	Better Requires in Classes. Fix bug #2093: the code does not require	msozeau	2009-04-16
*	Rewrite autorewrite to use a dnet indexed by the left-hand sides (or	msozeau	2009-04-14
*	Some additions in Max and Zmax. Unifiying list of statements and names	herbelin	2009-04-14
*	Rewrite of setoid_rewrite to modularize it based on proof-producing	msozeau	2009-04-13
*	Fix premature optimisation in dependent induction: even variable args need	msozeau	2009-04-10