coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Remove hack skipping comparison of algebraic universes in subtyping.	Gaëtan Gilbert	2018-06-22
*	Fix Univ.enforce_leq dropped constraints when algebraic on the right	Gaëtan Gilbert	2018-06-19
*	Collecting List.smart_* functions into a module List.Smart.	Hugo Herbelin	2018-05-23
*	Collecting Array.smart_* functions into a module Array.Smart.	Hugo Herbelin	2018-05-23
*	Always print explanation for univ inconsistency, rm Flags.univ_print	Gaëtan Gilbert	2018-04-26
*	Fix #6956: Uncaught exception in bytecode compilation	Maxime Dénès	2018-04-06
*	Cumulativity: improve treatment of irrelevant universes.	Gaëtan Gilbert	2018-03-09
*	Update headers following #6543.	Théo Zimmermann	2018-02-27
*	Adding a sanity check on inductive variance subtyping.	Pierre-Marie Pédrot	2018-02-15
*	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