aboutsummaryrefslogtreecommitdiff
path: root/kernel
AgeCommit message (Expand)Author
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-12Merge PR #13351: Fixes #13349: accept Search on subparts of an identifier, no...coqbot-app[bot]
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
2020-10-21Similar introduction of a Construct module in the Names API.Pierre-Marie Pédrot
2020-10-21Introduce an Ind module in the Names API.Pierre-Marie Pédrot
2020-10-21Rename the GlobRef comparison modules following the standard pattern.Pierre-Marie Pédrot
2020-10-21Same little game with Projection.Pierre-Marie Pédrot
2020-10-21Deprecate the non-qualified equality functions on kerpairs.Pierre-Marie Pédrot
2020-10-21Introduce a dummy name quotient API.Pierre-Marie Pédrot
2020-10-21Merge PR #12955: Reroot primitive arrays on accesscoqbot-app[bot]
2020-10-19Merge PR #13151: Remove the compare_graph field from the conversion API.coqbot-app[bot]
2020-10-14[build] [native] Don't assume installed native libraries are in custom output...Emilio Jesus Gallego Arias
2020-10-14Merge PR #13147: Use OCaml floating-point operations on 64 bits archcoqbot-app[bot]
2020-10-12Merge PR #13156: Store the resolver of required modules as functor parameters...coqbot-app[bot]
2020-10-12Merge PR #12449: Minimize Prop <= i to i := Setcoqbot-app[bot]
2020-10-11Similarly remove the explicit graph argument in the ~evar conversion API.Pierre-Marie Pédrot
2020-10-11Pick the universe graph out of the environment in conversion API.Pierre-Marie Pédrot
2020-10-11Remove the compare_graph field from the conversion API.Pierre-Marie Pédrot
2020-10-09Merge PR #13143: Drop misleading argument of Pp.h boxcoqbot-app[bot]
2020-10-09No bidirectionality when expected type for lambda is an evar.Gaëtan Gilbert
2020-10-09Merge PR #13087: Put type-in-type flag in ugraph.Pierre-Marie Pédrot
2020-10-09Store the resolver of required modules as functor parameters in safe_env.Pierre-Marie Pédrot
2020-10-08Dropping the misleading int argument of Pp.h.Hugo Herbelin
2020-10-08Remove occurrences of Parray.reroot.Guillaume Melquiond
2020-10-08Reroot primitive arrays on access (fix #12947).Guillaume Melquiond
2020-10-06Use OCaml floating-point operations on 64 bits archPierre Roux
2020-10-02{new,setoid_}ring -> ringMaxime Dénès
2020-09-28Put type-in-type flag in ugraph.Gaëtan Gilbert
2020-09-22Use the closure tag for accumulators.Guillaume Melquiond
2020-09-22Use the same memory layout as closures for accumulators.Guillaume Melquiond
2020-09-22Modify bytecode representation of closures to please OCaml's GC (fix #12636).Guillaume Melquiond
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 14:09:14 +0000