coq - The formal proof system

Age	Commit message (Expand)	Author
2009-10-27	Add a new vernacular command for controling implicit generalization of	msozeau
2009-10-25	Improved the treatment of Local/Global options (noneffective Local on	herbelin
2009-10-22	Fix new instances that could easily make class resolution loop on	msozeau
2009-10-21	MSetInterface: some explicit types to avoid Raw.t-instead-of-t effect	letouzey
2009-10-20	FSetCompat: a compatibility wrapper between FSets and MSets	letouzey
2009-10-19	Merge SetoidList2 into SetoidList: forgotten reference to the removed file	letouzey
2009-10-19	Merge SetoidList2 into SetoidList.	letouzey
2009-10-16	OrderedType2 : trivial lemmas are turned into tests for order.	letouzey
2009-10-16	Structure/OrderTac.v : highlight the "order" tactic by isolating it from FSet...	letouzey
2009-10-15	MSetInterface: (W)Raw2Sets splitted in 2 (helps a future commit by Elie)	letouzey
2009-10-15	OrderedType2.order is slightly weaker since last commit, adapt accordingly	letouzey
2009-10-15	OrderedType2.order : fix the last fix (a fail at the wrong place)	letouzey
2009-10-14	Typo in last commit	letouzey
2009-10-14	Improved tactic "order" in OrderedType	letouzey
2009-10-13	Made implicit arguments of Operators_Properties.v local	herbelin
2009-10-13	MSets: a new generation of FSets	letouzey
2009-10-09	Fix a typo(?) in previous commit	letouzey
2009-10-08	Fixed clash names in Relations (see bug report #2152) and make names	herbelin
2009-10-08	Init/Tactics.v: tactic with nicer name 'exfalso' for 'elimtype False'	letouzey
2009-10-08	Implicit argument of Logic.eq become maximally inserted	letouzey
2009-10-05	Correctly do backtracking during type class resolution even if only new	msozeau
2009-10-04	Removal of trailing spaces.	serpyc
2009-10-04	Some new lemmas on max and min and a fix for a wrongly stated lemma in r12358.	herbelin
2009-10-03	A few additions in Min.v.	herbelin
2009-09-28	Fix the stdlib doc compilation + switch all .v file to utf8	letouzey
2009-09-27	Add a few properties about Rmin/Rmax with replication in Zmin/Zmax.	herbelin
2009-09-17	Remove useless MonoList.v	glondu
2009-09-17	Delete trailing whitespaces in all .{v,ml} files	glondu
2009-09-15	Fix compilation errors due to last commit.	msozeau
2009-09-15	Stop using [obligation_tactic] from Program.Tactics as the default	msozeau
2009-09-11	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-10	Misc fixes:	msozeau
2009-09-09	Znumtheory + Zdiv enriched with stuff from ZMicromega, misc improvements	letouzey
2009-09-08	Fix the bug-ridden code used to choose leibniz or generalized	msozeau
2009-09-03	Remove unnecessary redefinitions of [Fix_sub] and [Fix_F_sub], as	msozeau
2009-08-31	Fix notation for ~x in theories/Unicode/Utf8.v	glondu
2009-08-24	New tactic to rewrite decidability lemmas when one knows which side	herbelin
2009-08-19	adds a property on map	bertot
2009-08-19	adds lemmas on interactions between existsb, forallb, and app	bertot
2009-08-11	Fixed extra space in printing notation { x & P } + minor other things	herbelin
2009-08-05	changed deprecated setoid into relation	amahboub
2009-08-04	- Add more precise error localisation when one of the application fails	herbelin
2009-08-03	Added "etransitivity".	herbelin
2009-07-24	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-22	Better comparison functions in OrderedTypeEx	letouzey
2009-07-20	Use unfold directly in unfold_equations. Fixes test-suite.	msozeau
2009-07-20	Typo in a comment	letouzey