aboutsummaryrefslogtreecommitdiff
path: root/kernel
AgeCommit message (Expand)Author
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-24Infrastructure for fine-grained debug flagsMaxime Dénès
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
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 18:10:35 +0000