coq - The formal proof system

Age	Commit message (Expand)	Author
2013-04-11	Backport r16394 from 8.4:	msozeau
2013-04-03	Fix for bug #3017: wrong handling of the unresolvability status	msozeau
2013-04-02	Revised infrastructure for lazy loading of opaque proofs	letouzey
2013-04-02	Exporting the SearchAbout filter.	ppedrot
2013-03-26	Moved the Loadpath part of Library to its own file, and documented	ppedrot
2013-03-23	Minor code cleaning in CArray / CList.	ppedrot
2013-03-22	Fix bug# 2994, 2971 about better error messages.	msozeau
2013-03-21	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-19	Removing the module Libtypes and unifying the Search[Pattern\|Rewrite]?	ppedrot
2013-03-18	Making local variable warning verbose by default.	ppedrot
2013-03-17	Avoid a few overzealous "when Errors.noncritical"	letouzey
2013-03-14	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-13	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-12	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-11	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-08	catch failures of pr_vernac to make -time failsafe	gareuselesinge
2013-03-05	More monomorphization.	ppedrot
2013-02-28	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-27	Update debug code according to reorganization into modules.	msozeau
2013-02-26	kernel/declarations becomes a pure mli	letouzey
2013-02-24	Fixing bug #2466	ppedrot
2013-02-20	Corrects bug #2959 (error during Qed leads to assertion failure).	aspiwack
2013-02-19	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-18	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	Minor code cleanups, especially take advantage of Dir_path.is_empty	letouzey
2013-02-17	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-10	Useless use of hooks in VernacDefinition. In addition, this was	ppedrot
2013-02-10	Moved code from Pretype_error to Evarutil	ppedrot