aboutsummaryrefslogtreecommitdiff
path: root/test-suite/output/ltac_missing_args.out
AgeCommit message (Expand)Author
2018-09-23Checking if low-level name printers are used on purpose or not.Hugo Herbelin
2017-11-28more complete not-fully-applied error messages, #6145Paul Steckler
2017-03-21[pp] Make feedback the only logging mechanism.Emilio Jesus Gallego Arias
2017-03-14Report missing tactic arguments in error messageTej Chajed