aboutsummaryrefslogtreecommitdiff
path: root/user-contrib/Ltac2/tac2print.ml
AgeCommit message (Expand)Author
2021-01-22Add a type of format strings to Ltac2.Pierre-Marie Pédrot
2020-12-04turn Ltac2's `pattern:` into `pat:`Kenji Maillard
2020-11-25Separate interning and pretyping of universesGaëtan Gilbert
2020-03-18Update headers in the whole code base.Théo Zimmermann
2019-07-07[error] Remove special error printing pre-processingEmilio Jesus Gallego Arias
2019-06-18[errors] remove "is_handled" logic, turn unhandled into anomaliesEmilio Jesus Gallego Arias
2019-06-17Update headers of files that were stuck on older headers.Théo Zimmermann
2019-05-07Integrate build and documentation of Ltac2Maxime Dénès