aboutsummaryrefslogtreecommitdiff
path: root/library
AgeCommit message (Expand)Author
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-24Statically ensure the content of delayed proofs in vio file.Pierre-Marie Pédrot
2019-05-23Merge PR #9895: [loadpath] Make loadpath handling self-contained and move to ...Maxime Dénès
2019-05-23Fixing typos - Part 2JPR
2019-05-22Merge PR #10177: Fix #10176: shadowing vs automatic class based generalizatio...Hugo Herbelin
2019-05-21[loadpath] Make loadpath handling self-contained and move to vernacEmilio Jesus Gallego Arias
2019-05-21Merge PR #10160: Miscellaneous fixes related to the command lineVincent Laporte
2019-05-20Ensure statically that declarations built by Term_typing are direct.Pierre-Marie Pédrot
2019-05-19Parameterize the constant_body type by opaque subproofs.Pierre-Marie Pédrot
2019-05-19Merge the definition of constants and private constants in the API.Pierre-Marie Pédrot
2019-05-19Inverting the responsibility to define logically a constant in Declare.Pierre-Marie Pédrot
2019-05-16Fix #10176: shadowing vs automatic class based generalizationGaëtan Gilbert
2019-05-14Ensuring suffix of file to compile also for -vio2vo checking.Hugo Herbelin
2019-05-10[api] Remove 8.10 deprecations.Emilio Jesus Gallego Arias
2019-04-30Remove Global.env from goptions by passing from vernacentriesGaëtan Gilbert
2019-04-30Merge PR #9952: Remove `constr_of_global_in_context`Pierre-Marie Pédrot
2019-04-17Merge PR #9876: Command-line setters for optionsEmilio Jesus Gallego Arias
2019-04-16Better error message when OCaml compiler not found for native computeMaxime Dénès
2019-04-16Command-line setters for optionsGaëtan Gilbert
2019-04-12Remove `constr_of_global_in_context`Maxime Dénès
2019-04-10Remove calls to global env in InductiveopsMaxime Dénès
2019-03-14Add a non-cumulative impredicative universe SProp.Gaëtan Gilbert
2019-02-26Fix deprecation warningEnrico Tassi
2019-02-08Remove global output_native_objects flag.Gaëtan Gilbert
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 11:59:42 +0000