coq - The formal proof system

Age	Commit message (Collapse)	Author
2019-05-19	Parameterize the constant_body type by opaque subproofs.	Pierre-Marie Pédrot

2018-07-03	Nativecode compile_mind, compile_mind_field: remove unused arguments	Gaëtan Gilbert

2018-06-05	More straightforward native compilation of primitive projections.	Pierre-Marie Pédrot
	Instead of having a constant-based compilation of projections, we generate them at the compilation time of the inductive block to which they pertain.
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-02-27	Update headers following #6543.	Théo Zimmermann

2018-02-05	[native_compute] Fix handling of evars in conversion	Maxime Dénès

2017-11-06	[api] Move structures deprecated in the API to the core.	Emilio Jesus Gallego Arias
	We do up to `Term` which is the main bulk of the changes.
2017-11-06	[api] Deprecate all legacy uses of Names in core.	Emilio Jesus Gallego Arias
	This will allow to merge back `Names` with `API.Names`
2017-07-04	Bump year in headers.	Pierre-Marie Pédrot

2016-01-20	Update copyright headers.	Maxime Dénès

2015-07-10	Native compiler: refactor code handling pre-computed values.	Maxime Dénès
	Fixes #4139 (Not_found exception with Require in modules).
2015-01-17	Make native compiler handle universe polymorphic definitions.	Maxime Dénès
	One remaining issue: aliased constants raise an anomaly when some unsubstituted universe variables remain. VM may suffer from the same problem.
2015-01-12	Update headers.	Maxime Dénès

2014-11-12	Cleaner interfaces for linking locations of native compiler.	Maxime Dénès
	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.
2013-12-30	Support for evars and metas in native compiler.	Maxime Dénès
	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.
2013-12-28	Removing native_name reference from constant_body.	Maxime Dénès
	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.
2013-07-06	Fixing a bug in the native compiler, introduced by r16363, leading to undefined	mdenes
	variables in the generated code. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16619 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-25	Native compiler: hash-consing of generated code and values.	mdenes
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16363 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-01-22	New implementation of the conversion test, using normalization by evaluation to	mdenes
	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