aboutsummaryrefslogtreecommitdiff
path: root/test-suite/output/Errors.v
AgeCommit message (Expand)Author
2019-02-05Unset the Ltac backtrace printing by default.Pierre-Marie Pédrot
2018-10-04Test-suite: avoid explicit references to “Top”Vincent Laporte
2018-10-04test-suite: cleaningVincent Laporte
2018-03-24Slightly refining some error messages about unresolvable evars.Hugo Herbelin
2016-07-13Fixing printing of evar name in an error message of instantiate.Hugo Herbelin
2013-02-17Revised the Ltac trace mechanism so that trace breaking due toherbelin
2010-10-03Test for non-regression of the display bug fixed in r13486.herbelin