aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/output/ltac_extra_args.v
Commit message (Collapse)AuthorAge
* Report missing arguments in error messageGravatar Tej Chajed2017-09-21
Augment the "Illegal tactic application" error message with the number of extra arguments passed. Fixes BZ#5753.