coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	[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
*	Separating the module_type and module_body types by using a type parameter.	Pierre-Marie Pédrot	2017-08-29
*	Properly handling polymorphic inductive subtyping in the kernel.	Pierre-Marie Pédrot	2017-07-11
*	Bump year in headers.	Pierre-Marie Pédrot	2017-07-04
*	Clean up universes of constants and inductives	Amin Timany	2017-06-16
*	Drop '.' from CErrors.anomaly, insert it in args	Jason Gross	2017-06-02
*	errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...	Pierre Letouzey	2016-07-03
*	Update copyright headers.	Maxime Dénès	2016-01-20
*	Inclusion of functors with restricted signature is now forbidden (fix #3746)	Pierre Letouzey	2015-12-22
*	Adds support for the virtual machine to perform reduction of universe polymor...	Gregory Malecha	2015-10-28
*	Minor module cleanup : error HigherOrderInclude was never happening	Pierre Letouzey	2015-10-25
*	Univs: uncovered bug in strengthening of opaque polymorphic definitions.	Matthieu Sozeau	2015-10-02
*	Fix vm compiler to refuse to compile code making use of inductives with	Matthieu Sozeau	2015-03-25
*	More sharing in module substitution.	Pierre-Marie Pédrot	2015-03-18
*	Univs: fix bug #3978: carry around the universe context used to	Matthieu Sozeau	2015-02-12
*	Correct restriction of vm_compute when handling universe polymorphic	Matthieu Sozeau	2015-01-15
*	Update headers.	Maxime Dénès	2015-01-12
*	Declarations.mli refactoring: module_type_body = module_body	Pierre Letouzey	2015-01-11
*	Fix bug #3804.	Matthieu Sozeau	2014-11-21
*	Cleaner interfaces for linking locations of native compiler.	Maxime Dénès	2014-11-12
*	selective join/export of the safe_environment	Enrico Tassi	2014-10-13
*	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
*	Adapt Y. Bertot's path on private inductives (now the keyword is "Private").	Yves Bertot	2014-05-06
*	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau	2014-05-06
*	Changing Retrokwnoledge entry type from kind_of_term to constr. It seems it had	Pierre-Marie Pédrot	2014-03-14
*	Remove many superfluous 'open' indicated by ocamlc -w +33	Pierre Letouzey	2014-03-05
*	Lazyconstr -> Opaqueproof	Enrico Tassi	2014-02-26
*	Removing native_name reference from constant_body.	Maxime Dénès	2013-12-28
*	Future: ported to Ephemeron + exception enhancing	gareuselesinge	2013-10-18
*	Declarations.mli: reorganization of modular structures	letouzey	2013-08-20
*	Declareops + Modops : more clever substitutions	letouzey	2013-08-20
*	Safe_typing code refactoring	letouzey	2013-08-20
*	enhance marshallable option for freeze (minor TODO in safe_typing)	gareuselesinge	2013-08-08
*	State Transaction Machine	gareuselesinge	2013-08-08
*	Modops.destr_functor without useless env	letouzey	2013-07-17
*	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
*	Fixing bug #2466	ppedrot	2013-02-24
*	Dir_path --> DirPath	letouzey	2013-02-19
*	Uniformization of the "anomaly" command.	ppedrot	2013-01-28
*	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
*	More monomorphizations	ppedrot	2012-11-13
*	Remove some more "open" and dead code thanks to OCaml4 warnings	letouzey	2012-10-02
*	Partial revert of Yann commit in order to use CLib.List when opening	ppedrot	2012-09-14