aboutsummaryrefslogtreecommitdiff
path: root/user-contrib/Ltac2/Ltac1.v
AgeCommit message (Expand)Author
2021-03-26Add an Ltac1 to Ltac2 FFI for identifiers.Pierre-Marie Pédrot
2020-11-30Add an abstraction function in the LtacX FFI.Pierre-Marie Pédrot
2020-03-18Update headers in the whole code base.Théo Zimmermann
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