coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Fixing discriminate for identity.	herbelin	2011-05-26
*	Q2R -> IQR	fbesson	2011-05-25
*	Made the emacs-U option deprecated. Also removed the old code	courtieu	2011-05-24
*	Applying Enrico Tassi's patch for giving priority to delta over eta in	herbelin	2011-05-24
*	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14152 85f007b7-540e-0...	fbesson	2011-05-23
*	ported r14149 from v8.3 branch: bug in checker (redefined global)	barras	2011-05-23
*	Restore display of notation when printing an inductive such as sig	letouzey	2011-05-21
*	added support to handle division by a constant over R	fbesson	2011-05-20
*	Remove useless "open Gc"	glondu	2011-05-19
*	Remove System.process_time (dead code)	glondu	2011-05-19
*	Extraction: avoid lots of late mind_of_kn	letouzey	2011-05-19
*	Extraction: global reference should be indexed on their user part (fix #2540)	letouzey	2011-05-19
*	cbv delta - [...] before calling lia	fbesson	2011-05-18
*	apply zeta reduction before syntaxification	fbesson	2011-05-18
*	Extraction: avoid printing of Recursive Extraction in coqide's console	letouzey	2011-05-18
*	Coqide: allow the use of Abort (grant wish #2357)	letouzey	2011-05-18
*	Class_tactics: Pervasives.(=) don't work for named_context_val (fix ATBR)	letouzey	2011-05-17
*	Modops: the strengthening functions can work without any env argument	letouzey	2011-05-17
*	More work on error handling	letouzey	2011-05-17
*	Add simple test of bullet behaviour.	aspiwack	2011-05-17
*	Break circular dependency Proof_global -> Vernacexpr -> Proof_global.	aspiwack	2011-05-17
*	Fixes bug in [maximal_unfocus] introduced in r14120.	aspiwack	2011-05-17
*	Repair the "Fail" command after recent changes in exception handling	letouzey	2011-05-16
*	test-suite: no more ..._beq in the output of the search tests	letouzey	2011-05-16
*	Fix order in Search tests.	letouzey	2011-05-16
*	Fixed my last patch: these files no longer use nat_beq (automatically	vsiles	2011-05-16
*	turn the automatic generation of boolean equality	vsiles	2011-05-16
*	Test for bug 462 and 2342 fixed by Matthieu's 13990 (or so).	herbelin	2011-05-15
*	Failing instead of switching to the coercion mechanism when VMcast	herbelin	2011-05-15
*	Turning Sys_error into error by default instead of anomaly. After all,	herbelin	2011-05-15
*	A better procedure for checking presence of undefined evars.	aspiwack	2011-05-13
*	The modules in proofs now use the Errors module to explain their exceptions t...	aspiwack	2011-05-13
*	A new mechanism to handle errors.	aspiwack	2011-05-13
*	New option [Set Bullet Behavior] allows to select the behaviour of bullets.	aspiwack	2011-05-13
*	Print Module (Type) M now tries to print more details	letouzey	2011-05-11
*	Improved lia + experimental nlia	fbesson	2011-05-09
*	remove useless dependancy for csdpcert	fbesson	2011-05-09
*	Fixes in the test-suite after modularisation of ZArith and co	letouzey	2011-05-06
*	Additionnal fix of romega after modularisation of ZArith	letouzey	2011-05-06
*	update of the file list in doc/stdlib	letouzey	2011-05-06
*	BinNat: N.binary_rect is now a definition instead of an opaque proof	letouzey	2011-05-05
*	Peano recursion for positive: integration of Daniel Schepler's code	letouzey	2011-05-05
*	Minimal lemmas about Z.gt, N.gt and co	letouzey	2011-05-05
*	Modularisation of Znat, a few name changed elsewhere	letouzey	2011-05-05
*	BinInt: Z.add become the alternative Z.add'	letouzey	2011-05-05
*	Modularization of BinInt, related fixes in the stdlib	letouzey	2011-05-05
*	Modularization of Nnat	letouzey	2011-05-05
*	Setoid_ring: some cleanups related with BinPos and BinNat	letouzey	2011-05-05
*	Wf.iter_nat becomes Peano.nat_iter (with an implicit arg)	letouzey	2011-05-05
*	BinNatDef containing all functions of BinNat, misc adaptations in BinPos	letouzey	2011-05-05