aboutsummaryrefslogtreecommitdiff
path: root/kernel
AgeCommit message (Expand)Author
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-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
2020-12-02Greatly simplify the conversion functions between Z.t and Uint63.t.Guillaume Melquiond
2020-12-01Make the code clearer and faster by calling mask63 explicitly at the end.Guillaume Melquiond
2020-12-01Avoid compiler warnings.Guillaume Melquiond
2020-12-01Added comment about l2r in check_correct_arityGaëtan Gilbert
2020-12-01Use ~l2r:true to restore previous order of unfolding when typing predicates o...Matthieu Sozeau
2020-11-30Merge PR #13501: [kernel] Fix #13495: incompleteness in cases typing for cumu...coqbot-app[bot]
2020-11-27[kernel] Fix #13495: incompleteness in cases typing for cumulative inductive ...Matthieu Sozeau
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-23Remove unused retro_reflGaëtan Gilbert
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 18:22:08 +0000