coq
forked from coq/coq
Star 1
Fork 0
Watch

Version history of kernel/retroknowledge.ml

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
Add a primitive string type.
committed

May 2021

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

January 2021

Pierre-Marie Pédrot
Merge PR #13454: Remove unused retro_refl
committed

November 2020

Gaëtan Gilbert
Remove unused retro_refl
committed

July 2020

Pierre-Marie Pédrot
Merge PR #11604: Primitive persistent arrays
committed
Maxime Dénès
Primitive persistent arrays
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

Maxime Dénès
Merge PR #9867: Add primitive floats (binary64 floating-point numbers)
committed
Pierre Roux
Implement classify on primitive float
committed
Pierre Roux
Change return type of primitive float comparison
committed
Guillaume Bertholon
Add primitive float computation in Coq kernel
committed
Pierre Roux
Declare type of primitives in CPrimitives
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 2019

Vincent Laporte
Merge PR #9627: Small retroknowledge/primitive cleanup
committed
Gaëtan Gilbert
Remove unused Retroknowledge.Register_inline
committed

February 2019

Pierre-Marie Pédrot
Merge PR #6914: Primitive integers
committed
Maxime Dénès
Primitive integers
committed

September 2018

Pierre-Marie Pédrot
Merge PR #8447: Cleaning in the retroknowledge
committed
Vincent Laporte
Register: simpler syntax
committed
Vincent Laporte
Retroknowledge: use GlobRef.t instead of Constr.t as entry
committed
Vincent Laporte
Retroknowledge: simpler parsing rules
committed
Vincent Laporte
Retroknowledge.KInt31: remove the (unused) group parameter
committed

July 2018

Pierre-Marie Pédrot
Merge PR #8066: [ltac] Remove unused functions.
committed
Emilio Jesus Gallego Arias
[ltac] Remove unused functions / constructors.
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
Maxime Dénès
Merge PR #6784: New IR in VM: Clambda
committed
Maxime Dénès
New IR in VM: Clambda.
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
William Lawvere
Merge remote-tracking branch 'upstream/trunk' into trunk
committed
Maxime Dénès
Merge PR#718: API cleanup: aliases
committed
Matej Košík
Remove (useless) aliases from the API.
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

January 2015

Maxime Dénès
Update headers.
committed

October 2014

Maxime Dénès
Fix segfault in native compiler on int31 division.
committed

September 2014

Arnaud Spiwack
Make the retroknowledge marshalable.
committed

August 2014

Jason Gross
"allows to", like "allowing to", is improper
committed

April 2014

Maxime Dénès
Machine arithmetic operations for native compiler.
committed
Maxime Dénès
Full support for int31 values in native compiler.
committed