aboutsummaryrefslogtreecommitdiff
path: root/library
AgeCommit message (Expand)Author
2020-02-13Merge PR #11521: Remove Goptions.opt_name fieldPierre-Marie Pédrot
2020-02-12Remove Goptions.opt_name fieldGaëtan Gilbert
2020-02-12Standardize constr -> globref operations to use destRef/isRef/isRefXGaëtan Gilbert
2020-02-09Remove the Template Check option.Pierre-Marie Pédrot
2020-01-30export_private_constants doesn't use the [constr in_univ_ctx] argumentGaëtan Gilbert
2020-01-30Merge PR #11307: Remove the hacks relying on hardwired libobject tags.Maxime Dénès
2020-01-28Remove dead code in Globnames.Pierre-Marie Pédrot
2020-01-27cleanup: Lib.freeze doesn't use its [~marshallable] argumentGaëtan Gilbert
2019-12-22Remove the hacks relying on hardwired libobject tags.Pierre-Marie Pédrot
2019-12-22Export the dynamic type API of libobjects.Pierre-Marie Pédrot
2019-12-18Merge PR #10616: Fix push_universe_context* interfaces to use a consistent ~s...Pierre-Marie Pédrot
2019-12-13Use ~strict argument consistently in push_context/push_context_set intfsMatthieu Sozeau
2019-12-12Merge PR #11278: Clean libobject stuffGaëtan Gilbert
2019-12-11Remove the unused add_leaves Libobject primitive.Pierre-Marie Pédrot
2019-12-09Type-safe implementation of libobjects.Pierre-Marie Pédrot
2019-12-09Simplify the implementation of Summary by specifying the type of ML-MODULES.Pierre-Marie Pédrot
2019-12-09Type-safe implementation of summary state.Pierre-Marie Pédrot
2019-12-07Section.t is never emptyGaëtan Gilbert
2019-11-21[coq] Untabify the whole ML codebase.Emilio Jesus Gallego Arias
2019-11-01Declare type of primitives in CPrimitivesPierre Roux
2019-10-24[library] [nit] Remove unnecessary type alias.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 obj_sec field of Nametab.obj_prefix record.Gaëtan Gilbert
2019-10-14Use kernel info from Global for Lib.sections_{depth,are_opened}Gaëtan Gilbert
2019-10-14Remove [in_section] arguments to Safe_typing functionsGaëtan Gilbert
2019-10-05Remove "is_polymorphic_univ" checks in upper layers.Gaëtan Gilbert
2019-10-04Merge PR #10798: Loosen restrictions on mixing universe mono/polymorphism in ...Pierre-Marie Pédrot
2019-10-03Merge PR #10727: [library] Move `Declaremods` to `vernac/`Pierre-Marie Pédrot
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-09-25Refine the API to declare section-local universes.Pierre-Marie Pédrot
2019-09-18[library] Move `Declaremods` to `vernac/`Emilio Jesus Gallego Arias
2019-09-16Optimize multiple importsMaxime Dénès
2019-09-16Optimize `Include`d `Export`sMaxime Dénès
2019-09-16Turn `module_objects` into a recordMaxime Dénès
2019-09-16Optimize module ExportsMaxime Dénès
2019-09-16Do not cache objects when importing modulesMaxime Dénès
2019-09-16Specialize `ImportObject` to `Export`Maxime Dénès
2019-09-16`do_modtype` -> `load_modtype`Maxime Dénès
2019-09-04Merge PR #10612: Fix feedback levelsEmilio Jesus Gallego Arias
2019-09-02Merge PR #10562: [library] Move library to vernacMaxime Dénès
2019-08-30[library] Move library to vernacEmilio Jesus Gallego Arias
2019-08-29Make sure that all query commands return a notice (not an info) feedbackMaxime Dénès
2019-08-26Make kernel parametric on the lowest universe and fix #9294Matthieu Sozeau
2019-08-23Merge PR #10665: [api] Move handling of variable implicit data to impargsGaëtan Gilbert
2019-08-21Merge PR #10666: [api] Move `Keys` to pretypingEnrico Tassi
2019-08-19[api] Move handling of variable implicit data to impargsEmilio Jesus Gallego Arias
2019-08-18[api] Move `Keys` to pretypingEmilio Jesus Gallego Arias
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 12:36:05 +0000