aboutsummaryrefslogtreecommitdiff
path: root/test-suite/output/auto.v
AgeCommit message (Collapse)Author
2020-05-30Remove info tactic, deprecated in 8.5Jim Fehrle
2017-09-19Fixing bug #5741 (anomaly in info_trivial).Hugo Herbelin
The bug was introduced in 1559f73.
2016-11-19Tests for info/debug auto/eauto.Hugo Herbelin
This is while waiting for a deeper uniformization of auto, eauto, and typeclasses eauto. Incidentally includes a little fix in harmonizing auto/eauto printing.