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

Now it is a private field, locations are optional.
---
 intf/glob_term.mli | 9 +++++----
 1 file changed, 5 insertions(+), 4 deletions(-)

(limited to 'intf')

diff --git a/intf/glob_term.mli b/intf/glob_term.mli
index a8311e0934..5aa5bdeebe 100644
--- a/intf/glob_term.mli
+++ b/intf/glob_term.mli
@@ -79,10 +79,11 @@ and cases_clause = (Id.t list * cases_pattern list * glob_constr) Loc.located
     of [t] are members of [il]. *)
 and cases_clauses = cases_clause list
 
-type extended_glob_local_binder =
-  | GLocalAssum of Loc.t * Name.t * binding_kind * glob_constr
-  | GLocalDef of Loc.t * Name.t * binding_kind * glob_constr * glob_constr option
-  | GLocalPattern of Loc.t * (cases_pattern * Id.t list) * Id.t * binding_kind * glob_constr
+type extended_glob_local_binder_r =
+  | GLocalAssum   of Name.t * binding_kind * glob_constr
+  | GLocalDef     of Name.t * binding_kind * glob_constr * glob_constr option
+  | GLocalPattern of (cases_pattern * Id.t list) * Id.t * binding_kind * glob_constr
+and extended_glob_local_binder = extended_glob_local_binder_r Loc.located
 
 (** A globalised term together with a closure representing the value
     of its free variables. Intended for use when these variables are taken
-- 
cgit v1.2.3