coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Evar_kinds.mli containing former Evd.hole_kind, avoid deps on Evd	letouzey	2012-05-29
*	Fix interface of resolve_typeclasses: onlyargs -> with_goals:	msozeau	2012-03-20
*	Fixing alpha-conversion bug #2723 introduced in r12485-12486.	herbelin	2012-03-20
*	Noise for nothing	pboutill	2012-03-02
*	Fix typeclass resolution error message which included goal evars (bug #2620).	msozeau	2012-01-23
*	Quick improvement of some error messages related to module application	herbelin	2011-08-30
*	Improving error message about coinductive guard (old "cases" is now "match")	herbelin	2011-08-10
*	Fix nf_evars_undefined use in pr_constraints	msozeau	2011-08-03
*	Cleaning debugging printer relative to new proof engine. In	herbelin	2011-06-21
*	Replaced printing number of ill-typed branch by printing name of constructor	herbelin	2011-04-08
*	Finish branching functions handling module errors (cf. r13886)	letouzey	2011-03-16
*	- Better error messages taking unif. constraints into account.	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
*	Moving printing of module typing errors upwards to himsg.ml so as to	herbelin	2011-03-05
*	A few more betaiota on environments and types of error messages. Seems to	herbelin	2011-03-05
*	Rename rawterm.ml into glob_term.ml	glondu	2010-12-23
*	Change of nomenclature: rawconstr -> glob_constr	glondu	2010-12-23
*	Misc improvements about evar_map	letouzey	2010-12-15
*	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
*	Two [Evd.fold] turned into [Evd.fold_undefined].	aspiwack	2010-10-04
*	Fixed a bug in printing fix/cofix error messages when several	herbelin	2010-09-24
*	Updated all headers for 8.3 and trunk	herbelin	2010-07-24
*	Fixed bug #2135 (second-order unification was raising cryptic message)	herbelin	2010-06-12
*	Fixing spelling: pr_coma -> pr_comma	herbelin	2010-06-12
*	Added support for Ltac-matching terms with variables bound in the pattern	herbelin	2010-06-06
*	Applicative commutative cuts in Fixpoint guard condition	pboutill	2010-05-18
*	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
*	missing space in error message	vsiles	2010-04-20
*	Fix splitting evars tactics and stop dropping evar constraints when	msozeau	2010-03-15
*	Opened the possibility to type Ltac patterns but it is not fully functional yet	herbelin	2009-12-24
*	Promote evar_defs to evar_map (in Evd)	glondu	2009-11-11
*	A bit of cleaning around name generation + creation of dedicated file namegen.ml	herbelin	2009-11-09
*	Hopefully improved layout of fix guardness error message.	herbelin	2009-10-29
*	Delete trailing whitespaces in all .{v,ml} files	glondu	2009-09-17
*	Fix "unsatisfiable constraints" error messages to include all the	msozeau	2009-06-18
*	Use a lazy value for the message in FailError, so that it won't be	msozeau	2009-06-11
*	Rewrite of Program Fixpoint to overcome the previous limitations:	msozeau	2009-03-28
*	Backport from v8.2 branch of 11986 (interpretation of quantified	herbelin	2009-03-22
*	commande Timeout + compaction des traces de debug_tactic	barras	2009-03-04
*	On remplace evar_map par evar_defs (seul evar_defs est désormais exporté	aspiwack	2009-02-19
*	- Deactivation of dynamic loading on Mac OS 10.5 (see bug #2024).	herbelin	2009-01-11
*	Moved parts of Sign to Term. Unified some names (e.g. decomp_n_prod ->	herbelin	2008-12-31
*	Inductive parameters: nicer doc examples and error message	letouzey	2008-11-28
*	- Fixed bug 1968 (inversion failing due to a Not_found bug introduced in	herbelin	2008-11-09
*	Fix in the unification algorithm using evars: unify types of evar	msozeau	2008-11-05
*	Raise informative errors instead of Failures or anomalies in case a meta	msozeau	2008-10-24
*	Fix bug #1940: uncaught exception when searching for a type class.	msozeau	2008-09-14