coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
*	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
*	Remove the "Boxed" syntaxes and the const_entry_boxed field	letouzey	2011-01-28
*	Minor fixes from Gregory Malecha. A typo fixed and a better (located)	msozeau	2010-11-15
*	Updated all headers for 8.3 and trunk	herbelin	2010-07-24
*	Added a few informations about file lineages (for the most part in kernel)	herbelin	2010-05-09
*	Remove the svn-specific $Id$ annotations	letouzey	2010-04-29
*	cf. 12945	soubiran	2010-04-16
*	fix commit 12706 + comments.	soubiran	2010-02-03
*	Small fix on module inclusion.	soubiran	2010-02-02
*	Include can accept both Module and Module Type	letouzey	2010-01-07
*	The following script was rasing an error	soubiran	2010-01-04
*	the inlining computation at functor application was raising not_found when th...	soubiran	2009-11-13
*	First debug... the renaming of librairies was not working and auto/dn were no...	soubiran	2009-10-23
*	This big commit addresses two problems:	soubiran	2009-10-21
*	Delete trailing whitespaces in all .{v,ml} files	glondu	2009-09-17
*	Correction bug 2134.	soubiran	2009-07-09