aboutsummaryrefslogtreecommitdiff
path: root/user-contrib/Ltac2/tac2intern.ml
AgeCommit message (Expand)Author
2019-10-29Fix #10615: Notation substitution for Ltac2 terms.Pierre-Marie Pédrot
2019-10-18Allow to pass Ltac1 values to Ltac2 quotations.Pierre-Marie Pédrot
2019-06-17Update headers of files that were stuck on older headers.Théo Zimmermann
2019-06-08Fix #10339: Anomaly in Ltac2.Pierre-Marie Pédrot
2019-05-07Integrate build and documentation of Ltac2Maxime Dénès