coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	ring2, cring, nsatz avec type classe avec parametres plus notations	pottier	2011-06-10
*	More fixes in pruning/restriction of evars during unification.	msozeau	2011-06-09
*	Make Notation works with anonymous-level "Type".	herbelin	2011-06-08
*	Fixes in pruning in unification.	msozeau	2011-06-08
*	Fix bug #2399 in Program: used to build an ill-formed term due to a de Bruijn...	msozeau	2011-06-07
*	Fix bug #2335, fail if the search for reflexivity/symmetry/transitivity proof...	msozeau	2011-06-07
*	Catch AbstractionOverMeta as a unification failure in precatchable_exception.	msozeau	2011-06-07
*	Fix bug #2415: warn when closing modules or sections and some obligations are...	msozeau	2011-06-07
*	Fixed bug #2398: destruct ex2/sig2/sigT2 in Program, patch by Paolo Herms.	msozeau	2011-06-07
*	- Fix restrict_hyps to not allow filtering on a variable required to typechec...	msozeau	2011-06-07
*	Typo.	gmelquio	2011-06-06
*	Mini-test for eta	herbelin	2011-05-26
*	Partial fix for accepting bound variables with same name as implicit	herbelin	2011-05-26
*	Check if recursive calls are guarded before printing "Proof completed".	herbelin	2011-05-26
*	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