coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Added a table for using reserved names for binding names to types	herbelin	2011-03-05
*	A few more betaiota on environments and types of error messages. Seems to	herbelin	2011-03-05
*	Added support for instantiation of ?n by a lambda when "?n a" has to	herbelin	2011-03-05
*	Reorganized a bit evarconv.ml:	herbelin	2011-03-05
*	Improved define_evar_as_lambda which was creating an unrelated new evar	herbelin	2011-03-05
*	Instantiate evar by a lambda when "?n args" has to unify with Prod	herbelin	2011-03-05
*	- Use transparency information all the way through unification and	msozeau	2011-02-17
*	- Fix treatment of globality flag for typeclass instance hints (they	msozeau	2011-02-14
*	An automatic substitution of scope at functor application	letouzey	2011-02-11
*	In evars_of_term and co, visit array c in Evar(_,c) (sequel to r13809)	letouzey	2011-02-11
*	Repair Class_tactics.split_evars, broken by r13717 (should fix #2481)	letouzey	2011-02-03
*	Make simpl use the proper constant when folding (mutual) fixpoints	letouzey	2011-01-27
*	ratrapage exception, deja fait ...	bgregoir	2011-01-11
*	Fixing an uncaught exception bug with use of vmcast	herbelin	2011-01-07
*	mli comments for doc	pboutill	2011-01-07
*	Rename mkR* smart constructors (mostly in funind)	glondu	2010-12-25
*	More {raw => glob} changes for consistency	glondu	2010-12-24
*	Rename rawterm.ml into glob_term.ml	glondu	2010-12-23
*	Change of nomenclature: rawconstr -> glob_constr	glondu	2010-12-23
*	Fixing bug #2454: inversion predicate strategy for inferring the type	herbelin	2010-12-19
*	Univ.constraints made fully abstract instead of being a Set of abstract stuff	letouzey	2010-12-18
*	Misc improvements about evar_map	letouzey	2010-12-15
*	Refresh universes in params when generating schemes (Closes: #2429)	glondu	2010-11-08
*	Delayed the evar normalization in error messages to the last minute	herbelin	2010-11-07
*	An experimental support for open constrs in hints and in "using"	herbelin	2010-10-31
*	Cleaning the use of parentheses around evd and evdref (cosmetic commit).	herbelin	2010-10-31
*	Slight cosmetic cleaning of tacred.ml.	herbelin	2010-10-31
*	Fixing the Not_found error in bug #2404 + dead code removal in cases.ml	herbelin	2010-10-06
*	Improve handling of metas as evars in unification (patch by Hugo)	letouzey	2010-09-30
*	Speed-up refine by avoiding some calls to Evd.fold	letouzey	2010-09-30
*	Fix bug #2321, allowing "_" named projections in classes. Not realizing	msozeau	2010-09-28
*	Remove some occurrences of "open Termops"	glondu	2010-09-28
*	Remove "init" label from Termops.it_mk* specialized functions	glondu	2010-09-28
*	Some dead code removal, thanks to Oug analyzer	letouzey	2010-09-24
*	Added eta-expansion in kernel, type inference and tactic unification,	herbelin	2010-09-20
*	Improving a few error messages in Ltac interpretation	herbelin	2010-09-11
*	Fix [clenv_missing] to compute a better approximation of missing	msozeau	2010-08-02
*	kernel conversion and reduction do not raise assert failure on ill-typed term...	barras	2010-07-29
*	fixed bug #2105 (compilation of free de Bruijn) and missing lift of predicate...	barras	2010-07-29
*	Minor fixes:	msozeau	2010-07-27
*	Updated all headers for 8.3 and trunk	herbelin	2010-07-24
*	Some fine-tuning after removal of automatic imports of coercions in r13310	herbelin	2010-07-23
*	Extension of the recursive notations mechanism	herbelin	2010-07-22
*	Made coercions active only when modules are imported.	herbelin	2010-07-22
*	Reverted 13293 commited mistakenly. Sorry for the noise.	herbelin	2010-07-18
*	Tentative de suppression de l'import automatique des hints et coercions.	herbelin	2010-07-18
*	Fix (part of) bug #2347, de Bruijn bug in Program's pretyper.	msozeau	2010-06-30
*	Made tclABSTRACT normalize evars before saying it does not support	herbelin	2010-06-29
*	Fixed a bug introduced in a combination in r12807 and revealed in	herbelin	2010-06-28
*	Applying François' patches about Canonical Projections (see #2302 and #2334).	herbelin	2010-06-26