diff options
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 |