coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Remove some weird syntax "fun ... ," that used to be accepted (cf r13876)	letouzey	2011-03-16
*	Fix inductive_template building ill-typed evars, and update test-suite scripts	msozeau	2011-03-13
*	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
*	Correct handling of existential variables when multiple different	msozeau	2011-02-08
*	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
*	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
*	test-suite: fix success/unification.v	glondu	2010-10-07
*	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
*	Fixing bugs in previous commits about implicit arguments:	herbelin	2010-10-04
*	Added multiple implicit arguments rules per name.	herbelin	2010-10-03
*	Improve handling of metas as evars in unification (patch by Hugo)	letouzey	2010-09-30
*	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
*	unification des tactiques nsatz pour R Z avec celle des anneaux integres	pottier	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
*	Fix compilation and test-suite of nsatz	glondu	2010-07-12
*	nsatz in an integral domain with specialization to Z and R	pottier	2010-07-08
*	Made tclABSTRACT normalize evars before saying it does not support	herbelin	2010-06-29
*	Restored a "feature" of unification in pre-8.3 (it was used e.g. in a	herbelin	2010-06-25
*	Fixed bug #2314 (inversion using not checking the correctness of its arguments	herbelin	2010-06-13
*	Mainly made that evarconv is able to solve "?n = (fun x => x) ?n" (sic).	herbelin	2010-06-11
*	Automatic introduction of names given before ":" in Lemma's and	herbelin	2010-06-09
*	Backported r13080 (support for open terms in ltac matching) from trunk to v8.3.	herbelin	2010-06-09
*	Added support for Ltac-matching terms with variables bound in the pattern	herbelin	2010-06-06
*	Grobner.v removed	pottier	2010-06-04
*	plugin groebner updated and renamed as nsatz; first version of the doc of nsa...	pottier	2010-06-03
*	Remove the svn-specific $Id$ annotations	letouzey	2010-04-29
*	Moved Case3.v from ideal features to success (it works since 8.2).	herbelin	2010-04-17
*	Recovering 8.2 behavior of "simple (e)apply" (and hence of "(e)auto").	herbelin	2010-04-11
*	Commit 12906 continued (forgotten file).	herbelin	2010-04-07
*	Added automatic expansion on the left of recursive notations	herbelin	2010-03-23
*	fixed minor pbs with test cases	barras	2010-03-12
*	fixed confusion between number of cstr arguments and number of pattern variab...	barras	2010-03-12
*	ajout test de fied_simplify_eq in	barras	2010-02-10
*	New version of 12650 that was broken (supporting again records when	herbelin	2010-01-12
*	revert commit 12650 for the moment, since it breaks MSetAVL	letouzey	2010-01-12