coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Reduce circular dependency constants <-> projections	Gaëtan Gilbert	2018-05-31
*	Actually use the strategy information in the checker.	Pierre-Marie Pédrot	2018-01-14
*	When declaring constants/inductives use ContextSet if monomorphic.	Gaëtan Gilbert	2017-11-24
*	Fix -silent flag of coqchk after ff918e4.	Maxime Dénès	2017-09-21
*	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
*	Removing template polymorphism for definitions.	Pierre-Marie Pédrot	2017-07-26
*	Fixing the checker w.r.t. wrongly used abstract universe contexts.	Pierre-Marie Pédrot	2017-07-19
*	Clean up universes of constants and inductives	Amin Timany	2017-06-16
*	Feedback cleanup	Emilio Jesus Gallego Arias	2016-05-31
*	Checker: avoid using obsolete names from Names	Pierre Letouzey	2016-05-31
*	Univs: fix checker generating undeclared universes.	Matthieu Sozeau	2015-10-02
*	Univs: update checker	Matthieu Sozeau	2015-10-02
*	Declarations.mli refactoring: module_type_body = module_body	Pierre Letouzey	2015-01-11
*	coqchk: flush the pp buffer from time to time	Enrico Tassi	2014-12-26
*	Fix checker to handle projections with eta and universe polymorphism correctly.	Matthieu Sozeau	2014-09-06
*	Fix checking of constants in checker. Prelude can now be checked.	Matthieu Sozeau	2014-09-06
*	Adapt the checker to polymorphic universes and projections (untested).	Matthieu Sozeau	2014-05-08
*	- Fix bug preventing apply from unfolding Fixpoints.	Matthieu Sozeau	2014-05-06
*	Correct rebase on STM code. Thanks to E. Tassi for help on dealing with	Matthieu Sozeau	2014-05-06
*	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau	2014-05-06
*	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 and votour ported to new vo format (after -vi2vo)	Enrico Tassi	2014-02-26
*	Declarations.mli: reorganization of modular structures	letouzey	2013-08-20
*	Checker: empty sections hardcoded in cb and mind	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
*	Names: shortcuts for building {kn, constant, mind} with empty sections	letouzey	2013-02-26
*	Dir_path --> DirPath	letouzey	2013-02-19
*	make validate repaired via a temporary fix for #2949	letouzey	2013-02-13
*	Modulification of Label	ppedrot	2012-12-18
*	Modulification of dir_path	ppedrot	2012-12-14
*	still some more dead code removal	letouzey	2012-10-06
*	Getting rid of Pp.msgnl and Pp.message.	ppedrot	2012-06-01
*	Module names and constant/inductive names are now in two separate namespaces	letouzey	2012-03-26
*	Univ: enforce_leq instead of enforce_geq for more uniformity	letouzey	2012-03-22
*	Noise for nothing	pboutill	2012-03-02
*	Checker/subtyping.ml: avoid adding in env a module already there (fix #2609)	letouzey	2011-10-26
*	ported r14149 from v8.3 branch: bug in checker (redefined global)	barras	2011-05-23
*	Modops: the strengthening functions can work without any env argument	letouzey	2011-05-17
*	Subtyping: align coqtop behavior concerning opaque csts on coqchk's one	letouzey	2011-04-12
*	Lazy loading of opaque proofs: fast as -dont-load-proofs without its drawbacks	letouzey	2011-04-03
*	Univ.constraints made fully abstract instead of being a Set of abstract stuff	letouzey	2010-12-18
*	Checker: remove some dead code	letouzey	2010-09-24
*	Sharing is not anymore broken by traverse_module.	soubiran	2010-09-15
*	After the approval of Bruno, here the patch for the checker.	soubiran	2010-04-29
*	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