aboutsummaryrefslogtreecommitdiff
path: root/library
AgeCommit message (Expand)Author
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
2019-08-16Set/Unset commands for typing flagsSimonBoulier
2019-07-31Specialize the section API.Pierre-Marie Pédrot
2019-07-31Remove the universe part from the section variable mechanism.Pierre-Marie Pédrot
2019-07-31Code simplification in Lib section handling.Pierre-Marie Pédrot
2019-07-18Remove dead code in Lib.Pierre-Marie Pédrot
2019-07-18Attach the universe polymorphic status to sections.Pierre-Marie Pédrot
2019-07-18Use a dedicated data structure for section representation in Lib.Pierre-Marie Pédrot
2019-07-11Merge PR #10498: [api] Deprecate GlobRef constructors.Gaëtan Gilbert
2019-07-08[api] Deprecate GlobRef constructors.Emilio Jesus Gallego Arias
2019-07-08[core] [api] Support OCaml 4.08Emilio Jesus Gallego Arias
2019-07-04Merge PR #10461: Simplify Declare.declare_variableEmilio Jesus Gallego Arias
2019-07-04Merge PR #10359: Remove dependency of native_compile on global env for symbolsMaxime Dénès
2019-07-03Safe_typing.push_named_assum: don't take universesGaëtan Gilbert
2019-07-03Simplify (restrict_path 0 sp) -> (make_path DirPath.empty id)Gaëtan Gilbert
2019-07-03Merge PR #10442: Reify libobject containersEmilio Jesus Gallego Arias
2019-07-01[api] Reduce declare_kinds even more.Emilio Jesus Gallego Arias
2019-07-01[api] Refactor most of `Decl_kinds`Emilio Jesus Gallego Arias
2019-06-28Reify libobject containersMaxime Dénès
2019-06-25Merge PR #10316: [lemmas] Reify info for implicits, universe decls, and rec t...Pierre-Marie Pédrot
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 12:55:49 +0000