aboutsummaryrefslogtreecommitdiff
path: root/test-suite/ltac2/compat.v
AgeCommit message (Expand)Author
2020-11-30Add test for this new function.Pierre-Marie Pédrot
2019-06-25Give a functional type to Ltac1 quotations with a context.Pierre-Marie Pédrot
2019-06-25Adding the ability to transfer Ltac2 variables to Ltac1 quotations.Pierre-Marie Pédrot
2019-05-07Integrate build and documentation of Ltac2Maxime Dénès