coq - The formal proof system

Age	Commit message (Expand)	Author
2014-08-04	STM: encapsulate Pp.message in Feedback.feedback	Carst Tankink
2014-06-25	all coqide specific files moved into ide/	Enrico Tassi
2014-03-05	Adding a canary library. This canary is imperfect. It allows serialization	Pierre-Marie Pédrot
2014-03-05	Added a new module HMap. It works (almost) like Map, except that it expects	Pierre-Marie Pédrot
2014-03-05	Adding a CSet module in Coq lib.	Pierre-Marie Pédrot
2014-03-02	Grammar.cma with less deps (Glob_ops and Nameops) after moving minor code	Pierre Letouzey
2013-09-18	At least made the evar type opaque! There are still 5 remaining unsafe	ppedrot
2013-09-06	Moving Searchstack to CStack, and normalizing names a bit.	ppedrot
2013-08-25	Added a more efficient way to recover the domain of a map.	ppedrot
2013-07-02	Removing the use of leveled tactics wit_tacticn. It is now handled	ppedrot
2013-06-21	Cutting the dependency of Genarg in constr_expr, glob_constr	ppedrot
2013-06-18	Proof-of-concept: moved four easy-to-handle generic arguments to	ppedrot
2013-05-12	Added a generic notion of hook. Hooks are functions to be set	ppedrot
2013-03-12	Updated Exninfo to the new Store type.	ppedrot
2013-02-18	Added exception enrichment. Now one can define additional arbitrary	ppedrot
2013-01-28	Added backtrace primitives.	ppedrot
2012-12-14	Moving hcons_string to String namespace.	ppedrot
2012-12-14	Implemented a full-fledged equality on [constr_expr]. By the way,	ppedrot
2012-11-13	Added a CString module.	ppedrot
2012-11-08	Added an Int module with dummy utility functions.	ppedrot
2012-10-04	Moved Compat to parsing. This permits to break the dependency of the	ppedrot
2012-09-26	Reusing the Hashset data structure in Hashcons. Hopefully, this should	ppedrot
2012-09-18	More cleanup of Util: utf8 aspects moved to a new file unicode.ml	letouzey
2012-09-14	As r15801: putting everything from Util.array_* to CArray.*.	ppedrot
2012-09-14	Moving Utils.list_* to a proper CList module, which includes stdlib	ppedrot
2012-06-22	Added an indirection with respect to Loc in Compat. As many [open Compat]	ppedrot
2012-05-29	Extend become a mli-only file in intf/	letouzey
2012-05-29	place all files specific to camlp4 syntax extensions in grammar/	letouzey