Merge PR #10461: Simplify Declare.declare_variable

Reviewed-by: ejgallego
Reviewed-by: maximedenes
Reviewed-by: ppedrot

1 files changed, 10 insertions, 15 deletions

diff --git a/interp/decls.ml b/interp/decls.ml
index b802dbe9c3..d9d33b5e0b 100644
--- a/interp/decls.ml
+++ b/interp/decls.ml
@@ -59,27 +59,22 @@ type logical_kind =
 
 (** Data associated to section variables and local definitions *)
 
-type variable_data =
-  { path:DirPath.t
-  ; opaque:bool
-  ; univs:Univ.ContextSet.t
-  ; poly:bool
-  ; kind:logical_kind
-  }
+type variable_data = {
+  opaque:bool;
+  kind:logical_kind;
+}
 
 let vartab =
-  Summary.ref (Id.Map.empty : variable_data Id.Map.t) ~name:"VARIABLE"
+  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 !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_context id = let {univs} = Id.Map.find id !vartab in univs
-let variable_polymorphic id = let {poly} = Id.Map.find id !vartab in poly
+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