diff options
| author | Gaëtan Gilbert | 2019-07-03 10:29:29 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-07-03 17:05:29 +0200 |
| commit | d76a3591e091bb0807fa974c4098b32db9e6d1ad (patch) | |
| tree | aec688065f660a00d1d2da28b0030b88c2ecbad9 /interp/decls.mli | |
| parent | 6e22817c6dab5043f1bdcbb1a1c8da281d4b3d7b (diff) | |
Remove unused variable_path (note secpath is still used)
Diffstat (limited to 'interp/decls.mli')
| -rw-r--r-- | interp/decls.mli | 3 |
1 files changed, 0 insertions, 3 deletions
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 |