coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Improving error message in explain_cannot_find_well_typed_abstraction:	herbelin	2013-04-17
*	Fix for bug #3017: wrong handling of the unresolvability status	msozeau	2013-04-03
*	Robust display of NotConvertibleTypeField errors (fix #3008, #2995)	letouzey	2013-03-21
*	Add type information in error message when a constructor is not fully	herbelin	2013-03-21
*	Embedded exns in LtacLocated and EvaluatedError satisfy Errors.noncritical	letouzey	2013-03-14
*	Restrict (try...with...) to avoid catching critical exn (part 13)	letouzey	2013-03-13
*	More monomorphization.	ppedrot	2013-03-05
*	Repairing r16205: errors raised by check_evar_instance were no longer	herbelin	2013-02-28
*	More informative error when a global reference is used in a context of	herbelin	2013-02-28
*	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