coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
*	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
*	Fixes in the test-suite after modularisation of ZArith and co	letouzey	2011-05-06
*	Fixing an "apply -> ... in hyp" bug (the hyp was considered as a fixed	herbelin	2011-04-28
*	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
*	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