coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-21
\|\
\| *	Update copyright headers.	Maxime Dénès	2016-01-20
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-29
\|\\|
\| *	Adds support for the virtual machine to perform reduction of universe polymor...	Gregory Malecha	2015-10-28
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-09
\|\\|
\| *	Univs: fix bug #3807	Matthieu Sozeau	2015-10-08
* \|	Splitting kernel universe code in two modules.	Pierre-Marie Pédrot	2015-10-06
\|/
*	Univs: fix bug #4251, handling of template polymorphic constants.	Matthieu Sozeau	2015-10-02
*	Univs (kernel) adapt to new invariants	Matthieu Sozeau	2015-10-02
*	Forcing i > Set for global universes (incomplete)	Matthieu Sozeau	2015-10-02
*	Universes: enforce Set <= i for all Type occurrences.	Matthieu Sozeau	2015-10-02
*	Univs: proper printing of global and local universe names (only	Matthieu Sozeau	2015-01-17
*	Make native compiler handle universe polymorphic definitions.	Maxime Dénès	2015-01-17
*	Correct restriction of vm_compute when handling universe polymorphic	Matthieu Sozeau	2015-01-15
*	Update headers.	Maxime Dénès	2015-01-12
*	Implement module subtyping for polymorphic constants (errors on	Matthieu Sozeau	2014-10-02
*	Simplify even further the declaration of primitive projections,	Matthieu Sozeau	2014-08-30
*	Adding a primitive to merge ContextSets which is more efficient when one	Pierre-Marie Pédrot	2014-08-09
*	Cleaning up interface of ContextSet.	Pierre-Marie Pédrot	2014-08-09
*	Move to a representation of universe polymorphic constants using indices for ...	Matthieu Sozeau	2014-08-03
*	Useless export of Instance.eqeq. We hashcons everything before calling this	Pierre-Marie Pédrot	2014-07-31
*	Universe level maps use HMaps.	Pierre-Marie Pédrot	2014-07-21
*	Cleanup substitution inside universe instances, only done through subst_fn now,	Matthieu Sozeau	2014-07-21
*	Cleanup code related to the constraint solving, which sits now outside the	Matthieu Sozeau	2014-07-03
*	Add toplevel commands to declare global universes and constraints.	Matthieu Sozeau	2014-07-01
*	Code factorization in LMap.	Pierre-Marie Pédrot	2014-06-18
*	Made explanations for universe inconsistencies optional. They are only used	Pierre-Marie Pédrot	2014-06-10
*	- Fix substitution of universes which needlessly hashconsed existing universes.	Matthieu Sozeau	2014-06-10
*	More cleanup/reorganizing of univ.ml to separate constraint/universe handling...	Matthieu Sozeau	2014-06-10
*	Cleanup in Univ, moving code for UniverseConstraints outside the kernel in Un...	Matthieu Sozeau	2014-06-10
*	Remove unused function in univ	Matthieu Sozeau	2014-06-10
*	Function in Univ uselessly exported.	Pierre-Marie Pédrot	2014-06-08
*	- Force every universe level to be >= Prop, so one cannot "go under" it anymore.	Matthieu Sozeau	2014-06-04
*	- Fix hashing of levels to get the "right" order in universe contexts etc...	Matthieu Sozeau	2014-06-04
*	Find a more efficient fix for dealing with template universes:	Matthieu Sozeau	2014-05-06
*	- Fix bug preventing apply from unfolding Fixpoints.	Matthieu Sozeau	2014-05-06
*	- Fix handling of polymorphic inductive elimination schemes.	Matthieu Sozeau	2014-05-06
*	- Rename eq to equal in Univ, document new modules, set interfaces.	Matthieu Sozeau	2014-05-06
*	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau	2014-05-06
*	Fixing Pervasives.equality in extraction.	Pierre-Marie Pédrot	2014-03-03
*	Specializing hash functions for widely used types.	ppedrot	2013-10-24
*	Universe counters on slaves are in sync with master	gareuselesinge	2013-08-20
*	A version of Univ.check_eq with no anomaly for Evd.set_eq_sort	letouzey	2013-03-12
*	Dir_path --> DirPath	letouzey	2013-02-19
*	Modulification of dir_path	ppedrot	2012-12-14
*	Small cleaning of interface in Univ	ppedrot	2012-11-26
*	univ inconsistency error message gives evidence of a cycle	barras	2012-10-17
*	Updating headers.	herbelin	2012-08-08
*	Univ: enforce_leq instead of enforce_geq for more uniformity	letouzey	2012-03-22
*	Univ: a univ_depends function to avoid a hack in Inductiveops	letouzey	2012-03-01