coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	[VM] Remove projection names from structured constants.	Maxime Dénès	2018-06-10
\| \| \| \| \| \| \|	It was actually a hack since those names are never used to represent values, only to be passed as arguments to bytecode instructions. So instead of reusing the structured_constant type, we follow the same pattern as switch annotations.
*	Moving the VM global atom table to a ML reference.	Pierre-Marie Pédrot	2018-03-26
\|
*	Moving the VM global data to a ML reference.	Pierre-Marie Pédrot	2018-03-26
\|
*	Merge PR #6855: Update headers following #6543.	Maxime Dénès	2018-03-05
\|\
* \	Merge PR #935: Handling evars in the VM	Maxime Dénès	2018-03-04
\|\ \
\| * \|	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.
* \| \|	[VM] Unify Const_sorts and Const_type, and remove Vsort.	Maxime Dénès	2018-03-02
\|/ / \| \| \| \| \| \| \| \|	This simplifies the representation of values, and brings it closer to the ones of the native compiler.
\| *	Update headers following #6543.	Théo Zimmermann	2018-02-27
\|/
*	Safer VM interfaces	Maxime Dénès	2018-01-26
	We separate functions dealing with VM values (vmvalues.ml) and interfaces of the bytecode interpreter (vm.ml). Only the former relies on untyped constructions. This also makes the VM architecture closer to the one of native_compute, another patch could probably try to share more code between the two for conversion and reification (not trivial, though). This is also preliminary work for integers and arrays.