coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
*	Dead code in Univ.	Pierre-Marie Pédrot	2014-12-21
*	Cleaning up universe list implementation in Univ.	Pierre-Marie Pédrot	2014-12-18
*	Ensuring the good invariants of hashcons table generation in the API.	Pierre-Marie Pédrot	2014-12-17
*	Fix merging of name maps in union of universe contexts.	Matthieu Sozeau	2014-12-14
*	Implement module subtyping for polymorphic constants (errors on	Matthieu Sozeau	2014-10-02
*	Clean a bit of univ.ml, add credits.	Matthieu Sozeau	2014-09-18
*	Fix checker treatment of inductives using subst_instances instead of subst_un...	Matthieu Sozeau	2014-09-05
*	Fix bug #3559, ensuring a canonical order of universe level quantifications when	Matthieu Sozeau	2014-09-04
*	Simplify even further the declaration of primitive projections,	Matthieu Sozeau	2014-08-30
*	Fix pretty-printing of the graph in Print Sorted Universes. Type.0 was larger...	Matthieu Sozeau	2014-08-18
*	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
*	Fixing semantics of Univ.Level.equal.	Pierre-Marie Pédrot	2014-08-04