coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Add [Polymorphic] flag for defs	msozeau	2011-04-13
*	Replaced printing number of ill-typed branch by printing name of constructor	herbelin	2011-04-08
*	Extraction: unfolds the let-in created by Program when handling "match"	letouzey	2011-04-07
*	- Add modulo_delta_types flag for unification to allow full	msozeau	2011-03-13
*	Keep information on which fields are subclasses in class declarations,	msozeau	2011-03-11
*	Tentative to make unification check types at every instanciation of an	msozeau	2011-03-11
*	Reverted commit r13893 about propagation of more informative	herbelin	2011-03-07
*	Added propagation of evars unification failure reasons for better	herbelin	2011-03-07
*	Improved define_evar_as_lambda which was creating an unrelated new evar	herbelin	2011-03-05
*	Add a flag to hide obligations in Program-generated terms under an	msozeau	2011-02-28
*	Interp a definition with the implicit arguments of its local context	pboutill	2011-02-10
*	Data structure telling implicits of local variables is a map in the	pboutill	2011-02-10
*	A fine-grain control of inlining at functor application via priority levels	letouzey	2011-01-31
*	Remove the "Boxed" syntaxes and the const_entry_boxed field	letouzey	2011-01-28
*	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
*	Remove an unused function with a Evd.fold in subtac	letouzey	2010-12-13
*	Delayed the evar normalization in error messages to the last minute	herbelin	2010-11-07
*	Add information of localisation when an error involving an "implicit	herbelin	2010-11-07
*	Cleaning the use of parentheses around evd and evdref (cosmetic commit).	herbelin	2010-10-31
*	Fix bug #2393: allow let-ins inside telescopes (only fails when there's	msozeau	2010-10-12
*	Fix bug# 2392	msozeau	2010-10-07
*	Added multiple implicit arguments rules per name.	herbelin	2010-10-03
*	Fix bug #2321, allowing "_" named projections in classes. Not realizing	msozeau	2010-09-28
*	Remove some occurrences of "open Termops"	glondu	2010-09-28
*	Some dead code removal, thanks to Oug analyzer	letouzey	2010-09-24
*	Minor fixes:	msozeau	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
*	Simplified the way internalization_data (i.e. bindings of bound vars	herbelin	2010-07-22
*	Cleaned a bit the grammar and terminology for binders (see dev/doc/changes.txt).	herbelin	2010-07-22
*	Move [delayed] to util and use [force_delayed] everywhere to force	msozeau	2010-06-30
*	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
*	Fixing spelling: pr_coma -> pr_comma	herbelin	2010-06-12
*	Fix bug #2262: bad implicit argument number by avoiding counting	msozeau	2010-06-09
*	Fix treatment of {struct x} annotations in presence of generalized	msozeau	2010-06-08
*	Added support for Ltac-matching terms with variables bound in the pattern	herbelin	2010-06-06
*	Add (almost) compatibility with camlp4, without breaking support for camlp5	letouzey	2010-05-19
*	static (and shared) camlp4use instead of per-file declaration	letouzey	2010-05-19
*	Remove compile-command pragmas for emacs	letouzey	2010-05-19
*	Remove the svn-specific $Id$ annotations	letouzey	2010-04-29
*	Here comes the commit, announced long ago, of the new tactic engine.	aspiwack	2010-04-22
*	Several bug-fixes and improvements of coqdoc	herbelin	2010-03-29
*	Oops, don't use zeta by default.	msozeau	2010-03-15
*	Fix splitting evars tactics and stop dropping evar constraints when	msozeau	2010-03-15
*	fixed confusion between number of cstr arguments and number of pattern variab...	barras	2010-03-12
*	Consider OccurCheck a catchable exception.	msozeau	2010-03-08
*	Reorder resolution of type class and unification constraints.	msozeau	2010-03-07