coq
forked from coq/coq
Star 1
Fork 0
Watch

Version history of kernel/nativevalues.ml

October 2026

coqbot-app[bot]
Merge PR #22598: Expose the Nativevalues internals as OCaml externals.
committed
Pierre-Marie Pédrot
Expose the Nativevalues internals as OCaml externals.
committed

January 2026

coqbot-app[bot]
Merge PR #21540: Port native_compute to OCaml 5 (using tag 0 and caml_curry2_1)
committed
Guillaume Melquiond
Port native_compute to OCaml 5.
committed

December 2025

coqbot-app[bot]
Merge PR #21411: Split sort substitution from accumulator construction in native compilation
committed
Pierre-Marie Pédrot
Split sort substitution from accumulator construction in native compilation.
committed
coqbot-app[bot]
Merge PR #21409: Fix native conversion of polymorphic code after #21405.
committed
Pierre-Marie Pédrot
Fix native conversion of polymorphic code after #21405.
committed

October 2025

coqbot-app[bot]
Merge PR #21140: Use user equality in comparison of native values.
committed

September 2025

Pierre-Marie Pédrot
Use user equality in comparison of native values.
committed
coqbot-app[bot]
Merge PR #20910: Move Obj.magic outside mk_cofix_accu
committed

July 2025

Gaëtan Gilbert
Move Obj.magic outside mk_cofix_accu
committed
coqbot-app[bot]
Merge PR #20817: Native compute use OCaml Lazy.t instead of adhoc ref
committed
Gaëtan Gilbert
Native compute use OCaml Lazy.t instead of adhoc ref
committed

June 2025

coqbot-app[bot]
Merge PR #20782: Native compute reduce mutability of accus
committed
Gaëtan Gilbert
Native compute reduce mutability of accus
committed
coqbot-app[bot]
Merge PR #20719: Tweak the native compilation scheme of cofixpoints.
committed
coqbot-app[bot]
Merge PR #20696: nativecode don't generate forcecofix for non coinductive primproj
committed
Pierre-Marie Pédrot
Tweak the native compilation scheme of cofixpoints.
committed
Gaëtan Gilbert
nativevalues don't put finiteness info in annot_sw
committed
coqbot-app[bot]
Merge PR #20704: Stop using "dummy_value" in native compute
committed
Gaëtan Gilbert
Avoid using dummy_value for returning data from native compute
committed

January 2025

coqbot-app[bot]
Merge PR #20026: Rename Coq -> Rocq in various comments and doc
committed
Pierre Roux
Rename Coq -> Rocq in various comments and doc
committed

October 2024

coqbot-app[bot]
Merge PR #19734: Rocqify the core.
committed
Pierre-Marie Pédrot
Rocqify the core.
committed
coqbot-app[bot]
Merge PR #19721: Rocqify the VM
committed
Pierre-Marie Pédrot
Rename all C functions and macros from the VM according to the Great Rocqification.
committed
coqbot-app[bot]
Merge PR #19692: Update the OCaml headers to reflect the fact Coq is now Rocq.
committed
Pierre-Marie Pédrot
Update the OCaml headers to reflect the fact Coq is now Rocq.
committed

June 2024

coqbot-app[bot]
Merge PR #18973: Add primitive string type.
committed
Rodolphe Lepigre
Add a primitive string type.
committed

February 2024

coqbot-app[bot]
Merge PR #18669: Fix misplaced attributes.
committed
Rodolphe Lepigre
Fix misplaced attributes.
committed

November 2023

coqbot-app[bot]
Merge PR #17836: Kernel sort polymorphism
committed
Gaëtan Gilbert
sort poly (with simple squashing model and no inductive output in qsort)
committed
Gaëtan Gilbert
Move universe polymorphism APIs to new file UVars before sort poly
committed

September 2023

coqbot-app[bot]
Merge PR #18036: Rebuild case info in nativenorm
committed
Gaëtan Gilbert
Native: cleanup unused asw_ci in case annotation
committed

July 2023

coqbot-app[bot]
Merge PR #17872: Fix #17871 (inconsistency with native_compute and primitive floats)
committed
Pierre Roux
Fix #17871 inconsistency with native_compute and primitive floats
committed

January 2023

coqbot-app[bot]
Merge PR #16903: Introduce sort variables in unification
committed
Pierre-Marie Pédrot
Introduce quality variables in sorts.
committed

December 2022

coqbot-app[bot]
Merge PR #16947: Define a dummy replacement for Obj.set_tag for OCaml 5.
committed
Pierre-Marie Pédrot
Define a dummy replacement for Obj.set_tag for OCaml 5.
committed

November 2022

coqbot-app[bot]
Merge PR #16629: Merge the VM and native reification view type
committed
coqbot-app[bot]
Merge PR #16692: Remove the support of metavariables from native and VM compilation.
committed
Pierre-Marie Pédrot
Remove the support of metavariables from native and VM compilation.
committed

October 2022

Pierre-Marie Pédrot
Merge the VM and native view types.
committed
coqbot-app[bot]
Merge PR #16697: Move the Prod case from native atoms to values.
committed