coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Subtyping.check_constant: remove unused module path argument.	Gaëtan Gilbert	2018-07-03
*	Merge PR #7798: Remove hack skipping comparison of algebraic universes in sub...	Matthieu Sozeau	2018-06-25
\|\
* \|	Using more general information for primitive records.	Pierre-Marie Pédrot	2018-06-23
\| *	Remove hack skipping comparison of algebraic universes in subtyping.	Gaëtan Gilbert	2018-06-22
\|/
*	Update headers following #6543.	Théo Zimmermann	2018-02-27
*	Adding a sanity check on inductive variance subtyping.	Pierre-Marie Pédrot	2018-02-15
*	[api] Also deprecate constructors of Decl_kinds.	Emilio Jesus Gallego Arias	2017-12-23
*	[api] Move structures deprecated in the API to the core.	Emilio Jesus Gallego Arias	2017-11-06
*	[api] Deprecate all legacy uses of Names in core.	Emilio Jesus Gallego Arias	2017-11-06
*	Statically enforcing that module types have no retroknowledge.	Pierre-Marie Pédrot	2017-08-29
*	Removing template polymorphism for definitions.	Pierre-Marie Pédrot	2017-07-26
*	Properly handling polymorphic inductive 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
\| *	Removing dead code in Subtyping.	Pierre-Marie Pédrot	2017-07-04
\| *	Removing a few suspicious functions from the kernel.	Pierre-Marie Pédrot	2017-07-03
\|/
*	Clean up universes of constants and inductives	Amin Timany	2017-06-16
*	Disable debug printing	Amin Timany	2017-06-16
*	Squashed commit of the following:	Amin Timany	2017-06-16
*	[cleanup] Unify all calls to the error function.	Emilio Jesus Gallego Arias	2017-05-27
*	Update various comments to use "template polymorphism"	Gaetan Gilbert	2017-04-11
*	errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...	Pierre Letouzey	2016-07-03
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-21
\|\
\| *	Update copyright headers.	Maxime Dénès	2016-01-20
* \|	Splitting kernel universe code in two modules.	Pierre-Marie Pédrot	2015-10-06
\|/
*	Univs: correct handling of with in modules	Matthieu Sozeau	2015-10-02
*	Univs: fix subtyping of polymorphic parameters.	Matthieu Sozeau	2015-10-02
*	Make native compiler handle universe polymorphic definitions.	Maxime Dénès	2015-01-17
*	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
*	Implement module subtyping for polymorphic constants (errors on	Matthieu Sozeau	2014-10-02
*	Print [Variant] types with the keyword [Variant].	Arnaud Spiwack	2014-09-04
*	Adapt universe polymorphic branch to new handling of futures for delayed proofs.	Matthieu Sozeau	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-05-06
*	Lazyconstr -> Opaqueproof	Enrico Tassi	2014-02-26
*	Declarations.mli: reorganization of modular structures	letouzey	2013-08-20
*	Robust display of NotConvertibleTypeField errors (fix #3008, #2995)	letouzey	2013-03-21
*	kernel/declarations becomes a pure mli	letouzey	2013-02-26
*	Names: shortcuts for building {kn, constant, mind} with empty sections	letouzey	2013-02-26
*	Names: Modularize constant and mutual_inductive	letouzey	2013-02-26
*	Mod_subst: misc reformulations	letouzey	2013-02-26
*	Fixing bug #2466	ppedrot	2013-02-24
*	Dir_path --> DirPath	letouzey	2013-02-19
*	Modulification of name	ppedrot	2012-12-18
*	Modulification of Label	ppedrot	2012-12-18
*	Modulification of dir_path	ppedrot	2012-12-14
*	Modulification of identifier	ppedrot	2012-12-14
*	Monomorphization (kernel)	ppedrot	2012-11-22