aboutsummaryrefslogtreecommitdiff
path: root/test-suite/output/Errors.v
AgeCommit message (Collapse)Author
2019-02-05Unset the Ltac backtrace printing by default.Pierre-Marie Pédrot
This is only used for debugging, if a user wants more feedback she can turn on the option. Conversely, it has a cost for any tactic script, so it is wiser to disable it by default.
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
For instance, error in "Goal forall a f, f a = 0" is now located.
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
interleaving of ltac and ml code is not visible (this particularly applies to ltac notation ring, which calls ml-level ring_lookup and Ring again at the ltac level, resulting in non-localisation of "ring" errors). Added also missing LtacLocated checks in Class_instance and Proofview. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16204 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-10-03Test for non-regression of the display bug fixed in r13486.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13487 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 17:24:19 +0000