coq - The formal proof system

Age	Commit message (Collapse)	Author
2018-06-28	[env.env_rel_context.env_rel_ctx] -> [rel_context env]	Gaëtan Gilbert
	It's a bit shorter and more direct.
2018-05-31	Reduce circular dependency constants <-> projections	Gaëtan Gilbert
	Instead of having the projection data in the constant data we have it independently in the environment.
2018-05-28	Fix #7333: vm_compute segfaults / Anomaly with cofix	Maxime Dénès
	We eta-expand cofixpoints when needed, so that their call-by-need evaluation is correctly implemented by VM and native_compute.
2018-05-28	Unify pre_env and env	Maxime Dénès
	We now have only two notions of environments in the kernel: env and safe_env.
2018-05-23	Collecting Array.smart_* functions into a module Array.Smart.	Hugo Herbelin

2018-04-02	[lib] Move global options to their proper place.	Emilio Jesus Gallego Arias
	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.
2018-03-03	Handling evars in the VM.	Pierre-Marie Pédrot
	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.
2018-02-23	New IR in VM: Clambda.	Maxime Dénès
	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.