coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Added support for referring to subterms of the goal by pattern.	herbelin	2011-09-26
*	test-suite : an additional message displayed by Notation2.v	letouzey	2011-09-22
*	Fix test-suite for s/Defining '\1' as keyword/Identifier '\1' now a keyword/.	letouzey	2011-09-22
*	Fix test-suite/ide for repository compiled without -local (fix #2600)	letouzey	2011-09-19
*	Various fixes in the Makefiles	letouzey	2011-09-17
*	Omega aware of Z.pred (fix #1912)	letouzey	2011-09-15
*	Re-allowing assumptions during proofs seems safe now (fix #2411)	letouzey	2011-09-15
*	test-suite/ide: misc improvement	letouzey	2011-09-06
*	fake_ide: a short program to mimic an ide talking to coqtop -ideslave	letouzey	2011-09-05
*	Fixing printing bug with last trailing non-maximally implicit	herbelin	2011-08-10
*	Partly revert commit r14389 about relaxing the condition for being a keyword	herbelin	2011-08-10
*	Be a bit less aggressive in declaring idents as keywords in notations	herbelin	2011-08-08
*	moins de reification inutile, noatations standards	pottier	2011-08-04
*	or_introl is now too complicated for basic tests of test-suite/output/PrintIn...	pboutill	2011-07-26
*	This adds two option tables 'Printing Record' and 'Printing Constructor'	herbelin	2011-07-16
*	fix bug 2510: xml test is in the summary if it fails	pboutill	2011-06-22
*	Relaxed the constraint introduced in r14190 that froze the existing	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
*	add names of theorems in output	jnarboux	2011-06-18
*	Tests de nsatz avec la geometrie	pottier	2011-06-16
*	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
*	Added full pattern-unification on Meta for tactic unification.	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
*	Added a new flag for freezing evars in tactic unification. Used this	herbelin	2011-06-12
*	Fixing another bug with "_" intro pattern.	herbelin	2011-06-10
*	Made use of "_" in repeated use of intros_patterns work (with	herbelin	2011-06-10
*	ring2, cring, nsatz avec type classe avec parametres plus notations	pottier	2011-06-10
*	Make Notation works with anonymous-level "Type".	herbelin	2011-06-08
*	Mini-test for eta	herbelin	2011-05-26
*	Partial fix for accepting bound variables with same name as implicit	herbelin	2011-05-26
*	Fixing discriminate for identity.	herbelin	2011-05-26
*	Add simple test of bullet behaviour.	aspiwack	2011-05-17
*	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
*	Test for bug 462 and 2342 fixed by Matthieu's 13990 (or so).	herbelin	2011-05-15
*	Fixes in the test-suite after modularisation of ZArith and co	letouzey	2011-05-06
*	Merge branch 'subclasses' into coq-trunk	msozeau	2011-05-05
*	Typo in test InitSyntax.out	herbelin	2011-04-29
*	Fixing an "apply -> ... in hyp" bug (the hyp was considered as a fixed	herbelin	2011-04-28
*	Fixed notation printing bug when curly brackets are involved (requests	herbelin	2011-04-28
*	Fixing output of Notations2.v test messed up in r14060	herbelin	2011-04-27
*	Fixing and completing interpretation of let's in notations for iterated binders.	herbelin	2011-04-25
*	Take benefit of eta-expansion so that "ex P" is displayed "exists x, P x".	herbelin	2011-04-15
*	Revert "Add [Polymorphic] flag for defs"	msozeau	2011-04-13
*	- Do not make constants with an assigned type polymorphic (wrong unfoldings).	msozeau	2011-04-13
*	Add [Polymorphic] flag for defs	msozeau	2011-04-13
*	Applying and reworking Tom Prince's patch for test-suite/failure/universes2.v	herbelin	2011-04-08