aboutsummaryrefslogtreecommitdiff
path: root/kernel
AgeCommit message (Expand)Author
2019-10-24Raise an anomaly when looking up unknown constant/inductiveGaëtan Gilbert
2019-10-23Merge PR #10884: Last stop before CEP 40Maxime Dénès
2019-10-19universes_of_private: return set instead of list of setsGaëtan Gilbert
2019-10-18Merge PR #10904: Fix a De Bruijn bug in the computation of term relevance in ...Gaëtan Gilbert
2019-10-18Merge PR #8228: (Partially) Revert "Make Environ.globals abstract."Pierre-Marie Pédrot
2019-10-16Ensure that side-effect declarations reaching the kernel are forced.Pierre-Marie Pédrot
2019-10-16Split the function used to declare side-effects from the standard one.Pierre-Marie Pédrot
2019-10-16Cleaning up the previous code by ensuring statically invariants on opaque pro...Pierre-Marie Pédrot
2019-10-16Make explicit the delayed computation of opaque bodies in Term_typing.Pierre-Marie Pédrot
2019-10-16Fix a De Bruijn bug in the computation of term relevance in the kernel.Pierre-Marie Pédrot
2019-10-14Use kernel info from Global for Lib.sections_{depth,are_opened}Gaëtan Gilbert
2019-10-14Remove [in_section] arguments to Safe_typing functionsGaëtan Gilbert
2019-10-13Merge PR #10670: ComAssumption cleanupPierre-Marie Pédrot
2019-10-12Merge PR #10818: Merge Direct and Indirect nodes in Opaqueproof.Maxime Dénès
2019-10-07(Partially) Revert "Make Environ.globals abstract."Emilio Jesus Gallego Arias
2019-10-05Remove "is_polymorphic_univ" checks in upper layers.Gaëtan Gilbert
2019-10-04Merge Direct and Indirect nodes in Opaqueproof.Pierre-Marie Pédrot
2019-10-04Remove redundancy in section hypotheses of kernel entries.Pierre-Marie Pédrot
2019-10-04Merge PR #10798: Loosen restrictions on mixing universe mono/polymorphism in ...Pierre-Marie Pédrot
2019-10-02Merge PR #10768: [ci] Update to OCaml 4.09.0, drop now useless "trunk" jobs.Gaëtan Gilbert
2019-10-02Loosen restrictions on mixing universe mono/polymorphism in sectionsGaëtan Gilbert
2019-09-26Move the declararation of delayed constraints out of add_constant_aux.Pierre-Marie Pédrot
2019-09-26Implement section discharging inside kernel.Pierre-Marie Pédrot
2019-09-25Clean up InferCumulativity after its move to the kernel.Pierre-Marie Pédrot
2019-09-25Move the Lib section data into the kernel.Pierre-Marie Pédrot
2019-09-25Move cumulativity inference to the kernel.Pierre-Marie Pédrot
2019-09-25Stub code for handling sections in kernel.Pierre-Marie Pédrot
2019-09-19[ocaml] Allow building with deprecated Obj primitives.Emilio Jesus Gallego Arias
2019-09-02Merge PR #9918: Fix #9294: critical bug with template polymorphismPierre-Marie Pédrot
2019-08-26Make kernel parametric on the lowest universe and fix #9294Matthieu Sozeau
2019-08-24Simplify picking between uint63_63.ml and uint63_31.mlGaëtan Gilbert
2019-08-16Fix typing_flags in the checkerSimonBoulier
2019-08-16Set/Unset commands for typing flagsSimonBoulier
2019-08-16Split the [check_guarded] typing_flag into [check_guarded] (for (co)fixpoints...SimonBoulier
2019-08-02Merge PR #10553: Use a more traditional definition for uint63_div21 (fixes #1...Maxime Dénès
2019-07-30Merge PR #10430: [Extraction] Add support for primitive integersMaxime Dénès
2019-07-29Use the precondition of diveucl_21 to avoid massaging the dividend.Guillaume Melquiond
2019-07-29Transpose the C code of uint63_div21 to the OCaml implementations.Guillaume Melquiond
2019-07-29Use a more traditional definition for uint63_div21 (fixes #10551).Guillaume Melquiond
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 15:12:18 +0000