aboutsummaryrefslogtreecommitdiff
path: root/theories/Init/Byte.v
AgeCommit message (Expand)Author
2020-11-05Merge numeral and string notation pluginsPierre Roux
2020-04-21Moving the main Require Export Ltac in Prelude.v.Hugo Herbelin
2020-03-18Update headers in the whole code base.Théo Zimmermann
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2018-11-28Byte.v: use right-associative tuples in bitsJason Gross
2018-11-28Speed up ByteJason Gross
2018-11-28Add `String Notation` vernacular like `Numeral Notation`Jason Gross