aboutsummaryrefslogtreecommitdiff
path: root/kernel
AgeCommit message (Expand)Author
2019-07-30Merge PR #10430: [Extraction] Add support for primitive integersMaxime Dénès
2019-07-25Mark primitives integer as able to participate in reductions (fixes #10560).Guillaume Melquiond
2019-07-22[Int63] Implement all primitives in OCamlVincent Laporte
2019-07-16Move unfold_side_flags CClosure -> Tacred internalsGaëtan Gilbert
2019-07-11Merge PR #10439: Uniform handling of side-effects for opaque definitionsMaxime Dénès
2019-07-08Similar purity invariants in the kernel.Pierre-Marie Pédrot
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-06-27Kernel transparent definition entries have no body universes.Gaëtan Gilbert
2019-06-26Perform the opaque section variable inference outside of the kernel.Pierre-Marie Pédrot
2019-06-26Remove dead code for typing of section definitions in kernel.Pierre-Marie Pédrot
2019-06-25Merge PR #10284: Expose set interface to option tablesPierre-Marie Pédrot
2019-06-24Code simplification for definition_entry type.Pierre-Marie Pédrot
2019-06-24Remove the unused opaque_entry_inline_code field from opaque entries.Pierre-Marie Pédrot
2019-06-24Enforce that opaque entries carry their type.Pierre-Marie Pédrot
2019-06-24Dedicated type for opaque entries in the kernel.Pierre-Marie Pédrot
2019-06-24Enforce that transparent entries are forced beforehand.Pierre-Marie Pédrot
2019-06-24Take advantage of the change of entry representation to split opacity status.Pierre-Marie Pédrot
2019-06-17Merge PR #10362: Kernel-side delaying of polymorphic opaque constantsGaëtan Gilbert
2019-06-17Update headers of files that were stuck on older headers.Théo Zimmermann
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2019-06-17Clean up the code adding monomorphic global constraints in Safe_typing.Pierre-Marie Pédrot
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-11Move the side-effect role out of Entries into Evd.Pierre-Marie Pédrot
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-07Merge PR #10308: Merge the two sources of monomorphic constraints for side-ef...Gaëtan Gilbert
2019-06-06Merge PR #9972: [build] Select uint63 using `ocamlc -config` variables.Vincent Laporte
2019-06-06Merge the two sources of monomorphic constraints for side-effects.Pierre-Marie Pédrot
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-31Fix #10268: vio2vo produces incorrect term when discharging.Pierre-Marie Pédrot
2019-05-29Merge PR #10252: Various dynamic assertions and cleanups in opaque typingMaxime Dénès
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-28Merge PR #10133: mind_kelim is the highest allowed sort instead of a listPierre-Marie Pédrot
2019-05-27Remove the delayed universe table from object files.Pierre-Marie Pédrot
2019-05-27Merge PR #10249: More precise type for export and inlining of private constantsMaxime Dénès
2019-05-27Fix #10251: Type-checking of polymorphic opaque constr entry types is broken.Pierre-Marie Pédrot
2019-05-27Specific code path for opaque polymorphic constants.Pierre-Marie Pédrot
2019-05-27Ensure dynamically that non-opaque definitions are always side-effect free.Pierre-Marie Pédrot
2019-05-27Ensure dynamically that opaque definitions come with their type.Pierre-Marie Pédrot
2019-05-27mind_kelim is the highest allowed sort instead of a listGaëtan Gilbert
2019-05-26More precise type for Safe_typing export and inlining of private constants.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 18:26:32 +0000