aboutsummaryrefslogtreecommitdiff
path: root/plugins/ltac/tacsubst.ml
AgeCommit message (Expand)Author
2017-03-15Attempt to improve error message when "apply in" fail.Hugo Herbelin
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