aboutsummaryrefslogtreecommitdiff
path: root/intf/constrexpr.ml
AgeCommit message (Expand)Author
2018-04-23[api] Relocate `intf` modules according to dependency-order.Emilio Jesus Gallego Arias
2018-03-09[located] More work towards using CAst.tEmilio Jesus Gallego Arias
2018-03-07Merge PR #6905: Fix make ml-docMaxime Dénès
2018-03-07Merge PR #6790: Allow universe declarations for [with Definition].Maxime Dénès
2018-03-05Change non-documentation comment from ocamldoc stylemrmr1993
2018-03-05Fix formatting of some ocamldoc comments to reduce warningsmrmr1993
2018-03-05Allow universe declarations for [with Definition].Gaëtan Gilbert
2018-02-27Update headers following #6543.Théo Zimmermann
2018-02-22[ast] Improve precision of Ast location recognition in serialization.Emilio Jesus Gallego Arias
2018-02-20Adding support for parsing subterms of a notation as "pattern".Hugo Herbelin
2018-02-20Moving the argument of CProdN/CLambdaN from binder_expr to local_binder_expr.Hugo Herbelin
2018-01-30Use r.(p) syntax to print primitive projections.Maxime Dénès
2017-12-12Removing cumbersome location in multiple patterns.Hugo Herbelin
2017-11-06[api] Move structures deprecated in the API to the core.Emilio Jesus Gallego Arias
2017-09-19Allow declaring universe constraints at definition level.Matthieu Sozeau
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-06-14Constrexpr.Numeral stays uninterpreted (string+sign instead of BigInt.t)Pierre Letouzey
2017-06-07Put all plugins behind an "API".Matej Kosik
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 17:34:46 +0000