coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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-16
*	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-15
*	Typo in last commit	letouzey	2009-10-14
*	Improved tactic "order" in OrderedType	letouzey	2009-10-14
*	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-13
*	Fix bug #2162 and a name clashing bug in generalized binders.	msozeau	2009-10-09
*	Fix a typo(?) in previous commit	letouzey	2009-10-09
*	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-08
*	Fix for missing hypotesae in XML proof tree export.	cek	2009-10-07
*	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-06
*	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-05
*	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-04
*	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-10-03
*	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-29
*	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-28
*	Apply "Declare Implicit Tactic" also to terms interpreted as "open	herbelin	2009-09-27
*	Fixed a bug in the interaction between dEqThen and inject_at_positions	herbelin	2009-09-27
*	Fixed two tests that was incorrectly typed in former revisions 12348 and 12356.	herbelin	2009-09-27
*	Add a few properties about Rmin/Rmax with replication in Zmin/Zmax.	herbelin	2009-09-27
*	Fixed error message "cannot infer the type of id" in presence of	herbelin	2009-09-27
*	Delay the choice of eliminator in destruct/induction until we know if	herbelin	2009-09-27
*	Complement to 12347 and 12348 on the extended syntax of case/elim.	herbelin	2009-09-27
*	Fixed a hole in glob_tactic that allowed some Ltac code to refer to	herbelin	2009-09-26
*	Micromega doc : psatz Z -> psatz Z 2	fbesson	2009-09-24
*	Ltac doc: only variables are accepted as message_token	glondu	2009-09-23
*	Add the option to automatically introduce variables declared before the	msozeau	2009-09-22
*	Better use of transparency information for local hypotheses:	msozeau	2009-09-22
*	Update link to "Recursive Make Considered Harmful"	glondu	2009-09-21
*	Only one "in" clause in "destruct" even for a multiple "destruct".	herbelin	2009-09-20