coq
forked from coq/coq
Star 1
Fork 0
Watch

Version history of kernel/nativeconv.ml

April 2026

coqbot-app[bot]
Merge PR #21889: Stop relying on canonical names in Native conversion.
committed
Pierre-Marie Pédrot
Stop relying on canonical names in Native conversion.
committed

March 2026

coqbot-app[bot]
Merge PR #21809: VM/native support inductive cumulativity
committed
Gaëtan Gilbert
VM/native support inductive cumulativity
committed

January 2026

coqbot-app[bot]
Merge PR #21508: Stop unifying sorts in the kernel.
committed
Pierre-Marie Pédrot
Simplify quality APIs that do not require a QGraph anymore.
committed
coqbot-app[bot]
Merge PR #21449: Centralize the Nativenorm global state in a reference-passed record
committed
Pierre-Marie Pédrot
Pass Nativecode symbols by reference.
committed

November 2025

coqbot-app[bot]
Merge PR #21272: Instances-mod-elim-constraints
committed
Yann Leray
Conversion mod qgraph
committed
Yann Leray
Instances mod elim (wrong graph)
committed
Yann Leray
Revert qnorm
committed

October 2025

coqbot-app[bot]
Merge PR #20506: An elimination constraint graph to manage elimination of sort variables
committed
Johann Rosain
Use elimination graph at elaboration
committed
coqbot-app[bot]
Merge PR #21165: Add qnorm function to conversion and cclosure
committed
Yann Leray
Add quality normalisation function to conversion and cclosure
committed

June 2025

coqbot-app[bot]
Merge PR #20719: Tweak the native compilation scheme of cofixpoints.
committed
Pierre-Marie Pédrot
Tweak the native compilation scheme of cofixpoints.
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
coqbot-app[bot]
Merge PR #19120: Use algebraic datatypes to signal failure in Conversion API
committed
Pierre-Marie Pédrot
Parameterize the type of errors in conversion API.
committed
Pierre-Marie Pédrot
Remove the NotConvertible error from the Conversion API.
committed
Pierre-Marie Pédrot
Return an algebraic error out of kernel conversion functions.
committed
Pierre-Marie Pédrot
Stop relying on exceptions for universe unification in Conversion API.
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

May 2023

coqbot-app[bot]
Merge PR #17585: Revised warning API: warnings can have multiple categories
committed
Gaëtan Gilbert
Revised warning API: warnings can have multiple categories
committed
coqbot-app[bot]
Merge PR #17453: Kernel: split reduction.ml to have conversion-related functions in conversion.ml
committed

April 2023

Gaëtan Gilbert
Kernel: split reduction.ml to have conversion-related functions in conversion.ml
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
coqbot-app[bot]
Merge PR #16671: Share the VM and native lambda AST in a single type.
committed

October 2022

Pierre-Marie Pédrot
Share the VM and native lambda AST in a single type.
committed
Pierre-Marie Pédrot
Introduce a Lmeta node in the VM lambda representation.
committed
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
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
coqbot-app[bot]
Merge PR #16651: Fix the conversion of Prod values in the native compiler.
committed
Pierre-Marie Pédrot
Merge the Acofix and Acofixe constructors of native atoms.
committed
Pierre-Marie Pédrot
Fix the conversion of Prod values in the native compiler.
committed
coqbot-app[bot]
Merge PR #16574: Non rectypes Nativevalues.t using GADT
committed