coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
*	Further simplification of the graph traversal in Univ.	Pierre-Marie Pédrot	2015-07-01
*	Less closures makes the GC happy.	Pierre-Marie Pédrot	2015-06-24
*	Less closures makes the GC happy.	Pierre-Marie Pédrot	2015-06-23
*	Fixing bug #4019, and checker blow-up at once.	Pierre-Marie Pédrot	2015-02-11
*	Clarifying the implementation of universe hashconsing.	Pierre-Marie Pédrot	2015-02-11
*	Fixing bug #3931.	Pierre-Marie Pédrot	2015-01-28
*	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
*	Aligning printing of universe constraints.	Hugo Herbelin	2015-01-07