From 6b691bbd2101fd39395c0d2135fd7c06a8915e14 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Fri, 24 Dec 2010 11:53:29 +0100 Subject: Imported Upstream version 8.3pl1 --- toplevel/vernac.ml | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) (limited to 'toplevel/vernac.ml') diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index a00efc5c..9464d763 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: vernac.ml 13488 2010-10-03 22:27:05Z herbelin $ *) +(* $Id: vernac.ml 13668 2010-12-02 17:43:59Z herbelin $ *) (* Parsing of vernacular. *) @@ -34,8 +34,7 @@ exception HasNotFailed let raise_with_file file exc = let (cmdloc,re) = match exc with - | DuringCommandInterp(loc,e) - | DuringSyntaxChecking(loc,e) -> (loc,e) + | DuringCommandInterp(loc,e) -> (loc,e) | e -> (dummy_loc,e) in let (inner,inex) = @@ -171,7 +170,7 @@ let rec vernac_com interpfun (loc,com) = | e -> (* if [e] is an anomaly, the next function will re-raise it *) let msg = Cerrors.explain_exn_no_anomaly e in - msgnl (str "The command has indeed failed with message:" ++ + if_verbose msgnl (str "The command has indeed failed with message:" ++ fnl () ++ str "=> " ++ hov 0 msg) end -- cgit v1.2.3