coq - The formal proof system

Age	Commit message (Collapse)	Author
2021-02-23	Normalize evars during bytecode compilation (fix #13841).	Guillaume Melquiond
	Otherwise, the interpreter sees already unified evars as accumulators rather than actual constants, thus preventing the computations from progressing. This was caused by 6b61b63bb8626827708024cbea1312a703a54124, which removed evar normalization. The effect went unnoticed because the computed term is still convertible to the reduced term, except that it is the lazy machinery that ends up reducing it, rather than the bytecode one. So, performances became abysmal, seemingly at random.
2021-01-04	Change the representation of kernel case.	Pierre-Marie Pédrot
	We store bound variable names instead of functions for both branches and predicate, and we furthermore add the parameters in the node. Let bindings are not taken into account and require an environment lookup for retrieval.
2020-12-09	Optimization: take advantage that we don't use arrays anymore in substitutions.	Pierre-Marie Pédrot

2020-11-13	Remove unused if-then-else construct from VM.	Guillaume Melquiond

2020-11-13	Remove unchecked arithmetic operations from VM, as they are not used.	Guillaume Melquiond

2020-08-18	Rename VM-related kernel/cfoo files to kernel/vmfoo	Gaëtan Gilbert