aboutsummaryrefslogtreecommitdiff
path: root/library
AgeCommit message (Expand)Author
2019-06-25Merge PR #10284: Expose set interface to option tablesPierre-Marie Pédrot
2019-06-24Use named records instead of tuples where `polymorphic` used to be.Gaëtan Gilbert
2019-06-24[api] [proof] Move `discharge` type to vernac_ast where it is used.Emilio Jesus Gallego Arias
2019-06-24[api] Remove `polymorphic` type alias, use labels instead.Emilio Jesus Gallego Arias
2019-06-24[api] Move `locality` from `library` to `vernac`.Emilio Jesus Gallego Arias
2019-06-24[lemmas] [proof] Split proof kinds into per-layer components.Emilio Jesus Gallego Arias
2019-06-24[proof] Remove duplicated universe polymorphic from decl_kindsEmilio Jesus Gallego Arias
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-12Remove dependency of native_compile on global env for symbolsGaëtan Gilbert
2019-06-11Remove the side-effect role from the kernel.Pierre-Marie Pédrot
2019-06-11Move type definition Nativecode.symbols to NativevaluesGaëtan Gilbert
2019-06-08Cleaning the status of Local Definition and similar.Hugo Herbelin
2019-06-08Adding a new kind of assumption to track assumption coming from "Context".Hugo Herbelin
2019-06-04Remove the discharge segment from vo files.Pierre-Marie Pédrot
2019-06-04Slightly tweak the representation of dischargeable opaque proofs.Pierre-Marie Pédrot
2019-06-04Do not substitute opaque constants when discharging.Pierre-Marie Pédrot
2019-06-03Expose set interface to option tablesGaëtan Gilbert
2019-05-29Merge PR #10248: Move the Discharge module in the kernel and merge it with Co...Maxime Dénès
2019-05-28Merge PR #10258: Remove the delayed universe table from object files.Enrico Tassi
2019-05-27Remove the delayed universe table from object files.Pierre-Marie Pédrot
2019-05-26More precise type for Safe_typing export and inlining of private constants.Pierre-Marie Pédrot
2019-05-26Move the Discharge module into 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-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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 19:26:00 +0000