aboutsummaryrefslogtreecommitdiff
path: root/kernel/cClosure.ml
AgeCommit message (Expand)Author
2018-02-07Merge PR #6685: Use whd-all on rigid-flex conversion.Maxime Dénès
2018-02-05Respect the transparent state of the current conversion on strong weak-head.Pierre-Marie Pédrot
2018-02-02CClosure.unfold_projection: don't catch Not_found, assume env is okGaëtan Gilbert
2018-02-02kernel: cleanup projection unfoldingGaëtan Gilbert
2017-12-29Share the rel environment between Environ.env and reduction cache.Pierre-Marie Pédrot
2017-12-23[api] Also deprecate constructors of Decl_kinds.Emilio Jesus Gallego Arias
2017-11-26[api] Remove aliases of `Evar.t`Emilio Jesus Gallego Arias
2017-11-23Make some functions on terms more robust w.r.t new term constructs.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-07-04Bump year in headers.Pierre-Marie Pédrot
2017-06-02Drop '.' from CErrors.anomaly, insert it in argsJason Gross
2017-04-12Missing optimization when Kernel Term Sharing is disabled.Pierre-Marie Pédrot
2017-02-19Optimizing array mapping in the kernel.Pierre-Marie Pédrot
2016-09-09Fast access environment in CClosure.Pierre-Marie Pédrot
2016-07-03closure.ml renamed into cClosure.ml (avoid clash with a compiler-libs module)Pierre Letouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 18:05:10 +0000