aboutsummaryrefslogtreecommitdiff
path: root/test-suite/output/ltac_missing_args.v
AgeCommit message (Expand)Author
2019-02-05Unset the Ltac backtrace printing by default.Pierre-Marie Pédrot
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