aboutsummaryrefslogtreecommitdiff
path: root/plugins/ltac/tacintern.ml
AgeCommit message (Expand)Author
2017-04-27Remove some unused values and typesGaetan Gilbert
2017-03-15Attempt to improve error message when "apply in" fail.Hugo Herbelin
2017-03-14Merge PR#432: [cleanup] Change Id.t option to Name.t in TacFunMaxime Dénès
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