coq
forked from coq/coq
Star 1
Fork 0
Watch

Version history of kernel/nativelibrary.ml

January 2026

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
Pierre-Marie Pédrot
Move the Nativecode name counter to the local state.
committed
Pierre-Marie Pédrot
Centralize the Nativenorm global state in a reference-passed record.
committed

October 2025

coqbot-app[bot]
Merge PR #21174: Deprecate Names.Label
committed
Gaëtan Gilbert
Deprecate Names.Label
committed

July 2025

coqbot-app[bot]
Merge PR #20948: Do not overwrite modules in native compilation.
committed
Pierre-Marie Pédrot
Do not overwrite modules in native compilation.
committed

January 2025

coqbot-app[bot]
Merge PR #20124: Stronger invariants in delta resolvers.
committed
Pierre-Marie Pédrot
Stronger invariants in delta resolvers.
committed
coqbot-app[bot]
Merge PR #20060: Stop storing the module path in modules.
committed
Pierre-Marie Pédrot
Stop storing the module path in modules.
committed
coqbot-app[bot]
Merge PR #20058: Ensure at runtime that the modpath is synced with module bodies and types
committed
Pierre-Marie Pédrot
Ensure at runtime that the modpath is synced with module bodies and types.
committed
coqbot-app[bot]
Merge PR #19995: Abstract away the representation of module-related types
committed
Pierre-Marie Pédrot
Abstract away the various types of modules.
committed
Pierre-Marie Pédrot
Move the module-related definitions from Declarations to a new module.
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

February 2024

coqbot-app[bot]
Merge PR #18038: Add rewrite rules to Coq
committed
Yann Leray
Apply review suggestions
committed
Yann Leray
Add minimal support for native and checker for rewrite rules
committed
Yann Leray
Add symbols, patterns, rewrite rule fields
committed

May 2021

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

March 2021

coqbot-app[bot]
Merge PR #13956: Remove useless prefix argument in native compilation.
committed
Pierre-Marie Pédrot
Remove useless prefix argument in native compilation.
committed

February 2021

coqbot-app[bot]
Merge PR #13202: Infrastructure for fine-grained debug flags
committed
Maxime Dénès
Infrastructure for fine-grained debug flags
committed

March 2020

Hugo Herbelin
Merge PR #11559: Remove year in headers.
committed
Théo Zimmermann
Update headers in the whole code base.
committed

November 2019

Gaëtan Gilbert
Merge PR #11010: [coq] Untabify the whole ML codebase.
committed
Emilio Jesus Gallego Arias
[coq] Untabify the whole ML codebase.
committed

June 2019

Clément Pit-Claudel
Merge PR #10320: Update headers to the new year.
committed
Théo Zimmermann
Update ml-style headers to new year.
committed

October 2018

Pierre-Marie Pédrot
Merge PR #8555: Remove section paths from kernel names
committed
Maxime Dénès
[kernel] Remove section paths from `KerName.t`
committed

September 2018

Maxime Dénès
Merge PR #8534: Checking if low-level name printers are used on purpose or not
committed
Hugo Herbelin
Checking if low-level name printers are used on purpose or not.
committed

July 2018

Pierre-Marie Pédrot
Merge PR #7746: Many small cleanups removing unused arguments and functions
committed
Gaëtan Gilbert
Nativecode compile_mind, compile_mind_field: remove unused arguments
committed

May 2018

Pierre-Marie Pédrot
Merge PR #7521: Fix soundness bug with VM/native and cofixpoints
committed
Maxime Dénès
Unify pre_env and env
committed

March 2018

Maxime Dénès
Merge PR #6855: Update headers following #6543.
committed

February 2018

Théo Zimmermann
Update headers following #6543.
committed

November 2017

Maxime Dénès
Merge PR #6065: [api] Deprecate all legacy uses of Names in core.
committed
Emilio Jesus Gallego Arias
[api] Deprecate all legacy uses of Names in core.
committed

July 2017

Pierre-Marie Pédrot
Bump year in headers.
committed

June 2017

Maxime Dénès
Merge PR#713: Bump year in headers.
committed
Maxime Dénès
Bump year in headers.
committed

May 2016

Pierre-Marie Pédrot
This patch splits pretty printing representation from IO operations.
committed