coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
*	Fixing multiple printing bugs with "Notation f x := ..."	herbelin	2011-04-08
*	Did that adding a rule for printing applications as "f(x)" works.	herbelin	2011-03-31
*	Remove some weird syntax "fun ... ," that used to be accepted (cf r13876)	letouzey	2011-03-16
*	Adapt test-suite/output/Extraction_matchs_2413 to new indentation of extraction	letouzey	2011-03-16
*	Fix inductive_template building ill-typed evars, and update test-suite scripts	msozeau	2011-03-13
*	Starting being more explicit on the reasons why module subtyping fails.	herbelin	2011-03-05
*	Improved define_evar_as_lambda which was creating an unrelated new evar	herbelin	2011-03-05
*	Try to fix the behavior of clenv_missing used when declaring hints	letouzey	2011-02-22
*	Some fixes of the test-suite scripts	letouzey	2011-02-21
*	Fix test-suite script.	msozeau	2011-02-21
*	MacOS compatibility	pboutill	2011-02-10
*	Correct handling of existential variables when multiple different	msozeau	2011-02-08
*	test-suite/Makefile: add a rule to build all_stdlib.v (for the bench)	glondu	2011-01-27
*	Add a test for sorting all universes of stdlib	glondu	2011-01-25
*	Add "Print Sorted Universes"	glondu	2011-01-11