aboutsummaryrefslogtreecommitdiff
path: root/interp/notation_term.ml
AgeCommit message (Expand)Author
2020-11-20Add preliminary support for notations with large class (non-recursive) binders.Hugo Herbelin
2020-07-06Primitive persistent arraysMaxime Dénès
2020-03-18Update headers in the whole code base.Théo Zimmermann
2019-11-01Add primitive float computation in Coq kernelGuillaume Bertholon
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2019-04-16Clean the representation of recursive annotation in ConstrexprMaxime Dénès
2019-02-04Primitive integersMaxime Dénès
2018-12-09[doc] Enable Warning 50 [incorrect doc comment] and fix comments.Emilio Jesus Gallego Arias
2018-10-02Revert #6651: Use r.(p) syntax to print primitive projectionsMaxime Dénès
2018-07-29Adding support for custom entries in notations.Hugo Herbelin
2018-06-12[api] Misctypes removal: several moves:Emilio Jesus Gallego Arias
2018-05-31[notations] Split interpretation and parsing of notationsEmilio Jesus Gallego Arias
2018-05-04[api] Rename `global_reference` to `GlobRef.t` to follow kernel style.Emilio Jesus Gallego Arias
2018-04-23[api] Relocate `intf` modules according to dependency-order.Emilio Jesus Gallego Arias
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 14:29:04 +0000