aboutsummaryrefslogtreecommitdiff
path: root/user-contrib/Ltac2/Std.v
AgeCommit message (Expand)Author
2021-04-08remove `with hintdb` variant of Ltac2 `unify`, becauseSamuel Gruetter
2021-04-07unify for Ltac2Samuel Gruetter
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-06-16Fix #10090: Ltac1 destruct and Ltac2 destruct should do the same thing.Pierre-Marie Pédrot
2019-05-07Integrate build and documentation of Ltac2Maxime Dénès