index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
kernel
/
cClosure.mli
Age
Commit message (
Expand
)
Author
2020-07-06
Primitive persistent arrays
Maxime Dénès
2020-07-01
UIP in SProp
Gaëtan Gilbert
2020-04-03
Be cleverer and do not hopelessly rezip a term when not needed.
Pierre-Marie Pédrot
2020-03-18
Update headers in the whole code base.
Théo Zimmermann
2019-11-01
Add primitive float computation in Coq kernel
Guillaume Bertholon
2019-07-16
Move unfold_side_flags CClosure -> Tacred internals
Gaëtan Gilbert
2019-06-17
Update ml-style headers to new year.
Théo Zimmermann
2019-05-23
Fixing typos - Part 2
JPR
2019-05-19
Make the type of constant bodies parametric on opaque proofs.
Pierre-Marie Pédrot
2019-03-14
mutable relevance marks in fconstr
Gaëtan Gilbert
2019-03-14
Add relevance marks on binders.
Gaëtan Gilbert
2019-02-04
Primitive integers
Maxime Dénès
2018-12-23
Remove dead code from CClosure.
Pierre-Marie Pédrot
2018-11-20
Use a closure for the domain argument of FProd.
Pierre-Marie Pédrot
2018-11-20
Do not wrap FProd return types in a closure.
Pierre-Marie Pédrot
2018-11-19
Rename TranspState into TransparentState.
Pierre-Marie Pédrot
2018-11-19
Proper record type and accessors for transparent states.
Pierre-Marie Pédrot
2018-11-19
Move transparent_state to its own module.
Pierre-Marie Pédrot
2018-10-11
Clean up CClosure code.
Pierre-Marie Pédrot
2018-10-11
The cbv reduction does not rely on the kernel info data structure anymore.
Pierre-Marie Pédrot
2018-10-04
Remove FCast from CClosure.fterm.
Pierre-Marie Pédrot
2018-07-26
Turn the kernel reduction sharing flag into an argument passed in the cache.
Pierre-Marie Pédrot
2018-07-24
Projections use index representation
Gaëtan Gilbert
2018-06-17
Faster and cleaner fconstr-to-constr conversion function.
Pierre-Marie Pédrot
2018-05-21
Simplify the newring hack.
Pierre-Marie Pédrot
2018-03-28
[api] Deprecate a couple of aliases that we missed.
Emilio Jesus Gallego Arias
2018-03-09
Merge PR #6769: Split closure cache and remove whd_both
Maxime Dénès
2018-03-05
Replace invalid tag @raises in ocamldoc comments with @raise
mrmr1993
2018-03-04
Pass the constant cache as a separate argument in kernel reduction.
Pierre-Marie Pédrot
2018-02-27
Update headers following #6543.
Théo Zimmermann
2018-02-07
Merge PR #6685: Use whd-all on rigid-flex conversion.
Maxime Dénès
2018-02-05
Respect the transparent state of the current conversion on strong weak-head.
Pierre-Marie Pédrot
2018-02-02
kernel: cleanup projection unfolding
Gaëtan Gilbert
2017-11-26
[api] Remove aliases of `Evar.t`
Emilio Jesus Gallego Arias
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-07-04
Bump year in headers.
Pierre-Marie Pédrot
2017-06-04
Added support for a side effect on constants in reduction functions.
Thomas Sibut-Pinote
2016-07-03
closure.ml renamed into cClosure.ml (avoid clash with a compiler-libs module)
Pierre Letouzey
