coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Nativecode compile_mind, compile_mind_field: remove unused arguments	Gaëtan Gilbert	2018-07-03
\|
*	More straightforward native compilation of primitive projections.	Pierre-Marie Pédrot	2018-06-05
\| \| \| \| \| \|	Instead of having a constant-based compilation of projections, we generate them at the compilation time of the inductive block to which they pertain.
*	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.
*	Update headers following #6543.	Théo Zimmermann	2018-02-27
\|
*	[native_compute] Fix handling of evars in conversion	Maxime Dénès	2018-02-05
\|
*	[api] Move structures deprecated in the API to the core.	Emilio Jesus Gallego Arias	2017-11-06
\| \| \| \|	We do up to `Term` which is the main bulk of the changes.
*	[api] Deprecate all legacy uses of Names in core.	Emilio Jesus Gallego Arias	2017-11-06
\| \| \| \|	This will allow to merge back `Names` with `API.Names`
*	Bump year in headers.	Pierre-Marie Pédrot	2017-07-04
\|
*	Update copyright headers.	Maxime Dénès	2016-01-20
\|
*	Native compiler: refactor code handling pre-computed values.	Maxime Dénès	2015-07-10
\| \| \| \|	Fixes #4139 (Not_found exception with Require in modules).
*	Make native compiler handle universe polymorphic definitions.	Maxime Dénès	2015-01-17
\| \| \| \| \|	One remaining issue: aliased constants raise an anomaly when some unsubstituted universe variables remain. VM may suffer from the same problem.
*	Update headers.	Maxime Dénès	2015-01-12
\|
*	Cleaner interfaces for linking locations of native compiler.	Maxime Dénès	2014-11-12
\| \| \| \| \| \|	Stop sharing those references across constants of the same module, which was triggering some bugs when using native_compute in interactive mode in a functor declaration.
*	Support for evars and metas in native compiler.	Maxime Dénès	2013-12-30
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Experimental. Turned out to be much harder to implement than I thought. The main issue is that the reification in the native compiler and the VM is not quite untyped. Indeed, type annotations for lambdas have to be reconstructed. Hence, when reifying an application u = t a1 ... an, the type of t has to be known or reconstructed. It is always possible to do so in plain CIC, when u is in normal form and its type is known. However, with partial terms this may no longer be the case, as in: ?1 a1 ... an. So we also compile and evaluate the type of evars and metas. This still has to be tested more extensively, but the correction of the kernel native conversion (on terms without evars or metas) should not be impacted. Much of this could be reused for the VM.
*	Removing native_name reference from constant_body.	Maxime Dénès	2013-12-28
\| \| \| \| \| \|	For now, this reference (renamed to link_info) has been moved to the environment (for constants and inductive types). But this is only a first step towards making the native compiler more functional.
*	Fixing a bug in the native compiler, introduced by r16363, leading to undefined	mdenes	2013-07-06
\| \| \| \| \| \| \|	variables in the generated code. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16619 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Native compiler: hash-consing of generated code and values.	mdenes	2013-03-25
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16363 85f007b7-540e-0410-9357-904b9bb8a0f7
*	New implementation of the conversion test, using normalization by evaluation to	mdenes	2013-01-22
	native OCaml code. Warning: the "retroknowledge" mechanism has not been ported to the native compiler, because integers and persistent arrays will ultimately be defined as primitive constructions. Until then, computation on numbers may be faster using the VM, since it takes advantage of machine integers. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16136 85f007b7-540e-0410-9357-904b9bb8a0f7