diff options
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/decls.ml | 6 | ||||
| -rw-r--r-- | interp/decls.mli | 3 |
2 files changed, 3 insertions, 6 deletions
diff --git a/interp/decls.ml b/interp/decls.ml index ef22a393e4..d9d33b5e0b 100644 --- a/interp/decls.ml +++ b/interp/decls.ml @@ -67,14 +67,14 @@ type variable_data = { let vartab = Summary.ref (Id.Map.empty : (variable_data*DirPath.t) Id.Map.t) ~name:"VARIABLE" -let add_variable_data id o = vartab := Id.Map.add id (o,Lib.cwd()) !vartab +let secpath () = drop_dirpath_prefix (Lib.library_dp()) (Lib.cwd()) +let add_variable_data id o = vartab := Id.Map.add id (o,secpath()) !vartab -let variable_path id = let _,path = Id.Map.find id !vartab in path let variable_opacity id = let {opaque},_ = Id.Map.find id !vartab in opaque let variable_kind id = let {kind},_ = Id.Map.find id !vartab in kind let variable_secpath id = - let dir = drop_dirpath_prefix (Lib.library_dp()) (variable_path id) in + let _, dir = Id.Map.find id !vartab in make_qualid dir id let variable_exists id = Id.Map.mem id !vartab 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 |