coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
*	Moving Utils.list_* to a proper CList module, which includes stdlib	ppedrot	2012-09-14
*	This patch removes unused "open" (automatically generated from	regisgia	2012-09-14
*	Updating headers.	herbelin	2012-08-08
*	Noise for nothing	pboutill	2012-03-02
*	Mod_subst: some simplifications, some more significant names to functions, etc	letouzey	2011-10-26
*	Various simplifications about constant_of_delta and mind_of_delta	letouzey	2011-10-11
*	Modops: the strengthening functions can work without any env argument	letouzey	2011-05-17
*	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