From 30d3515546cf244837c6340b6b87c5f51e68cbf4 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias <e+git@x80.org>
Date: Tue, 17 Jan 2017 23:40:35 +0100
Subject: [location] Remove Loc.ghost.

Now it is a private field, locations are optional.
---
 vernac/explainErr.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'vernac/explainErr.ml')

diff --git a/vernac/explainErr.ml b/vernac/explainErr.ml
index 04841c922..ed2dd274a 100644
--- a/vernac/explainErr.ml
+++ b/vernac/explainErr.ml
@@ -119,6 +119,6 @@ let process_vernac_interp_error ?(allow_uncaught=true) (exc, info) =
   in
   match e' with
   | None -> e
-  | Some (None, loc) -> (fst e, Loc.add_loc (snd e) loc)
-  | Some (Some msg, loc) ->
+  | Some (loc, None) -> (fst e, Loc.add_loc (snd e) loc)
+  | Some (loc, Some msg) ->
     (EvaluatedError (msg, Some (fst e)), Loc.add_loc (snd e) loc)
-- 
cgit v1.2.3