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

1 files changed, 3 insertions, 2 deletions

diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 84968c3d4..e037944f2 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;