coq - The formal proof system

Age	Commit message (Expand)	Author
2016-07-03	errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...	Pierre Letouzey
2016-06-29	A new infrastructure for warnings.	Maxime Dénès
2016-05-31	Feedback cleanup	Emilio Jesus Gallego Arias
2016-05-08	Removing dead code and unused opens.	Pierre-Marie Pédrot
2016-01-20	Update copyright headers.	Maxime Dénès
2016-01-04	Extraction: msg_notice instead of msg_info.	Pierre Courtieu
2015-12-22	Inclusion of functors with restricted signature is now forbidden (fix #3746)	Pierre Letouzey
2015-12-14	Extraction: cosmetically avoid generating spaces on empty lines	Pierre Letouzey
2015-12-12	Extraction: nicer implementation of Implicits	Pierre Letouzey
2015-12-12	Extraction: fix for bug #4334 (use of delta_resolver in Extract_env)	Pierre Letouzey
2015-04-09	Add extraction to JSON.	Nickolai Zeldovich
2015-03-21	Properly capitalize filenames when extracting to Haskell. (Fix for bug #3221)	Guillaume Melquiond
2015-02-12	Univs: fix bug #3978: carry around the universe context used to	Matthieu Sozeau
2015-01-12	Update headers.	Maxime Dénès
2015-01-11	Extraction: discard code unnecessary to fulfill a module signature	Pierre Letouzey
2015-01-11	Declarations.mli refactoring: module_type_body = module_body	Pierre Letouzey
2015-01-11	Extraction: discard unnecessary code inside modules without signatures	Pierre Letouzey
2015-01-11	Extraction : some more support functions for a future "Extraction Compute"	Pierre Letouzey
2014-05-06	Initial work on reintroducing old-style polymorphism for compatibility (the s...	Matthieu Sozeau
2014-05-06	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau
2014-02-26	Lazyconstr -> Opaqueproof	Enrico Tassi
2013-09-27	Removing a bunch of generic equalities.	ppedrot
2013-08-22	Nicer code concerning dirpaths and modpath around Lib	letouzey
2013-08-20	Declarations.mli: reorganization of modular structures	letouzey
2013-07-17	Lib.contents () instead of Lib.contents_after None	letouzey
2013-07-17	Extraction : message about lack of support for toplevel Include	letouzey
2013-03-15	Extract_env : correct exceptions mentionned in a try ... with	letouzey
2013-03-13	Restrict (try...with...) to avoid catching critical exn (part 9)	letouzey
2013-03-13	Restrict (try...with...) to avoid catching critical exn (part 6)	letouzey
2013-02-26	kernel/declarations becomes a pure mli	letouzey
2013-02-26	Names: shortcuts for building {kn, constant, mind} with empty sections	letouzey
2013-02-19	Dir_path --> DirPath	letouzey
2013-01-28	Uniformization of the "anomaly" command.	ppedrot
2012-12-18	Modulification of Label	ppedrot
2012-12-14	Modulification of dir_path	ppedrot
2012-12-14	Modulification of identifier	ppedrot
2012-10-30	Extraction: avoid initial strange empty comments after Arnaud's hack	letouzey
2012-10-02	Remove some more "open" and dead code thanks to OCaml4 warnings	letouzey
2012-09-17	More cleaning on Utils and CList. Some parts of the code being	ppedrot
2012-09-15	Some documentation and cleaning of CList and Util interfaces.	ppedrot
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-08-24	Experimental support for a comment in the files' preamble in extraction.	aspiwack
2012-08-08	Updating headers.	herbelin
2012-08-06	Vecnacentries.dump_global silently ignores exceptions	pboutill
2012-08-05	Dump references in Extraction	pboutill
2012-06-01	More cleaning	ppedrot
2012-06-01	Getting rid of Pp.msgnl and Pp.message.	ppedrot
2012-05-29	global_reference migrated from Libnames to new Globnames, less deps in gramma...	letouzey
2012-03-26	Module names and constant/inductive names are now in two separate namespaces	letouzey