coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
*	Fixing an uncaught exception bug with use of vmcast	herbelin	2011-01-07
*	Remove the two-argument variant of "decide equality"	glondu	2010-12-23
*	Extraction: avoid type-unsafe optimisation of pattern-matchings (fix #2413)	letouzey	2010-12-21
*	Fixing bug #2454: inversion predicate strategy for inferring the type	herbelin	2010-12-19
*	Fixing bug #2448 (wrongly-scoped alpha-renaming in notations).	herbelin	2010-12-04
*	Fixing bug using explictly declared implicit arguments in inductive arities.	herbelin	2010-12-03
*	Fixing a bug introduced in r12304 (move of interpretation of	herbelin	2010-12-02
*	SearchAbout: who has never been annoyed by the [ ] syntax ?	letouzey	2010-11-19
*	An experimental support for open constrs in hints and in "using"	herbelin	2010-10-31
*	Fix missing -coqlib argument to coqdep in test-suite	glondu	2010-10-16
*	Adding test-case for bug #2362, which uses HO unification during	msozeau	2010-10-12
*	Fix bug #2393: allow let-ins inside telescopes (only fails when there's	msozeau	2010-10-12
*	Backporting r13521 from branch 8.3 to trunk (fixing bug #2406, looping	herbelin	2010-10-11
*	test-suite: fix success/unification.v	glondu	2010-10-07
*	test-suite: fix output/Existentials.out	glondu	2010-10-06
*	test-suite: fix success/Typeclasses.v	glondu	2010-10-05
*	test-suite: fix success/AdvancedCanonicalStructure.v	glondu	2010-10-05
*	Export definition of type implicits_list for contribs + fixed a	herbelin	2010-10-05
*	test-suite: use unified diff output and use expected output as reference	glondu	2010-10-05
*	Fixing bugs in previous commits about implicit arguments:	herbelin	2010-10-04
*	Test for non-regression of the display bug fixed in r13486.	herbelin	2010-10-03
*	Added multiple implicit arguments rules per name.	herbelin	2010-10-03
*	Making display of various informations about constants more modular:	herbelin	2010-10-03
*	Improve handling of metas as evars in unification (patch by Hugo)	letouzey	2010-09-30
*	Fix inconsistency in Prop/Set conversion check	glondu	2010-09-23
*	Fixed test of bug #2360 (use of Fail to check a regular error instead	herbelin	2010-09-20
*	Fixing bug #2360 (descend_in_conjunctions built ill-typed terms). Shouldn't we	herbelin	2010-09-19
*	Added test for bugs 2242, 2337, 2339 + remove the use of name "ambiguous" in	herbelin	2010-09-18
*	Fixing bugs #2347 (part 2) and #2388: error message printing was done	herbelin	2010-09-18
*	Fixed a problem introduced in r12607 after pattern_of_constr served	herbelin	2010-09-17
*	In the computation of missing arguments for apply, accept that the	herbelin	2010-09-17
*	Improving a few error messages in Ltac interpretation	herbelin	2010-09-11
*	fixed bug #2375 (congruence)	corbinea	2010-09-02
*	Updated test on Nsatz after Loïc moved NsatzR to Nsatz.	herbelin	2010-07-30
*	test-case for bug #2105	barras	2010-07-29
*	unification des tactiques nsatz pour R Z avec celle des anneaux integres	pottier	2010-07-28
*	fixed bug #2139: compiled cofix loops, missing offset to evaluate cofix bodies	barras	2010-07-28
*	nstaz pour les anneaux integres et les setoides, R Z et Q	pottier	2010-07-27
*	Updated all headers for 8.3 and trunk	herbelin	2010-07-24
*	Extension of the recursive notations mechanism	herbelin	2010-07-22