aboutsummaryrefslogtreecommitdiff
path: root/library
AgeCommit message (Expand)Author
2020-12-02Stop calling Id.Map.domain on univ binders every individual universeGaëtan Gilbert
2020-11-26[kernel] Allow to set typing flags in add_mind [inductive]Emilio Jesus Gallego Arias
2020-11-26[kernel] Allow to set typing flags in add_constantEmilio Jesus Gallego Arias
2020-11-25Separate interning and pretyping of universesGaëtan Gilbert
2020-11-09Remove the native symbol registering from the safe environment.Pierre-Marie Pédrot
2020-10-21Similar introduction of a Construct module in the Names API.Pierre-Marie Pédrot
2020-10-21Introduce an Ind module in the Names API.Pierre-Marie Pédrot
2020-10-21Rename the GlobRef comparison modules following the standard pattern.Pierre-Marie Pédrot
2020-08-21Use a map function instead of a fold when freezing summaries.Pierre-Marie Pédrot
2020-06-30[states] Move States to vernacEmilio Jesus Gallego Arias
2020-05-15[misc] Better preserve backtraces in several modulesEmilio Jesus Gallego Arias
2020-05-13Make explicit that UGraph lower bounds are only of two kinds.Pierre-Marie Pédrot
2020-04-28Merge PR #12003: Improve error messages for Set and Unset commands.Emilio Jesus Gallego Arias
2020-04-23Merge PR #12034: Make cumulative sprop a typing flag, deprecate command line...Pierre-Marie Pédrot
2020-04-20Move new iter_table function to Goptions.Théo Zimmermann
2020-04-20Improve undeclared key messages.Théo Zimmermann
2020-04-16Make cumulative sprop a typing flag, deprecate command line -sprop-cumulativeGaëtan Gilbert
2020-04-13correctly open objects for Names filtersGaëtan Gilbert
2020-04-13pass filters aroundGaëtan Gilbert
2020-04-13Add ExtRefMap/Set to globnamesGaëtan Gilbert
2020-04-06Clean and fix definitions of options.Théo Zimmermann
2020-04-03Improve error messages for Set and Unset commands.Théo Zimmermann
2020-03-30Merge PR #11817: [cleanup] Remove unnecessary Map/Set module creationGaëtan Gilbert
2020-03-18Update headers in the whole code base.Théo Zimmermann
2020-03-13[cleanup] Remove unnecessary Map/Set module creationEmilio Jesus Gallego Arias
2020-03-03[exninfo] Deprecate aliases for exception re-raising.Emilio Jesus Gallego Arias
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 14:25:50 +0000