coq
forked from coq/coq
Star 1
Fork 0
Watch

Version history of kernel/nativevalues.mli

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

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

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

June 2025

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

October 2024

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
Statically enforce primitive string size invariant.
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

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

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
Pierre-Marie Pédrot
Clever hack to reduce the amount of unsafe casts in native Vprod.
committed
Pierre-Marie Pédrot
Move the Prod case from native atoms to values.
committed
coqbot-app[bot]
Merge PR #16657: Merge the Acofix and Acofixe constructors of native atoms.
committed
Pierre-Marie Pédrot
Merge the Acofix and Acofixe constructors of native atoms.
committed
coqbot-app[bot]
Merge PR #16574: Non rectypes Nativevalues.t using GADT
committed
Gaëtan Gilbert
Non rectypes Nativevalues.t using GADT
committed
coqbot-app[bot]
Merge PR #16575: Remove unused Nativevalues.arrayinit and arraymap
committed

September 2022

Gaëtan Gilbert
Remove unused Nativevalues.arrayinit and arraymap
committed

February 2022

coqbot-app[bot]
Merge PR #15719: Add primitive floating-point Leibniz equality test
committed
Pierre Roux
Add floating-point Leibniz equality primitive
committed

November 2021

coqbot-app[bot]
Merge PR #15081: Use a uniform representation for the internal persistent arrays.
committed
Pierre-Marie Pédrot
Change the native compilation scheme of arrays.
committed

May 2021

Théo Zimmermann
Add examples from former detailed tactic examples chapter to their new location.
committed

February 2021

coqbot-app[bot]
Merge PR #13559: Signed primitive integers
committed
Ana
Signed primitive integers
committed

October 2020

coqbot-app[bot]
Merge PR #12955: Reroot primitive arrays on access
committed
Guillaume Melquiond
Remove occurrences of Parray.reroot.
committed

July 2020

Pierre-Marie Pédrot
Merge PR #11604: Primitive persistent arrays
committed