diff options
| author |  Stephane Glondu <steph@glondu.net> | 2010-12-24 12:51:11 +0100 |
|---|---|---|
| committer | Stephane Glondu <steph@glondu.net> | 2010-12-24 12:51:11 +0100 |
| commit | 20d03a28285c430740d0b675583fe5c4d13ffecc (patch) | |
| tree | 36bd87c5c42d948291605fc35b4b7cf573fc8113 /toplevel/vernac.ml | |
| parent | c0a92523eaa76afabcbaf06ac4a7e8f7930ee4a3 (diff) | |
| parent | 50dc9067e98ca001ad2e875011abab5da6fdb621 (diff) | |
Merge commit 'upstream/8.3.pl1+dfsg' into experimental/master
Diffstat (limited to 'toplevel/vernac.ml')
| -rw-r--r-- | toplevel/vernac.ml | 7 |
1 files changed, 3 insertions, 4 deletions
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 |