coq
forked from coq/coq
Star 1
Fork 0
Watch

Version history of kernel/cPrimitives.ml

December 2025

coqbot-app[bot]
Merge PR #21195: Add parsing and interpretation of elimination constraints
committed
Johann Rosain
Add support for parsing elimination constraints
committed
Johann Rosain
Rename Constraint(s) to UnivConstraint(s) for a more consistent naming
committed

April 2025

coqbot-app[bot]
Merge PR #20496: Use record instead of tuple for UVars.bound_names
committed
Soudant
Changed bound_names from product to record, with fields quals (for qualities) and univs (for universes),
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
Add a primitive string type.
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
Gaëtan Gilbert
Move universe polymorphism APIs to new file UVars before sort poly
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

July 2021

coqbot-app[bot]
Merge PR #14654: A few terminology changes in module names of the universe API
committed
Hugo Herbelin
Renaming Univ.AUContext into Univ.AbstractContext.
committed
Hugo Herbelin
Renaming module Univ.Constraint into Univ.Constraints.
committed

June 2021

coqbot-app[bot]
Merge PR #13895: Rename Int63 ~> Uint63
committed
Ana
Rename Int63 ~> Uint63
committed

May 2021

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

March 2021

Pierre-Marie Pédrot
Merge PR #14005: Support OCaml primitives with an actual arity larger than 4.
committed
Guillaume Melquiond
Split the return type away from the signature of primitive operations.
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
Maxime Dénès
Primitive persistent arrays
committed

May 2020

Maxime Dénès
Merge PR #12122: Avoid registering as keywords the #... in Primitive
committed

April 2020

Pierre Roux
Remove # keywords in Primitive
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
Erik Martin-Dorel
Add "==", "<", "<=" in PrimFloat.v
committed
Pierre Roux
Add next_{up,down} primitive float functions
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
Nicer error for bad primitive types (through type_errors etc)
committed

February 2019

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

August 2017

Maxime Dénès
Merge PR #965: Moving file primitive.ml to cPrimitive.ml to avoid conflict with OCaml.
committed
Hugo Herbelin
Moving file primitive.ml to cPrimitive.ml to avoid conflict with OCaml.
committed