coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Merge PR #6685: Use whd-all on rigid-flex conversion.	Maxime Dénès	2018-02-07
\|\
* \	Merge PR #6686: Kernel/checker reduction cleanups around projection unfolding	Maxime Dénès	2018-02-07
\|\ \
\| \| *	Respect the transparent state of the current conversion on strong weak-head.	Pierre-Marie Pédrot	2018-02-05
* \| \|	[native_compute] Fix handling of evars in conversion	Maxime Dénès	2018-02-05
* \| \|	[native_compute] Remove useless conversion to list in reification.	Maxime Dénès	2018-02-05
\| * \|	CClosure.unfold_projection: don't catch Not_found, assume env is ok	Gaëtan Gilbert	2018-02-02
\| * \|	kernel: cleanup projection unfolding	Gaëtan Gilbert	2018-02-02
\|/ /
\| *	Use whd-all on rigid-flex conversion.	Pierre-Marie Pédrot	2018-02-02
\|/
*	Merge PR #6666: Fix reduction of primitive projections on coinductive records...	Maxime Dénès	2018-01-30
\|\
* \	Merge PR #6649: Fix #6621: Anomaly on fixpoint with primitive projections	Maxime Dénès	2018-01-30
\|\ \
\| \| *	[native_compute] Fix evaluation of cofixpoints under primitive projections.	Maxime Dénès	2018-01-29
* \| \|	Safer VM interfaces	Maxime Dénès	2018-01-26
\| \|/ \|/\|
\| *	Fix #6621: Anomaly on fixpoint with primitive projections	Maxime Dénès	2018-01-24
\|/
*	Merge PR #6627: Fix #6619: coqchk does not reduce compatibility constants for...	Maxime Dénès	2018-01-23
\|\
* \	Merge PR #6506: Fast rel lookup	Maxime Dénès	2018-01-22
\|\ \
\| \| *	Remove dead code in Environ.	Pierre-Marie Pédrot	2018-01-20
\| \|/ \|/\|
* \|	Store the conversion oracle in constant and inductive definitions.	Pierre-Marie Pédrot	2018-01-14
* \|	Merge PR #6578: Remove references to deleted Unicode.Unsupported exception	Maxime Dénès	2018-01-13
\|\ \
* \| \|	Enforce that polymorphic definitions do not generate internal constraints.	Pierre-Marie Pédrot	2018-01-11
\| * \|	Remove references to removed Unicode.Unsupported	Jasper Hugunin	2018-01-11
\|/ /
* \|	Add a comment about universe lifting in sections in the kernel.	Pierre-Marie Pédrot	2017-12-31
* \|	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
* \|	Hardening universe abstraction in Cooking.	Pierre-Marie Pédrot	2017-12-30
\| *	Share the rel environment between Environ.env and reduction cache.	Pierre-Marie Pédrot	2017-12-29
\| *	Fast environment lookup for rels.	Pierre-Marie Pédrot	2017-12-29
\|/
*	[api] Also deprecate constructors of Decl_kinds.	Emilio Jesus Gallego Arias	2017-12-23
*	Merge PR #6469: No universe constraints in Let definitions	Maxime Dénès	2017-12-22
\|\
* \	Merge PR #6449: Let definitions must not contain side-effects when reaching t...	Maxime Dénès	2017-12-20
\|\ \
\| \| *	Let definitions do not create new universe constraints.	Pierre-Marie Pédrot	2017-12-19
\| \| *	Specific type for section definition entries.	Pierre-Marie Pédrot	2017-12-19
\| \|/
* \|	Fix order of let-in representation comment.	Jasper Hugunin	2017-12-19
\| *	Let definitions must not contain side-effects when reaching the kernel.	Pierre-Marie Pédrot	2017-12-16
\|/
*	Merge PR #6264: [kernel] Patch allowing to disable VM reduction.	Maxime Dénès	2017-12-14
\|\
* \	Merge PR #6038: [build] Remove coqmktop in favor of ocamlfind.	Maxime Dénès	2017-12-14
\|\ \
* \ \	Merge PR #6368: [api] Remove yet another type alias.	Maxime Dénès	2017-12-11
\|\ \ \
* \| \| \|	[api] Remove kernel dependency on intf (Decl_kind)	Emilio Jesus Gallego Arias	2017-12-10
\| * \| \|	[api] Remove yet another type alias.	Emilio Jesus Gallego Arias	2017-12-09
\|/ / /
\| * /	[lib] Rename Profile to CProfile	Emilio Jesus Gallego Arias	2017-12-09
\|/ /
\| *	[kernel] Patch allowing to disable VM reduction.	Emilio Jesus Gallego Arias	2017-12-02
* \|	Proper nametab handling of global universe names	Matthieu Sozeau	2017-12-01
\|/
*	Fix native compute for byte compiled Coq.	Gaëtan Gilbert	2017-11-28
*	Merge PR #1033: Universe binder improvements	Maxime Dénès	2017-11-28
\|\
* \|	[api] Remove aliases of `Evar.t`	Emilio Jesus Gallego Arias	2017-11-26
\| *	When declaring constants/inductives use ContextSet if monomorphic.	Gaëtan Gilbert	2017-11-24
\|/
*	Merge PR #486: Make some functions on terms more robust w.r.t new term constr...	Maxime Dénès	2017-11-24
\|\
\| *	Make some functions on terms more robust w.r.t new term constructs.	Maxime Dénès	2017-11-23
* \|	[api] Deprecate Term destructors, move to Constr	Emilio Jesus Gallego Arias	2017-11-22
* \|	[api] Miscellaneous consolidation + moves to engine.	Emilio Jesus Gallego Arias	2017-11-21
\|/
*	Merge PR #6058: Remove redundant env argument to Reduction.ccnv	Maxime Dénès	2017-11-15
\|\