index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
kernel
/
nativevalues.mli
Age
Commit message (
Expand
)
Author
2019-02-04
Primitive integers
Maxime Dénès
2018-07-26
Fix #8121: anomalies in native_compute with let and evars.
Pierre-Marie Pédrot
2018-07-13
Generate type-specific code for is_accu in native compilation of fixpoints.
Pierre-Marie Pédrot
2018-06-05
More straightforward native compilation of primitive projections.
Pierre-Marie Pédrot
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
2018-02-05
[native_compute] Remove useless conversion to list in reification.
Maxime Dénès
2017-11-06
[api] Move structures deprecated in the API to the core.
Emilio Jesus Gallego Arias
2017-11-06
[api] Deprecate all legacy uses of Names in core.
Emilio Jesus Gallego Arias
2017-11-04
[api] Deprecate all legacy uses of Name.Id in core.
Emilio Jesus Gallego Arias
2017-07-04
Bump year in headers.
Pierre-Marie Pédrot
2016-01-20
Update copyright headers.
Maxime Dénès
2015-01-17
Make native compiler handle universe polymorphic definitions.
Maxime Dénès
2015-01-12
Update headers.
Maxime Dénès
2014-05-06
This commit adds full universe polymorphism and fast projections to Coq.
Matthieu Sozeau
2014-04-09
Fix name of some Int31 operations in native compiler.
Maxime Dénès
2014-04-09
Machine arithmetic operations for native compiler.
Maxime Dénès
2014-04-09
Full support for int31 values in native compiler.
Maxime Dénès
2014-04-09
Partial support for open terms in int31.
Maxime Dénès
2013-12-30
Support for evars and metas in native compiler.
Maxime Dénès
2013-03-25
Native compiler: hash-consing of generated code and values.
mdenes
2013-01-22
New implementation of the conversion test, using normalization by evaluation to
mdenes
