aboutsummaryrefslogtreecommitdiff
path: root/plugins/syntax/int31_syntax.ml
AgeCommit message (Expand)Author
2019-02-04Primitive integersMaxime Dénès
2018-09-19Fix Numeral Notations (4/4 - fixing synch)Jason Gross
2018-08-31Make Numeral Notation obey Local/GlobalJason Gross
2018-08-31prim notations backtrackable, their declarations now in two parts (API change)Pierre Letouzey
2018-05-04[api] Rename `global_reference` to `GlobRef.t` to follow kernel style.Emilio Jesus Gallego Arias
2018-02-27Update headers following #6543.Théo Zimmermann
2017-09-04Making detyping potentially lazy.Pierre-Marie Pédrot
2017-07-17[API] Remove `open API` in ml files in favor of `-open API` flag.Emilio Jesus Gallego Arias
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-06-13BigNums: remove files about BigN,BigZ,BigQ (now in an separate git repo)Pierre Letouzey