From 52a844dc9419223c9e72a6be43b9657e4d7f1f5f Mon Sep 17 00:00:00 2001
From: letouzey
Date: Wed, 17 Apr 2013 15:58:27 +0000
Subject: Coqc: repair localisation of errors in files

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16418 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 toplevel/vernac.ml | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 84968c3d44..e037944f26 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -344,8 +344,9 @@ let rec vernac_com interpfun checknav (loc,com) =
     with reraise ->
       let reraise = Errors.push reraise in
       Format.set_formatter_out_channel stdout;
-      if Loc.is_ghost loc || Loc.get_loc reraise != None then raise reraise
-      else Loc.raise loc reraise
+      let loc' = Option.default Loc.ghost (Loc.get_loc reraise) in
+      if Loc.is_ghost loc' then Loc.raise loc reraise
+      else raise reraise
 
 and read_vernac_file verbosely s =
   Flags.make_warn verbosely;
-- 
cgit v1.2.3