Better exception handling in TACTIC EXTEND and VERNAC EXTEND (fix #2797)

If an EXTEND block triggers an exception, the current behavior
is to print the exception (with Errors.print) ... and continue
as if nothing happened.

It's tempting to stop ignoring this exception, but that would currently
break ssreflect. For the moment, we simply display a nicer message
as suggested in bug #2797:
 - the message starts with Warning instead of Error, and ends with a \n
 - it also embeds the name of the concerned EXTEND block

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15607 85f007b7-540e-0410-9357-904b9bb8a0f7

0 files changed, 0 insertions, 0 deletions