aboutsummaryrefslogtreecommitdiff
path: root/test-suite/output/ltac_missing_args.v
AgeCommit message (Collapse)Author
2017-08-21Ensuring all .v files end with a newline to make "sed -i" work better on them.Hugo Herbelin
2017-03-14Report missing tactic arguments in error messageTej Chajed
Augments "A fully applied tactic is expected" with the list of missing arguments to the tactic. Addresses [bug 5344](https://coq.inria.fr/bugs/show_bug.cgi?id=5344).