coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Merge PR #6728: Extrude monomorphic universe contexts from with Definition co...	Maxime Dénès	2018-02-19
\|\
\| *	Extrude monomorphic universe contexts from with Definition constraints.	Pierre-Marie Pédrot	2018-02-16
* \|	Factorize the relocations in the on-disk VM representation.	Pierre-Marie Pédrot	2018-02-14
* \|	Use a more compact representation for bytecode relocations stored on disk.	Pierre-Marie Pédrot	2018-02-14
* \|	Do not use global variables for VM bytecode compilation in Cemitcodes.	Pierre-Marie Pédrot	2018-02-14
* \|	Remove the unsafe bytes conversion function in Cemitcodes.	Pierre-Marie Pédrot	2018-02-14
* \|	Move the call to the computation of bytecode inside Cemitcodes.	Pierre-Marie Pédrot	2018-02-14
* \|	Abstract further the type of VM bytecode compilation.	Pierre-Marie Pédrot	2018-02-14
\|/
*	Merge PR #6713: Fix #6677: Critical bug with VM and universes	Maxime Dénès	2018-02-14
\|\
* \	Merge PR #6702: [vernac] [minor] Move print effects to top-level caller.	Maxime Dénès	2018-02-13
\|\ \
* \ \	Merge PR #1082: Fixing Print for inductive types with let-in in parameters	Maxime Dénès	2018-02-12
\|\ \ \
* \ \ \	Merge PR #6128: Simplification: cumulativity information is variance informa...	Maxime Dénès	2018-02-12
\|\ \ \ \
* \ \ \ \	Merge PR #6729: [nativecomp] Remove ad-hoc handling of Dynlink exception.	Maxime Dénès	2018-02-12
\|\ \ \ \ \
* \ \ \ \ \	Merge PR #6674: Delay computation of lifts in the reduction machine.	Maxime Dénès	2018-02-12
\|\ \ \ \ \ \
\| \| \| \| \| \| *	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
\| \| \| * \| \|	Use specialized function for inductive subtyping inference.	Gaëtan Gilbert	2018-02-11
\| \| \| * \| \|	Simplification: cumulativity information is variance information.	Gaëtan Gilbert	2018-02-10
\| \| \| * \| \|	[get_cumulativity_constraints] allowing further code sharing.	Gaëtan Gilbert	2018-02-10
\| \| \| * \| \|	Factorize code for comparing maybe-cumulative inductives.	Gaëtan Gilbert	2018-02-10
\| \| \| * \| \|	Fix typo in Univ.CumulativityInfo	Gaëtan Gilbert	2018-02-10
\| \|_\|/ / / \|/\| \| \| \|
\| \| \| \| *	[nit] Remove some unnecessary global `open Feedback`	Emilio Jesus Gallego Arias	2018-02-09
\| \| \| \|/ \| \| \|/\|
\| \| * \|	[nativecomp] Remove ad-hoc handling of Dynlink exception.	Emilio Jesus Gallego Arias	2018-02-09
\| \|/ / \|/\| \|
* \| \|	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
\| \| \| * \|	Delay computation of lifts in the reduction machine.	Pierre-Marie Pédrot	2018-02-04
\| \|_\|/ / \|/\| \| \|
\| * \| \|	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
\|/ /