coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Adding a comment regarding De Bruijn universe indices in the kernel.	Pierre-Marie Pédrot	2017-07-12
*	Cleaning up the implementation of module subtyping in the kernel.	Pierre-Marie Pédrot	2017-07-11
*	Merge PR #853: Clean 'with Definition' implementation.	Maxime Dénès	2017-07-06
\|\
* \|	Bump year in headers.	Pierre-Marie Pédrot	2017-07-04
\| *	Do not add original constraints to the environment in 'with Definition' check.	Pierre-Marie Pédrot	2017-07-03
\|/
*	Clean up universes of constants and inductives	Amin Timany	2017-06-16
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-21
\|\
\| *	Update copyright headers.	Maxime Dénès	2016-01-20
* \|	Merge branch 'v8.5' into trunk	Guillaume Melquiond	2015-12-31
\|\\|
\| *	Inclusion of functors with restricted signature is now forbidden (fix #3746)	Pierre Letouzey	2015-12-22
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-29
\|\\|
\| *	Adds support for the virtual machine to perform reduction of universe polymor...	Gregory Malecha	2015-10-28
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-26
\|\\|
\| *	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-25
* \|	Splitting kernel universe code in two modules.	Pierre-Marie Pédrot	2015-10-06
\|/
*	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-10-02
*	Modules: fix bug #4294	Matthieu Sozeau	2015-07-16
*	Fix vm compiler to refuse to compile code making use of inductives with	Matthieu Sozeau	2015-03-25
*	Univs: fix bug #3978: carry around the universe context used to	Matthieu Sozeau	2015-02-12
*	Update headers.	Maxime Dénès	2015-01-12
*	Declarations.mli refactoring: module_type_body = module_body	Pierre Letouzey	2015-01-11
*	library/opaqueTables: enable their use in interactive mode	Enrico Tassi	2014-10-13
*	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-05-06
*	Lazyconstr -> Opaqueproof	Enrico Tassi	2014-02-26
*	New compilation mode -vi2vo	Enrico Tassi	2014-02-26
*	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-20
*	State Transaction Machine	gareuselesinge	2013-08-08
*	Modops.destr_functor without useless env	letouzey	2013-07-17
*	kernel/declarations becomes a pure mli	letouzey	2013-02-26
*	Uniformization of the "anomaly" command.	ppedrot	2013-01-28
*	Modulification of Label	ppedrot	2012-12-18
*	Monomorphization (kernel)	ppedrot	2012-11-22
*	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-09-14
*	Updating headers.	herbelin	2012-08-08
*	Module names and constant/inductive names are now in two separate namespaces	letouzey	2012-03-26
*	Noise for nothing	pboutill	2012-03-02
*	Modops: the strengthening functions can work without any env argument	letouzey	2011-05-17
*	Subtyping: align coqtop behavior concerning opaque csts on coqchk's one	letouzey	2011-04-12
*	Lazy loading of opaque proofs: fast as -dont-load-proofs without its drawbacks	letouzey	2011-04-03
*	Moving printing of module typing errors upwards to himsg.ml so as to	herbelin	2011-03-05
*	Mod_typing: some refactoring (common parts about MSEapply and co)	letouzey	2011-02-11
*	A fine-grain control of inlining at functor application via priority levels	letouzey	2011-01-31
*	Remove the "Boxed" syntaxes and the const_entry_boxed field	letouzey	2011-01-28