coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Fixing bug #2466	ppedrot	2013-02-24
*	use List.rev_map whenever possible	letouzey	2013-02-18
*	Displaying environment and unfolding aliases in "cannot_unify"	herbelin	2013-02-17
*	A more informative message when the elimination predicate for	herbelin	2013-02-17
*	Added propagation of evars unification failure reasons for better	herbelin	2013-02-17
*	Revised the Ltac trace mechanism so that trace breaking due to	herbelin	2013-02-17
*	Moved code from Pretype_error to Evarutil	ppedrot	2013-02-10
*	Renaming evar_env/evar_unfiltered_env into evar_filtered_env/evar_env	herbelin	2013-01-29
*	Modulification of Label	ppedrot	2012-12-18
*	Modulification of identifier	ppedrot	2012-12-14
*	Monomorphization (toplevel)	ppedrot	2012-11-26
*	Added a CString module.	ppedrot	2012-11-13
*	Monomorphized a lot of equalities over OCaml integers, thanks to	ppedrot	2012-11-08
*	Clean-up of proof_type.ml : no more Nested nor abstract_tactic_box	letouzey	2012-10-06
*	Improving error message when abtraction over goal (abstract_list_all	herbelin	2012-10-04
*	Moving Utils.list_* to a proper CList module, which includes stdlib	ppedrot	2012-09-14
*	This patch removes unused "open" (automatically generated from	regisgia	2012-09-14
*	Updating headers.	herbelin	2012-08-08
*	Fix typeclass error handling which was sometimes raising a Failure ("hd").	msozeau	2012-07-11
*	rewrite_db : a first attempt at using rewrite_strat for a quicker autorewrite	letouzey	2012-07-05
*	Added an indirection with respect to Loc in Compat. As many [open Compat]	ppedrot	2012-06-22
*	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