aboutsummaryrefslogtreecommitdiff
path: root/kernel
AgeCommit message (Expand)Author
2020-11-26[environ] [typing_flags] Introduce helper function to remove duplicate codeEmilio Jesus Gallego Arias
2020-11-26[kernel] Allow to set typing flags in add_mind [inductive]Emilio Jesus Gallego Arias
2020-11-26[kernel] Allow to set typing flags in add_constantEmilio Jesus Gallego Arias
2020-11-25Separate interning and pretyping of universesGaëtan Gilbert
2020-11-24Merge PR #13411: Rename the confusing neutral annotation in CClosure.coqbot-app[bot]
2020-11-21Rename the confusing neutral annotation in CClosure.Pierre-Marie Pédrot
2020-11-20Make sure accumulators do not exceed the minor heap (partly fix #11170).Guillaume Melquiond
2020-11-19Merge PR #12959: Improve the bytecode interpreterPierre-Marie Pédrot
2020-11-17Merge PR #13397: Adding heterogeneous map on named contexts.Pierre-Marie Pédrot
2020-11-16Adding heterogeneous map on named contexts.Hugo Herbelin
2020-11-16Improve bad variance error message: mention expected and actual variancesGaëtan Gilbert
2020-11-16Syntax for specifying cumulative inductivesGaëtan Gilbert
2020-11-16Infrastructure for cumulative inductive syntax (no grammar extension yet)Gaëtan Gilbert
2020-11-15Merge PR #13356: Make the universe of primitive arrays irrelevantPierre-Marie Pédrot
2020-11-13Merge PR #13358: Merge the Linked / LinkedInteractive native link information...coqbot-app[bot]
2020-11-13Hardcode next_up and next_down instead of relying on nextafter.Guillaume Melquiond
2020-11-13Add allocation-free variants of the nextup and nextdown floating-point operat...Guillaume Melquiond
2020-11-13Remove floating-point comparison operators as they are no longer needed.Guillaume Melquiond
2020-11-13Turn coq_float64.h into a .c file as it is no longer needed by coq_interp.c.Guillaume Melquiond
2020-11-13Inline the functions from coq_float64.h.Guillaume Melquiond
2020-11-13Make callback opcodes more generic.Guillaume Melquiond
2020-11-13Optimize Is_accu a bit.Guillaume Melquiond
2020-11-13Improve documentation of closure representations.Guillaume Melquiond
2020-11-13Turn Ksequence into a unary opcode, as its binary structure was never used.Guillaume Melquiond
2020-11-13Remove unused if-then-else construct from VM.Guillaume Melquiond
2020-11-13Restore discard_dead_code and use it to simplify match-with constructs.Guillaume Melquiond
2020-11-13Remove some unused opcodes from VM.Guillaume Melquiond
2020-11-13Remove unchecked arithmetic operations from VM, as they are not used.Guillaume Melquiond
2020-11-13Optimize handling of the VM stack with respect to the GC.Guillaume Melquiond
2020-11-13Make the universe of primitive arrays irrelevantGaëtan Gilbert
2020-11-13Remove unused CClosure.FNativeEntries.farrayGaëtan Gilbert
2020-11-12Merge PR #13351: Fixes #13349: accept Search on subparts of an identifier, no...coqbot-app[bot]
2020-11-12Merge the Linked and LinkedInteractive constructors.Pierre-Marie Pédrot
2020-11-12Statically ensure that the native interactive flag is always set to true.Pierre-Marie Pédrot
2020-11-12Statically ensure that native update locations are of form Linked*.Pierre-Marie Pédrot
2020-11-12Fix #13330: Kernel messes with polymorphic side-effects.Pierre-Marie Pédrot
2020-11-11Addressing #13349: accept Search on subparts of ident, not only on subidents.Hugo Herbelin
2020-11-09Remove the native symbol registering from the safe environment.Pierre-Marie Pédrot
2020-11-04Merge PR #13193: [build] [native] Don't assume installed native libraries are...coqbot-app[bot]
2020-11-03Eagerly reduce rigid/flex conversion problems.Pierre-Marie Pédrot
2020-11-03Add a fast path in CClosure stack zipping.Pierre-Marie Pédrot
2020-11-02Merge PR #13274: Fix two bugs in conversion of primitive valuescoqbot-app[bot]
2020-11-02Merge PR #13273: universes_of_constr: don't ignore CaseInvert universesPierre-Marie Pédrot
2020-10-26Yet another normal / neutral bug in primitive conversion.Pierre-Marie Pédrot
2020-10-26Fix bug in conversion of primitive values.Pierre-Marie Pédrot
2020-10-26universes_of_constr: don't ignore CaseInvert universesGaëtan Gilbert
2020-10-21Add missing deprecations in Projection API.Pierre-Marie Pédrot
2020-10-21Document the signatures of quotient names in the API.Pierre-Marie Pédrot
2020-10-21Introduce the missing dual name quotient modules in Environ.Pierre-Marie Pédrot
2020-10-21Code factorization in Names.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 16:22:46 +0000