aboutsummaryrefslogtreecommitdiff
path: root/plugins/ltac/tacintern.ml
AgeCommit message (Expand)Author
2017-02-27Merge PR#395: Allow hintdb to be parameters in a Ltac definition orMaxime Dénès
2017-02-17Ltac as a plugin.Pierre-Marie Pédrot