coq
forked from coq/coq
Star 1
Fork 0
Watch

Version history of kernel/nativeconv.mli

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 #19120: Use algebraic datatypes to signal failure in Conversion API
committed
Pierre-Marie Pédrot
Parameterize the type of errors in conversion API.
committed

November 2023

coqbot-app[bot]
Merge PR #18340: Fix const_relevance and default qvar handler with sort polymorphism
committed
Gaëtan Gilbert
Move evar_handler type to cclosure and make evar_handler argument implicit
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 #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

March 2020

Hugo Herbelin
Merge PR #11559: Remove year in headers.
committed
Théo Zimmermann
Update headers in the whole code base.
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

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 #6098: [api] Move structures deprecated in the API to the core.
committed
Emilio Jesus Gallego Arias
[api] Move structures deprecated in the API to the 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

April 2016

Pierre Courtieu
Merge remote-tracking branch 'OFFICIAL/trunk' into morefresh
committed

January 2016

Pierre-Marie Pédrot
Merge branch 'v8.5'
committed
Maxime Dénès
Update copyright headers.
committed

December 2015

Matej Kosik
CLEANUP: in the Reduction module
committed

October 2015

Maxime Dénès
Merge branch 'v8.5' into trunk
committed
Maxime Dénès
Fix #4346 2/2: VM casts were not inferring universe constraints.
committed
Maxime Dénès
Fix #4346 1/2: native casts were not inferring universe constraints.
committed

January 2015

Maxime Dénès
Update headers.
committed

March 2014

Pierre Letouzey
Remove many superfluous 'open' indicated by ocamlc -w +33
committed

December 2013

Maxime Dénès
Support for evars and metas in native compiler.
committed

January 2013

mdenes
New implementation of the conversion test, using normalization by evaluation to native OCaml code.
committed