aboutsummaryrefslogtreecommitdiff
path: root/kernel
AgeCommit message (Expand)Author
2021-04-14Put async worker id in universe namesGaëtan Gilbert
2021-03-31[dune] Rename byterun to coqrunEmilio Jesus Gallego Arias
2021-03-30[flags] [profile] Remove bit-rotten CProfile code.Emilio Jesus Gallego Arias
2021-03-30Merge PR #14005: Support OCaml primitives with an actual arity larger than 4.Pierre-Marie Pédrot
2021-03-26[recordops] complete API rewrite; the module is now called [structures]Enrico Tassi
2021-03-26Improve dump of primitive OCaml operations.Guillaume Melquiond
2021-03-26Support OCaml primitives with an actual arity larger than 4.Guillaume Melquiond
2021-03-26Make it more obvious when the calling convention of APPLY changes.Guillaume Melquiond
2021-03-26Fix assertion that checks that APPLY can only be passed 4 arguments.Guillaume Melquiond
2021-03-26Split the return type away from the signature of primitive operations.Guillaume Melquiond
2021-03-26Similar fix for native compilation.Pierre-Marie Pédrot
2021-03-26Never store persistent arrays as VM structured values.Pierre-Marie Pédrot
2021-03-25Merge PR #13988: Mention label name in signature mismatch error when constant...Pierre-Marie Pédrot
2021-03-24Mention label name in signature mismatch error when constant expectedGaëtan Gilbert
2021-03-24Merge PR #13941: Set the lsb of return addresses on the bytecode interpreter ...Pierre-Marie Pédrot
2021-03-19Merge PR #13956: Remove useless prefix argument in native compilation.coqbot-app[bot]
2021-03-19Merge PR #13924: Fix kernel incorrectly assuming the "using" hyps are transit...Pierre-Marie Pédrot
2021-03-18Remove useless prefix argument in native compilation.Pierre-Marie Pédrot
2021-03-13Set the lsb of return addresses on the bytecode interpreter stack.Guillaume Melquiond
2021-03-11Merge PR #13854: Normalize evars during bytecode compilation.coqbot-app[bot]
2021-03-10Fix kernel incorrectly assuming the "using" hyps are transitively closedGaëtan Gilbert
2021-03-03[build] Split stdlib to it's own opam package.Emilio Jesus Gallego Arias
2021-02-28Merge PR #13853: Delay the dynamic linking of native-code libraries until nat...Pierre-Marie Pédrot
2021-02-26Signed primitive integersAna
2021-02-26Merge PR #13676: Protect caml_process_pending_actions_exn with caml_something...Pierre-Marie Pédrot
2021-02-26Merge PR #13868: Make genOpcodeFiles.ml handle opcode arity.Pierre-Marie Pédrot
2021-02-26Delay the dynamic linking of native-code libraries until native_compute is ca...Guillaume Melquiond
2021-02-24Infrastructure for fine-grained debug flagsMaxime Dénès
2021-02-23Normalize evars during bytecode compilation (fix #13841).Guillaume Melquiond
2021-02-19Be less permissive with respect to nonsensical bytecode.Guillaume Melquiond
2021-02-19Make the generated file the official source of arity.Guillaume Melquiond
2021-02-19Add a file coq_arity.h generated by genOpcodeFiles.ml.Guillaume Melquiond
2021-02-16Fix missing arities of VM opcodes.Guillaume Melquiond
2021-01-19Merge PR #13699: Fix #13579 (hnf on primitives raises an anomaly)Pierre-Marie Pédrot
2021-01-18Merge PR #13454: Remove unused retro_reflPierre-Marie Pédrot
2021-01-18Fix #13579 (hnf on primitives raises an anomaly)Pierre Roux
2021-01-10Remove MAKEPROD.Guillaume Melquiond
2021-01-10Remove SETFIELD0 and SETFIELD1.Guillaume Melquiond
2021-01-10Add a peephole optimization for PUSHFIELDS(1).Guillaume Melquiond
2021-01-10Remove LSLINT63CONST1 and LSRINT63CONST1 as they are unused.Guillaume Melquiond
2021-01-10Remove PUSHACC0, as it is strictly equivalent to PUSH.Guillaume Melquiond
2021-01-07Merge PR #13718: Move printing and sorting out of AcyclicGraphcoqbot-app[bot]
2021-01-06Further pushing up the printing and sorting of universes.Pierre-Marie Pédrot
2021-01-05Move universe printing out of AcyclicGraph.Pierre-Marie Pédrot
2021-01-04Remove redundant univ and parameter info from CaseInvertGaëtan Gilbert
2021-01-04Change the representation of kernel case.Pierre-Marie Pédrot
2021-01-04Move the relative linking order of Inductive w.r.t. VM / native.Pierre-Marie Pédrot
2021-01-04Merge PR #13685: Add a debug printer for fconstr substitutions.coqbot-app[bot]
2020-12-28Export a high-level representation of term substitutions.Pierre-Marie Pédrot
2020-12-26Protect caml_process_pending_actions_exn with caml_something_to_do.Guillaume Melquiond
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 12:11:01 +0000