aboutsummaryrefslogtreecommitdiff
path: root/library
AgeCommit message (Expand)Author
2019-02-04Primitive integersMaxime Dénès
2018-12-17Merge PR #9220: Move shallow state logic to the function preparing state for ...Enrico Tassi
2018-12-14[proof] Rework proof interface.Emilio Jesus Gallego Arias
2018-12-13Move shallow state logic to the function preparing state for workersMaxime Dénès
2018-12-12Higher-level libobject API for objects with fixed scopesMaxime Dénès
2018-12-12Merge PR #8974: Fix mod_subst wrt universe polymorphismMaxime Dénès
2018-12-12Merge PR #9150: [doc] Enable Warning 50 [incorrect doc comment] and fix comme...Maxime Dénès
2018-12-09[doc] Enable Warning 50 [incorrect doc comment] and fix comments.Emilio Jesus Gallego Arias
2018-12-06Revise API for global universes.Gaëtan Gilbert
2018-12-06Fix race condition triggered by fresh universe generationMaxime Dénès
2018-12-05Fix mod_subst wrt universe polymorphismGaëtan Gilbert
2018-11-28[options] New helper for creation of boolean options plus reference.Emilio Jesus Gallego Arias
2018-11-27Merge PR #9046: Goptions.declare_* functions return unit instead of a write_f...Emilio Jesus Gallego Arias
2018-11-26Put -indices-matter in typing_flagsGaëtan Gilbert
2018-11-23Goptions.declare_* functions return unit instead of a write_functionGaëtan Gilbert
2018-11-15Move generating library dirpath to stm in compile mode.Gaëtan Gilbert
2018-11-13Merge PR #8906: [Goptions] More detailed error messagesMaxime Dénès
2018-11-09Use arrays of names instead of lists in abstract universe names.Pierre-Marie Pédrot
2018-11-09Force the user to provide names when generating abstract universe contexts.Pierre-Marie Pédrot
2018-11-05Merge PR #8871: [library] Move Nametab/Lib specific-names to NametabHugo Herbelin
2018-11-05[Goptions] More detailed error messagesVincent Laporte
2018-11-05Merge PR #8870: Pass native and VM flags to the kernel through environmentPierre-Marie Pédrot
2018-11-05Merge PR #8857: [library] Better sizing for libobject hashtbl.Pierre-Marie Pédrot
2018-11-05Merge PR #8766: [nametab] [api] Provide basic support for efficient completion.Pierre-Marie Pédrot
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-31[nametab] Move `object_prefix` to `Nametab`.Emilio Jesus Gallego Arias
2018-10-31[nametab] Move global_dir_reference to NametabEmilio Jesus Gallego Arias
2018-10-31Merge PR #8825: [libobject] Move object_name next to object definition.Pierre-Marie Pédrot
2018-10-31[library] Better sizing for libobject hashtbl.Emilio Jesus Gallego Arias
2018-10-29Merge PR #8812: [ssreflect] Better use of CoqlibEnrico Tassi
2018-10-26[libobject] Move object_name next to object definition.Emilio Jesus Gallego Arias
2018-10-26Merge PR #8687: Mini reorganization type of global constr of globalPierre-Marie Pédrot
2018-10-24[Coqlib] Remove redundant checkVincent Laporte
2018-10-19Deprecating Global.type_of_global_in_context.Hugo Herbelin
2018-10-19Deprecating Global.constr_of_global_in_context.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-18[nametab] [api] Provide basic support for efficient completion.Emilio Jesus Gallego Arias
2018-10-18[api] Qualify access to `Nametab`Emilio Jesus Gallego Arias
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-10[coqlib] Rebindable Coqlib namespace.Emilio Jesus Gallego Arias
2018-10-08Merge PR #8585: Simplify declaration of universe namesPierre-Marie Pédrot
2018-10-05[kernel] Remove section paths from `KerName.t`Maxime Dénès
2018-10-04Simplify declaration of universe namesGaëtan Gilbert
2018-10-03Merge PR #8596: [api] Cleanup `Decls`: remove unused function, move vernac he...Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 21:15:17 +0000