aboutsummaryrefslogtreecommitdiff
path: root/library/global.ml
AgeCommit message (Expand)Author
2020-04-16Make cumulative sprop a typing flag, deprecate command line -sprop-cumulativeGaëtan Gilbert
2020-03-18Update headers in the whole code base.Théo Zimmermann
2020-02-09Remove the Template Check option.Pierre-Marie Pédrot
2019-12-13Use ~strict argument consistently in push_context/push_context_set intfsMatthieu Sozeau
2019-11-21[coq] Untabify the whole ML codebase.Emilio Jesus Gallego Arias
2019-10-16Split the function used to declare side-effects from the standard one.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-26Make kernel parametric on the lowest universe and fix #9294Matthieu Sozeau
2019-08-16Set/Unset commands for typing flagsSimonBoulier
2019-06-17Merge PR #10362: Kernel-side delaying of polymorphic opaque constantsGaëtan Gilbert
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2019-06-17Merge universe quantification and delayed constraints in opaque proofs.Pierre-Marie Pédrot
2019-06-17Allow to delay polymorphic opaque constants.Pierre-Marie Pédrot
2019-06-11Remove the side-effect role from the kernel.Pierre-Marie Pédrot
2019-05-24Remove the indirect opaque accessor hooks from Opaqueproof.Pierre-Marie Pédrot
2019-05-24Move body_of_constant_body to Global and specialize its uses.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-10[api] Remove 8.10 deprecations.Emilio Jesus Gallego Arias
2019-04-12Remove `constr_of_global_in_context`Maxime Dénès
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-12-13Move shallow state logic to the function preparing state for workersMaxime Dénès
2018-11-26Put -indices-matter in typing_flagsGaëtan Gilbert
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-31Seeing Global purely as a wrapper on top of kernel functions.Hugo Herbelin
2018-10-19Moving Global.constr_of_global_in_context to Typeops.Hugo Herbelin
2018-10-19Moving Global.type_of_global_in_context to Typeops.Hugo Herbelin
2018-10-16Deprecate Global.universes_of_global (replaced by environ version)Gaëtan Gilbert
2018-10-11A state-free version of is_polymorphic.Hugo Herbelin
2018-10-11Adding a functional version of constant_of_delta_kn.Hugo Herbelin
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: remove the (unused) by clauseVincent Laporte
2018-07-26Turn the kernel reduction sharing flag into an argument passed in the cache.Pierre-Marie Pédrot
2018-04-07Fixes #7192 (Print Assumptions does not enter implementation of submodules).Hugo Herbelin
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-09[summary] Adapt STM to the new Summary API.Emilio Jesus Gallego Arias
2017-12-01Proper nametab handling of global universe namesMatthieu Sozeau
2017-11-06[api] Move structures deprecated in the API to the core.Emilio Jesus Gallego Arias
2017-11-04[api] Deprecate all legacy uses of Name.Id in core.Emilio Jesus Gallego Arias
2017-07-26Removing template polymorphism for definitions.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 19:23:44 +0000