coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	[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
*	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
*	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
*	Minor module cleanup : error HigherOrderInclude was never happening	Pierre Letouzey	2015-10-25
*	Update headers.	Maxime Dénès	2015-01-12
*	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
*	Remove many superfluous 'open' indicated by ocamlc -w +33	Pierre Letouzey	2014-03-05
*	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
*	Fixing bug #2466	ppedrot	2013-02-24
*	Modulification of name	ppedrot	2012-12-18
*	Modulification of mod_bound_id	ppedrot	2012-12-18
*	Modulification of Label	ppedrot	2012-12-18
*	Modulification of identifier	ppedrot	2012-12-14
*	Updating headers.	herbelin	2012-08-08
*	remove many excessive open Util & Errors in mli's	letouzey	2012-05-29
*	Noise for nothing	pboutill	2012-03-02
*	Modops: the strengthening functions can work without any env argument	letouzey	2011-05-17
*	Moving printing of module typing errors upwards to himsg.ml so as to	herbelin	2011-03-05
*	Starting being more explicit on the reasons why module subtyping fails.	herbelin	2011-03-05
*	A fine-grain control of inlining at functor application via priority levels	letouzey	2011-01-31
*	Updated all headers for 8.3 and trunk	herbelin	2010-07-24
*	New script dev/tools/change-header to automatically update Coq files headers.	herbelin	2010-06-22
*	Remove the svn-specific $Id$ annotations	letouzey	2010-04-29
*	Move from ocamlweb to ocamdoc to generate mli documentation	pboutill	2010-04-29
*	cf. 12945	soubiran	2010-04-16
*	Include can accept both Module and Module Type	letouzey	2010-01-07
*	This big commit addresses two problems:	soubiran	2009-10-21
*	Delete trailing whitespaces in all .{v,ml} files	glondu	2009-09-17
*	Ajout des alias de module dans le noyau.	soubiran	2008-03-14
*	Attempt of fix for extraction of modules types	letouzey	2008-03-05
*	Beaoucoup de changements dans la representation interne des modules.	soubiran	2008-02-01
*	Processor integers + Print assumption (see coqdev mailing list for the	aspiwack	2007-05-11
*	Fixed the pseudo-cicularity problem due to the with operator on Module Type.	soubiran	2007-02-21
*	modifications des messages d'erreurs renvoyés lors de la comparaison	soubiran	2007-01-24
*	Inversion de l'ordre de chargement des objets logiques et non logiques	herbelin	2006-04-15