coq - The formal proof system

Age	Commit message (Expand)	Author
2016-01-21	Merge branch 'v8.5'	Pierre-Marie Pédrot
2016-01-20	Update copyright headers.	Maxime Dénès
2015-12-31	Merge branch 'v8.5' into trunk	Guillaume Melquiond
2015-12-22	Inclusion of functors with restricted signature is now forbidden (fix #3746)	Pierre Letouzey
2015-10-29	Merge branch 'v8.5'	Pierre-Marie Pédrot
2015-10-28	Adds support for the virtual machine to perform reduction of universe polymor...	Gregory Malecha
2015-10-26	Merge branch 'v8.5'	Pierre-Marie Pédrot
2015-10-25	Safe_typing: add clean_bounded_mod_expr in Include Self of modtype (fix #4331)	Pierre Letouzey
2015-10-25	Minor module cleanup : error HigherOrderInclude was never happening	Pierre Letouzey
2015-10-06	Splitting kernel universe code in two modules.	Pierre-Marie Pédrot
2015-10-02	Univs: forgot a substitution in mod_typing.	Matthieu Sozeau
2015-10-02	Univs: correct handling of with in modules	Matthieu Sozeau
2015-10-02	Univs: module constraints move to universe contexts as they might	Matthieu Sozeau
2015-07-16	Modules: fix bug #4294	Matthieu Sozeau
2015-03-25	Fix vm compiler to refuse to compile code making use of inductives with	Matthieu Sozeau
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	Declarations.mli refactoring: module_type_body = module_body	Pierre Letouzey
2014-10-13	library/opaqueTables: enable their use in interactive mode	Enrico Tassi
2014-05-06	Adapt universe polymorphic branch to new handling of futures for delayed proofs.	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
2014-02-26	New compilation mode -vi2vo	Enrico Tassi
2013-08-20	Declarations.mli: reorganization of modular structures	letouzey
2013-08-20	Mod_typing : code cleanup	letouzey
2013-08-20	Safe_typing code refactoring	letouzey
2013-08-08	State Transaction Machine	gareuselesinge
2013-07-17	Modops.destr_functor without useless env	letouzey
2013-02-26	kernel/declarations becomes a pure mli	letouzey
2013-01-28	Uniformization of the "anomaly" command.	ppedrot
2012-12-18	Modulification of Label	ppedrot
2012-11-22	Monomorphization (kernel)	ppedrot
2012-09-14	Partial revert of Yann commit in order to use CLib.List when opening	ppedrot
2012-09-14	This patch removes unused "open" (automatically generated from	regisgia
2012-08-08	Updating headers.	herbelin
2012-03-26	Module names and constant/inductive names are now in two separate namespaces	letouzey
2012-03-02	Noise for nothing	pboutill
2011-05-17	Modops: the strengthening functions can work without any env argument	letouzey
2011-04-12	Subtyping: align coqtop behavior concerning opaque csts on coqchk's one	letouzey
2011-04-03	Lazy loading of opaque proofs: fast as -dont-load-proofs without its drawbacks	letouzey
2011-03-05	Moving printing of module typing errors upwards to himsg.ml so as to	herbelin
2011-02-11	Mod_typing: some refactoring (common parts about MSEapply and co)	letouzey
2011-01-31	A fine-grain control of inlining at functor application via priority levels	letouzey
2011-01-28	Remove the "Boxed" syntaxes and the const_entry_boxed field	letouzey
2010-12-18	Univ.constraints made fully abstract instead of being a Set of abstract stuff	letouzey
2010-09-24	Some dead code removal, thanks to Oug analyzer	letouzey
2010-07-24	Updated all headers for 8.3 and trunk	herbelin
2010-07-07	Mod_typing: fix the content of the typ_expr_alg field	letouzey
2010-05-09	Added a few informations about file lineages (for the most part in kernel)	herbelin
2010-04-29	Remove the svn-specific $Id$ annotations	letouzey