coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Merge PR #6713: Fix #6677: Critical bug with VM and universes	Maxime Dénès	2018-02-14
\|\
\| *	Fix #6677: Critical bug with VM and universes	Maxime Dénès	2018-02-12
* \|	Universe instance printer: add optional variance argument.	Gaëtan Gilbert	2018-02-11
* \|	Simplification: cumulativity information is variance information.	Gaëtan Gilbert	2018-02-10
* \|	Fix typo in Univ.CumulativityInfo	Gaëtan Gilbert	2018-02-10
\|/
*	Moving some universe substitution code out of the kernel.	Pierre-Marie Pédrot	2017-12-30
*	Returning instance instead of substitution in universe context abstraction.	Pierre-Marie Pédrot	2017-12-30
*	Proper nametab handling of global universe names	Matthieu Sozeau	2017-12-01
*	When declaring constants/inductives use ContextSet if monomorphic.	Gaëtan Gilbert	2017-11-24
*	Use type nonrec in some functor arguments.	Gaëtan Gilbert	2017-10-16
*	Do not hashcons universes beforehand.	Pierre-Marie Pédrot	2017-09-01
*	deprecate Pp.std_ppcmds type alias	Matej Košík	2017-07-27
*	The only abstraction-breaking function in Univ is now AUContext.instance.	Pierre-Marie Pédrot	2017-07-13
*	Cleaning up the implementation of module subtyping in the kernel.	Pierre-Marie Pédrot	2017-07-11
*	Less footguns in universe handling: remove subst_instance_context.	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
*	Simplify Univ.ml	Amin Timany	2017-06-16
*	Squashed commit of the following:	Amin Timany	2017-06-16
*	Check subtyping of inductive types in Kernel	Amin Timany	2017-06-16
*	Using UInfoInd for universes in inductive types	Amin Timany	2017-06-16
*	New datastructure for universes of inductive types	Amin Timany	2017-06-16
*	Drop '.' from CErrors.anomaly, insert it in args	Jason Gross	2017-06-02
*	Remove some unused values and types	Gaetan Gilbert	2017-04-27
*	Document changes	Matthieu Sozeau	2016-12-02
*	Slightly more efficient [Univ.super] implem	Matthieu Sozeau	2016-11-30
*	errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...	Pierre Letouzey	2016-07-03
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-03-30
\|\
\| *	A patch renaming equal into eq in the module dealing with	Hugo Herbelin	2016-03-22
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-21
\|\\|
\| *	Update copyright headers.	Maxime Dénès	2016-01-20
* \|	Universes algorithm : clarified comments	Jacques-Henri Jourdan	2016-01-17
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-11-29
\|\\|
\| *	Univs: entirely disallow instantiation of polymorphic constants with	Matthieu Sozeau	2015-11-27
\| *	Fix output of universe arcs. (Fix bug #4422)	Guillaume Melquiond	2015-11-23
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-11-05
\|\\|
\| *	Univs: update refman, better printers for universe contexts.	Matthieu Sozeau	2015-11-04
* \|	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 #4288, Print Sorted generated backward < constraints.	Matthieu Sozeau	2015-10-05
*	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
*	Reverting 16 last commits, committed mistakenly using the wrong push command.	Hugo Herbelin	2015-08-02
*	A patch renaming equal into eq in the module dealing with	Hugo Herbelin	2015-08-02
*	Modules: fix bug #4294	Matthieu Sozeau	2015-07-16