coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Numbers: change definition of divide (compat with Znumtheory)	letouzey	2011-06-24
*	cleanup of Zsgn	letouzey	2011-06-23
*	cleanup of Zmin and Zmax	letouzey	2011-06-23
*	Some more cleanup of Zorder	letouzey	2011-06-23
*	fix bug 2510: xml test is in the summary if it fails	pboutill	2011-06-22
*	Follow-up concerning eqb / ltb / leb comparisons	letouzey	2011-06-21
*	Cleaning debugging printer relative to new proof engine. In	herbelin	2011-06-21
*	Some migration of results from BinInt to Numbers	letouzey	2011-06-20
*	Zcompare.destr_zcompare subsumed by case Z.compare_spec	letouzey	2011-06-20
*	Clean-up of Zcompare and Zorder	letouzey	2011-06-20
*	Arithemtic: more concerning compare, eqb, leb, ltb	letouzey	2011-06-20
*	Some simplifications in NZDomain	letouzey	2011-06-20
*	Add compatibility option "-compat 8.3".	herbelin	2011-06-20
*	Fixing two typos introduced in r14217 and r14223	herbelin	2011-06-20
*	Ensured that the transparency state is used when flag betaiota is on for apply.	herbelin	2011-06-19
*	Relaxed the constraint introduced in r14190 that froze the existing	herbelin	2011-06-18
*	Generalizing flag use_evars_pattern_unification into a flag	herbelin	2011-06-18
*	Activating flags betaiota by default for apply	herbelin	2011-06-18
*	r14204 and 14218 continued: completely removing test for bug #2490,	herbelin	2011-06-18
*	Partial backtrack on wrong r14204: bug #2490 still open.	herbelin	2011-06-18
*	The ad hoc version for first-order unification at toplevel of "?n args	herbelin	2011-06-18
*	Typo in CHANGES	herbelin	2011-06-18
*	add names of theorems in output	jnarboux	2011-06-18
*	Customized accelerator maps for macos are globally installed (end to fix 2462)	pboutill	2011-06-17
*	Fix 2516: Utf8 font in Coqide Command panel	pboutill	2011-06-17
*	Fix bug 2269, program typechecker not used in Instance conclusions	msozeau	2011-06-17
*	refman nsatz	pottier	2011-06-16
*	Tests de nsatz avec la geometrie	pottier	2011-06-16
*	git rebase -i mess consequence	pboutill	2011-06-15
*	Revert "Coqide now need lablgtk2.14.0" + Ide build system debugging	pboutill	2011-06-14
*	Making printing of backtick in Program reparsable (avoiding collision with "`(")	herbelin	2011-06-14
*	Regression files for bugs #2304 and #2490.	herbelin	2011-06-14
*	Fixing bug #2181 (Class mechanism can create dependencies over unnamed	herbelin	2011-06-14
*	A few comments and a dev file to summarize issues with unification	herbelin	2011-06-13
*	Added full pattern-unification on Meta for tactic unification.	herbelin	2011-06-13
*	Added a flag to restrict conversion in tactic unification on the	herbelin	2011-06-13
*	Another bug of Scheme Induction (generated names dep/nodep were swapped).	herbelin	2011-06-13
*	Fixing an anomaly in Scheme Induction.	herbelin	2011-06-13
*	Oups, typo in previous commit	herbelin	2011-06-12
*	Removed what looks like a (very old) useless f.o. unification pass	herbelin	2011-06-12
*	Added a new flag for freezing evars in tactic unification. Used this	herbelin	2011-06-12
*	Rather quick hack to avoid using notations involving "Type" when	herbelin	2011-06-12
*	Coqide now need lablgtk2.14.0	pboutill	2011-06-11
*	Updated CHANGES (info, Show Script, rephrasing).	herbelin	2011-06-10
*	Moved allow_K to a unification flag	herbelin	2011-06-10
*	Fixing another bug with "_" intro pattern.	herbelin	2011-06-10
*	Fixing the "buggy" first_name and prepare multi-induction.	herbelin	2011-06-10
*	Made use of "_" in repeated use of intros_patterns work (with	herbelin	2011-06-10
*	Integrating onLastHypId into intro so that we can get the introduction	herbelin	2011-06-10
*	Call process_vernac_interp_error before calling Errors.print in	herbelin	2011-06-10