aboutsummaryrefslogtreecommitdiff
path: root/kernel
AgeCommit message (Expand)Author
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
2020-12-21Move evaluable_global_reference from Names to Tacred.Pierre-Marie Pédrot
2020-12-11Merge PR #13519: Better primitive type support in custom string and numeral n...coqbot-app[bot]
2020-12-11Merge PR #13540: Clean support of primitive integersPierre-Marie Pédrot
2020-12-09Please the god of nitpicking by renaming the shift monoid operations.Pierre-Marie Pédrot
2020-12-09Document Esubst API and implementation.Pierre-Marie Pédrot
2020-12-09Compact representation of identity substitutions.Pierre-Marie Pédrot
2020-12-09Optimization: take advantage that we don't use arrays anymore in substitutions.Pierre-Marie Pédrot
2020-12-09More efficient implementation for substitutions.Pierre-Marie Pédrot
2020-12-09Cleanup substitution API.Pierre-Marie Pédrot
2020-12-04Better primitive type support in custom string and numeral notations.Fabian Kunze
2020-12-02Move *_with_full_binders variants out of the kernel.Pierre-Marie Pédrot
2020-12-02Make sure the msb is clear.Guillaume Melquiond
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 12:07:05 +0000