aboutsummaryrefslogtreecommitdiffhomepage
path: root/API/grammar_API.mli
Commit message (Expand)AuthorAge
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* Merge PR#719: Constrexpr.Numeral without bigintGravatar Maxime Dénès2017-06-15
|\
* | API: exports Mltop.module_is_known to both API.mli and grammar_API.mliGravatar Pierre Letouzey2017-06-14
| * G_prim: the bigint entry keeps numbers in raw stringsGravatar Pierre Letouzey2017-06-14
|/
* Put "ssreflect" behind "API".Gravatar Matej Košík2017-06-07
* Put all plugins behind an "API".Gravatar Matej Kosik2017-06-07