aboutsummaryrefslogtreecommitdiff
path: root/kernel/safe_typing.mli
AgeCommit message (Expand)Author
2019-12-07Section.t is never emptyGaëtan Gilbert
2019-11-01Declare type of primitives in CPrimitivesPierre Roux
2019-10-23Merge PR #10884: Last stop before CEP 40Maxime Dénès
2019-10-19universes_of_private: return set instead of list of setsGaëtan Gilbert
2019-10-16Ensure that side-effect declarations reaching the kernel are forced.Pierre-Marie Pédrot
2019-10-16Split the function used to declare side-effects from the standard one.Pierre-Marie Pédrot
2019-10-16Cleaning up the previous code by ensuring statically invariants on opaque pro...Pierre-Marie Pédrot
2019-10-14Remove [in_section] arguments to Safe_typing functionsGaëtan Gilbert
2019-10-02Loosen restrictions on mixing universe mono/polymorphism in sectionsGaëtan Gilbert
2019-09-26Implement section discharging inside kernel.Pierre-Marie Pédrot
2019-09-25Move the Lib section data into the kernel.Pierre-Marie Pédrot
2019-09-25Stub code for handling sections in kernel.Pierre-Marie Pédrot
2019-08-16Set/Unset commands for typing flagsSimonBoulier
2019-07-08Similar purity invariants in the kernel.Pierre-Marie Pédrot
2019-07-04Merge PR #10461: Simplify Declare.declare_variableEmilio Jesus Gallego Arias
2019-07-04Merge PR #10359: Remove dependency of native_compile on global env for symbolsMaxime Dénès
2019-07-03Safe_typing.push_named_assum: don't take universesGaëtan Gilbert
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2019-06-12Remove dependency of native_compile on global env for symbolsGaëtan Gilbert
2019-06-11Remove the side-effect role from the kernel.Pierre-Marie Pédrot
2019-06-11Move type definition Nativecode.symbols to NativevaluesGaëtan Gilbert
2019-05-26More precise type for Safe_typing export and inlining of private constants.Pierre-Marie Pédrot
2019-05-20Ensure statically that declarations built by Term_typing are direct.Pierre-Marie Pédrot
2019-05-19Merge the definition of constants and private constants in the API.Pierre-Marie Pédrot
2019-05-15Simplify the private constant API.Pierre-Marie Pédrot
2019-05-14Abstract away the implementation of side-effects in Safe_typing.Pierre-Marie Pédrot
2019-03-14Add a non-cumulative impredicative universe SProp.Gaëtan Gilbert
2019-02-08Remove global output_native_objects flag.Gaëtan Gilbert
2019-02-04Primitive integersMaxime Dénès
2018-11-26Put -indices-matter in typing_flagsGaëtan Gilbert
2018-11-06[checker] Refactor by sharing code with the kernelMaxime Dénès
2018-11-05Pass native and VM flags to the kernel through environmentMaxime Dénès
2018-10-31Use standard combinator for Global.set_strategyMaxime Dénès
2018-10-31Introduce Safe_typing.set_share_reductionMaxime Dénès
2018-10-11Adding a functional version of constant_of_delta_kn.Hugo Herbelin
2018-10-06[api] Remove (most) 8.9 deprecated objects.Emilio Jesus Gallego Arias
2018-10-05[kernel] Remove section paths from `KerName.t`Maxime Dénès
2018-09-27Remove {Safe_typing,Global}.push_contextGaëtan Gilbert
2018-09-14Retroknowledge: use GlobRef.t instead of Constr.t as entryVincent Laporte
2018-09-14Retroknowledge: remove the (unused) by clauseVincent Laporte
2018-09-03Merge PR #7912: Simplify effects APIMaxime Dénès
2018-06-28Deprecate Environ.retroknowledge function in favor of the projectionGaëtan Gilbert
2018-06-24Further cleaning of the side-effect API.Pierre-Marie Pédrot
2018-06-24Share the role type between the implementations of side-effects.Pierre-Marie Pédrot
2018-02-27Update headers following #6543.Théo Zimmermann
2017-12-19Let definitions do not create new universe constraints.Pierre-Marie Pédrot
2017-12-19Specific type for section definition entries.Pierre-Marie Pédrot
2017-12-16Let definitions must not contain side-effects when reaching the kernel.Pierre-Marie Pédrot
2017-12-09[api] Remove yet another type alias.Emilio Jesus Gallego Arias
2017-11-06[api] Move structures deprecated in the API to the core.Emilio Jesus Gallego Arias
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 04:21:33 +0000