aboutsummaryrefslogtreecommitdiff
path: root/plugins/syntax/plugin_base.dune
AgeCommit message (Expand)Author
2020-04-11[dune] [stdlib] Build the standard library natively with Dune.Emilio Jesus Gallego Arias
2019-11-01Parsing primitive float constantsPierre Roux
2019-05-03Fix #10054: Numeral Notations without the ltac plugin.Pierre-Marie Pédrot
2019-02-04Primitive integersMaxime Dénès
2018-11-28Add `String Notation` vernacular like `Numeral Notation`Jason Gross
2018-09-05[build] Preliminary support for building Coq with `dune`.Emilio Jesus Gallego Arias