From 158f40db9482ead89befbf9bc9ad45ff8a60b75f Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Tue, 17 Jan 2017 14:23:53 +0100
Subject: [location] Switch glob_constr to Loc.located

---
 lib/loc.ml  | 1 +
 lib/loc.mli | 1 +
 2 files changed, 2 insertions(+)

(limited to 'lib')

diff --git a/lib/loc.ml b/lib/loc.ml
index 8d7432ff4b..2a785fac48 100644
--- a/lib/loc.ml
+++ b/lib/loc.ml
@@ -62,6 +62,7 @@ type 'a located = t * 'a
 
 let to_pair x = x
 let tag ?loc x = Option.default ghost loc, x
+let obj (_,x) = x
 
 let with_loc   f (loc, x) = f ~loc x
 let with_unloc f (_,x) = f x
diff --git a/lib/loc.mli b/lib/loc.mli
index 3f484bc4c3..10f63a8dd7 100644
--- a/lib/loc.mli
+++ b/lib/loc.mli
@@ -60,6 +60,7 @@ type 'a located = t * 'a
 
 val to_pair : 'a located -> t * 'a
 val tag : ?loc:t -> 'a -> 'a located
+val obj : 'a located -> 'a
 
 val with_loc : (loc:t -> 'a -> 'b) -> 'a located -> 'b
 val with_unloc : ('a -> 'b) -> 'a located -> 'b
-- 
cgit v1.2.3