From d76a3591e091bb0807fa974c4098b32db9e6d1ad Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Wed, 3 Jul 2019 10:29:29 +0200
Subject: Remove unused variable_path (note secpath is still used)

---
 interp/decls.mli | 3 ---
 1 file changed, 3 deletions(-)

(limited to 'interp/decls.mli')

diff --git a/interp/decls.mli b/interp/decls.mli
index ba355999c2..56866aeb43 100644
--- a/interp/decls.mli
+++ b/interp/decls.mli
@@ -67,9 +67,6 @@ type variable_data = {
 
 val add_variable_data : variable -> variable_data -> unit
 
-(* Not used *)
-val variable_path : variable -> DirPath.t
-
 (* Only used in dumpglob *)
 val variable_secpath : variable -> qualid
 val variable_kind : variable -> logical_kind
-- 
cgit v1.2.3