aboutsummaryrefslogtreecommitdiff
path: root/kernel/cClosure.ml
AgeCommit message (Expand)Author
2019-07-25Mark primitives integer as able to participate in reductions (fixes #10560).Guillaume Melquiond
2019-07-16Move unfold_side_flags CClosure -> Tacred internalsGaëtan Gilbert
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2019-05-23Fixing typos - Part 2JPR
2019-05-19Make the type of constant bodies parametric on opaque proofs.Pierre-Marie Pédrot
2019-03-14Put [@inline] on CClosure.Mark functionsGaëtan Gilbert
2019-03-14mutable relevance marks in fconstrGaëtan Gilbert
2019-03-14Enable proof irrelevance for SProp.Gaëtan Gilbert
2019-03-14Add relevance marks on binders.Gaëtan Gilbert
2019-02-04Primitive integersMaxime Dénès
2018-12-23Remove dead code from CClosure.Pierre-Marie Pédrot
2018-11-20Use a closure for the domain argument of FProd.Pierre-Marie Pédrot
2018-11-20Do not wrap FProd return types in a closure.Pierre-Marie Pédrot
2018-11-19Rename TranspState into TransparentState.Pierre-Marie Pédrot
2018-11-19Proper record type and accessors for transparent states.Pierre-Marie Pédrot
2018-11-19Move transparent_state to its own module.Pierre-Marie Pédrot
2018-10-31Merge PR #8752: Enable fragile pattern warning in cclosureMaxime Dénès
2018-10-17Enable fragile pattern warning in cclosureGaëtan Gilbert
2018-10-11Clean up CClosure code.Pierre-Marie Pédrot
2018-10-11The cbv reduction does not rely on the kernel info data structure anymore.Pierre-Marie Pédrot
2018-10-04Remove FCast from CClosure.fterm.Pierre-Marie Pédrot
2018-09-26Inline the definition of CClosure.mk_clos_deep.Pierre-Marie Pédrot
2018-09-24[kernel] Compile with almost all warnings enabled.Emilio Jesus Gallego Arias
2018-07-26Turn the kernel reduction sharing flag into an argument passed in the cache.Pierre-Marie Pédrot
2018-07-24Projections use index representationGaëtan Gilbert
2018-06-27Swapping Context and Constr: defining declarations on constr in Constr.Hugo Herbelin
2018-06-23Using more general information for primitive records.Pierre-Marie Pédrot
2018-06-17Faster and cleaner fconstr-to-constr conversion function.Pierre-Marie Pédrot
2018-06-04Merge PR #7418: Actually take advantage of the normalization status of kernel...Maxime Dénès
2018-05-28Unify pre_env and envMaxime Dénès
2018-05-23Exporting Fun1 within Array so that Array.Fun1 and not only CArray.Fun1 works.Hugo Herbelin
2018-05-01Actually take advantage of the normalization status of kernel closures.Pierre-Marie Pédrot
2018-03-28[api] Deprecate a couple of aliases that we missed.Emilio Jesus Gallego Arias
2018-03-09Merge PR #6769: Split closure cache and remove whd_bothMaxime Dénès
2018-03-05Replace invalid tag @raises in ocamldoc comments with @raisemrmr1993
2018-03-04Pass the constant cache as a separate argument in kernel reduction.Pierre-Marie Pédrot
2018-02-27Update headers following #6543.Théo Zimmermann
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 18:41:31 +0000