coq - The formal proof system

Age	Commit message (Expand)	Author
2009-10-25	Add support for remaining side-conditions in "apply in as".	herbelin
2009-10-25	Improved the treatment of Local/Global options (noneffective Local on	herbelin
2009-10-24	Fixing XML doc (COQ_XML not working as an environment variable).	herbelin
2009-10-23	First debug... the renaming of librairies was not working and auto/dn were no...	soubiran
2009-10-22	Fix new instances that could easily make class resolution loop on	msozeau
2009-10-21	This big commit addresses two problems:	soubiran
2009-10-21	MSetInterface: some explicit types to avoid Raw.t-instead-of-t effect	letouzey
2009-10-20	Repaired bug #2165 (buggy coq example in Tactic Examples doc chapter)	herbelin
2009-10-20	Added syntactic coloration for 'Function'.	gmelquio
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-17	Fixed a notation bug when extending binder_constr with empty levels	herbelin
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-16	note for later : when the tag table is shared, never, ever create two	vgross
2009-10-15	typo in doc of Extraction Blacklist	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-15	Fix bug in typeclass resolution discoverd by Eeelis van der Weegen:	msozeau
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	Typos.	gmelquio
2009-10-13	Better handling of emphasis.	msozeau
2009-10-13	MSets: a new generation of FSets	letouzey
2009-10-09	Fix bug #2162 and a name clashing bug in generalized binders.	msozeau
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-08	Fixed a bug introduced in revision 12265.	herbelin
2009-10-07	Fix for missing hypotesae in XML proof tree export.	cek
2009-10-06	Fixed installation of Coqide interface/library files (bug #2147).	gmelquio
2009-10-06	Relaxed error severity when encountering unknown library objects or tactic	gmelquio
2009-10-05	Correctly do backtracking during type class resolution even if only new	msozeau
2009-10-05	Revert "kills the old backtracking framework and replaces it with"	vgross
2009-10-04	Changed the way to support compatibility with previous versions.	herbelin
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	Fixed small name freshness bug in Functional Scheme ("Heq" name was	herbelin
2009-10-03	A few additions in Min.v.	herbelin
2009-10-03	Added option "Unset Dependent Propositions Elimination" to protect	herbelin
2009-09-29	Add support for Local Declare ML Module	glondu
2009-09-29	Remove legacy export_* functions	glondu
2009-09-29	kills the old backtracking framework and replaces it with	vgross
2009-09-28	Fix the stdlib doc compilation + switch all .v file to utf8	letouzey
2009-09-28	Applied patches from BSD/pkgsrc maintainer, so that Coq compiles out-of-the-box.	gmelquio
2009-09-27	Apply "Declare Implicit Tactic" also to terms interpreted as "open	herbelin