coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	[cleanup] Unify all calls to the error function.	Emilio Jesus Gallego Arias	2017-05-27
*	Merge PR #244.	Pierre-Marie Pédrot	2016-09-08
\|\
\| *	Make the user_err header an optional parameter.	Emilio Jesus Gallego Arias	2016-08-19
\| *	Remove errorlabstrm in favor of user_err	Emilio Jesus Gallego Arias	2016-08-19
\|/
*	errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...	Pierre Letouzey	2016-07-03
*	Fixing the checker.	Pierre-Marie Pédrot	2016-06-18
*	Feedback cleanup	Emilio Jesus Gallego Arias	2016-05-31
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-21
\|\
\| *	Update copyright headers.	Maxime Dénès	2016-01-20
* \|	Do not compose "str" and "to_string" whenever possible.	Guillaume Melquiond	2015-12-22
\|/
*	Checker was forgetting to register global universes introduced by opaque	Matthieu Sozeau	2015-11-04
*	Univs: update checker	Matthieu Sozeau	2015-10-02
*	Option -type-in-type: added support in checker and making it contaminating	Hugo Herbelin	2015-07-10
*	coqchk: more prints when -debug	Enrico Tassi	2015-03-23
*	Update headers.	Maxime Dénès	2015-01-12
*	vi2vo: universes handling finally fixed	Enrico Tassi	2014-03-11
*	Remove many superfluous 'open' indicated by ocamlc -w +33	Pierre Letouzey	2014-03-05
*	Checker: vo validation is now done in check.ml (and always)	letouzey	2013-04-15
*	Checker: reified encoding of .vo types in values.ml	letouzey	2013-04-15
*	Checker: regroup all vo-related types in cic.mli	letouzey	2013-04-15
*	Revised infrastructure for lazy loading of opaque proofs	letouzey	2013-04-02
*	Safe_typing+Libary: use some arrays instead of lists in vo structures	letouzey	2013-03-28
*	Dir_path --> DirPath	letouzey	2013-02-19
*	Modulification of dir_path	ppedrot	2012-12-14
*	Updating headers.	herbelin	2012-08-08
*	Getting rid of Pp.msgnl and Pp.message.	ppedrot	2012-06-01
*	Noise for nothing	pboutill	2012-03-02
*	Lazy loading of opaque proofs: fast as -dont-load-proofs without its drawbacks	letouzey	2011-04-03
*	Checker: remove some dead code	letouzey	2010-09-24
*	Explicit Mod_checking signature	glondu	2010-09-16
*	Sharing is not anymore broken by traverse_module.	soubiran	2010-09-15
*	* checker/Safe_typing.LightenLibrary:	regisgia	2010-08-27
*	* (checker\|kernel)/Safe_typing:	regisgia	2010-08-27
*	* (checker\|kernel)/Safe_typing:	regisgia	2010-08-27
*	* checker/SafeTyping kernel/SafeTyping:	regisgia	2010-08-27
*	* Improve documentation of LightenLibrary.	regisgia	2010-08-27
*	* (checker\|kernel)/Safe_typing: New LightenLibrary.	regisgia	2010-08-27
*	adpated the checker to handle coomutative cuts and lazyness	barras	2010-07-30
*	Updated all headers for 8.3 and trunk	herbelin	2010-07-24
*	Remove the svn-specific $Id$ annotations	letouzey	2010-04-29
*	kills a warning about vo in checker/safe_typing	letouzey	2010-03-18
*	[checker] fixed vo validation problems, module incompatibilities remain	barras	2010-02-19
*	This big commit addresses two problems:	soubiran	2009-10-21
*	Delete trailing whitespaces in all .{v,ml} files	glondu	2009-09-17
*	porting r11900 11905 and 11953 to trunk	barras	2009-03-02
*	fixed bug #1927 + univ constraints (module cstrs include cstrs of its subcomp...	barras	2008-09-02
*	doc of coqchk + improved module cache and computation of module sets	barras	2008-05-23
*	checker deals with polymorphic constants and module aliases	barras	2008-05-06
*	added the .vo checker (with independent Makefile)	barras	2008-04-21