From ee3c7ddaf0ab726594b278d30430123cd60e63fa Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 3 Oct 2010 22:27:05 +0000
Subject: Avoid raising an anomaly when an error encapsulated with a dummy
 location is raised from a loaded/compiled file!

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

diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index aef772676e..57fa29e162 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -43,7 +43,7 @@ let raise_with_file file exc =
           ((b, f, loc), e)
       | Loc.Exc_located (loc, e) when loc <> dummy_loc ->
           ((false,file, loc), e)
-      | _ -> ((false,file,cmdloc), re)
+      | Loc.Exc_located (_, e) | e -> ((false,file,cmdloc), e)
   in
   raise (Error_in_file (file, inner, disable_drop inex))
 
-- 
cgit v1.2.3