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.mli | 1 +
 1 file changed, 1 insertion(+)

(limited to 'lib/loc.mli')

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