coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	[env.env_rel_context.env_rel_ctx] -> [rel_context env]	Gaëtan Gilbert	2018-06-28
\| \| \| \|	It's a bit shorter and more direct.
*	Reduce circular dependency constants <-> projections	Gaëtan Gilbert	2018-05-31
\| \| \| \| \|	Instead of having the projection data in the constant data we have it independently in the environment.
*	Fix #7333: vm_compute segfaults / Anomaly with cofix	Maxime Dénès	2018-05-28
\| \| \| \| \|	We eta-expand cofixpoints when needed, so that their call-by-need evaluation is correctly implemented by VM and native_compute.
*	Unify pre_env and env	Maxime Dénès	2018-05-28
\| \| \| \| \|	We now have only two notions of environments in the kernel: env and safe_env.
*	Collecting Array.smart_* functions into a module Array.Smart.	Hugo Herbelin	2018-05-23
\|
*	[lib] Move global options to their proper place.	Emilio Jesus Gallego Arias	2018-04-02
\| \| \| \| \| \| \| \|	Recent commits introduced global flags, but these should be module-specific so relocating. Global flags are deprecated, and for 8.9 `Lib.Flags` will be reduced to the truly global stuff.
*	Handling evars in the VM.	Pierre-Marie Pédrot	2018-03-03
\| \| \| \| \| \| \|	We simply treat them as as an application of an atom to its instance, and in the decompilation phase we reconstruct the instance from the stack. This grants wish BZ#5659.
*	New IR in VM: Clambda.	Maxime Dénès	2018-02-23
	This intermediate representation serves two purposes: 1- It is a preliminary step for primitive machine integers, as iterators will be compiled to Clambda. 2- It makes the VM compilation passes closer to the ones of native_compute. Once we unifiy the representation of values, we should be able to factorize the lambda-code generation between the two compilers, as well as the reification code. This code was written by Benjamin Grégoire and myself.