coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Declarations.mli: reorganization of modular structures	letouzey	2013-08-20
*	Himsg : strict 80-column indentation	letouzey	2013-08-20
*	Safe_typing code refactoring	letouzey	2013-08-20
*	Added more flags choice in desambiguating printer. The code is	ppedrot	2013-08-06
*	Tentative fix for bug #2961. When we have to print two terms that	ppedrot	2013-08-05
*	Fixing #2846: Uncaught exception Reduction.NotArity.	ppedrot	2013-08-04
*	Using the whole tactic environment while Pretyping.	ppedrot	2013-06-24
*	Generalizing the use of maps instead of lists in the interpretation	ppedrot	2013-06-22
*	Replacing lists by maps in matching interpretation.	ppedrot	2013-06-05
*	Improvement of r16204 on reporting tactic error locations: if the main	herbelin	2013-05-05
*	Merging Context and Sign.	ppedrot	2013-04-29
*	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