coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	code simplifications concerning Summary	letouzey	2013-04-22
*	interface.mli and serialize.ml reworked to avoid copy/paste of types	gareuselesinge	2013-04-19
*	Only arguments declared as implicit can be renamed	gareuselesinge	2013-04-18
*	Matching patterns: fixed allow_partial_app which was not working on	herbelin	2013-04-17
*	Coqc: repair localisation of errors in files	letouzey	2013-04-17
*	Improving error message in explain_cannot_find_well_typed_abstraction:	herbelin	2013-04-17
*	More functional implementation of locality_flag and program_mode	gareuselesinge	2013-04-15
*	Backport r16394 from 8.4:	msozeau	2013-04-11
*	Fix for bug #3017: wrong handling of the unresolvability status	msozeau	2013-04-03
*	Revised infrastructure for lazy loading of opaque proofs	letouzey	2013-04-02
*	Exporting the SearchAbout filter.	ppedrot	2013-04-02
*	Moved the Loadpath part of Library to its own file, and documented	ppedrot	2013-03-26
*	Minor code cleaning in CArray / CList.	ppedrot	2013-03-23
*	Fix bug# 2994, 2971 about better error messages.	msozeau	2013-03-22
*	Robust display of NotConvertibleTypeField errors (fix #3008, #2995)	letouzey	2013-03-21
*	Typo dans message d'erreur (obligations).	herbelin	2013-03-21
*	Add type information in error message when a constructor is not fully	herbelin	2013-03-21
*	Check unexpected "Local" keyword in cmd before opening a proof (fix #2975)	letouzey	2013-03-21
*	Removing the module Libtypes and unifying the Search[Pattern\|Rewrite]?	ppedrot	2013-03-19
*	Making local variable warning verbose by default.	ppedrot	2013-03-18
*	Avoid a few overzealous "when Errors.noncritical"	letouzey	2013-03-17
*	Embedded exns in LtacLocated and EvaluatedError satisfy Errors.noncritical	letouzey	2013-03-14
*	Cerrors: get rid of some FIXME	letouzey	2013-03-14
*	Use Pp.msg instead of Pp.pp in -beautify (loss of text otherwise)	letouzey	2013-03-14
*	Modules and ppvernac, sequel of Enrico's commit 16261	letouzey	2013-03-13
*	Toplevel: improved comments	letouzey	2013-03-13
*	Vernac+Toplevel: get rid of Error_in_file	letouzey	2013-03-13
*	Vernac+Toplevel: get rid of DuringVernacInterp	letouzey	2013-03-13
*	Restrict (try...with...) to avoid catching critical exn (part 14)	letouzey	2013-03-13
*	Restrict (try...with...) to avoid catching critical exn (part 13)	letouzey	2013-03-13
*	Restrict (try...with...) to avoid catching critical exn (part 10)	letouzey	2013-03-13
*	invalid_arg instead of raise (Invalid_argement ...)	letouzey	2013-03-12
*	Allowing different types of, not to be mixed, generic Stores through	ppedrot	2013-03-12
*	Allowing (Co)Fixpoint to be defined local and Let-style.	ppedrot	2013-03-11
*	Obligations generated by Program are now local.	ppedrot	2013-03-11
*	Added a Local Definition vernacular command. This type of definition	ppedrot	2013-03-11
*	catch failures of pr_vernac to make -time failsafe	gareuselesinge	2013-03-08
*	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
*	Update debug code according to reorganization into modules.	msozeau	2013-02-27
*	kernel/declarations becomes a pure mli	letouzey	2013-02-26
*	Fixing bug #2466	ppedrot	2013-02-24
*	Corrects bug #2959 (error during Qed leads to assertion failure).	aspiwack	2013-02-20
*	avoid (Int.equal (cmp ...) 0) when a boolean equality exists	letouzey	2013-02-19
*	Dir_path --> DirPath	letouzey	2013-02-19
*	Names: revised representation of constants and mutual_inductive	letouzey	2013-02-19
*	Removing Exc_located and using the new exception enrichement	ppedrot	2013-02-18
*	Updating the backtrace handling mechanism to accomodate the new	ppedrot	2013-02-18
*	use List.rev_map whenever possible	letouzey	2013-02-18