declare_variable: path is always Lib.cwd()

8 files changed, 23 insertions, 29 deletions

diff --git a/interp/decls.ml b/interp/decls.ml
index ec5d4fa3cb..ef22a393e4 100644
--- a/interp/decls.ml
+++ b/interp/decls.ml
@@ -59,20 +59,19 @@ type logical_kind =
 
 (** Data associated to section variables and local definitions *)
 
-type variable_data =
-  { path:DirPath.t
-  ; opaque: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 add_variable_data id o = vartab := Id.Map.add id (o,Lib.cwd()) !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_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
diff --git a/interp/decls.mli b/interp/decls.mli
index 2a11a271cc..ba355999c2 100644
--- a/interp/decls.mli
+++ b/interp/decls.mli
@@ -60,11 +60,10 @@ type logical_kind =
 
 (** Registration and access to the table of variable *)
 
-type variable_data =
-  { path:DirPath.t
-  ; opaque:bool
-  ; kind:logical_kind
-  }
+type variable_data = {
+  opaque:bool;
+  kind:logical_kind;
+}
 
 val add_variable_data : variable -> variable_data -> unit
 
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index ca19116ef0..c906670dc0 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -128,7 +128,7 @@ let save name const ?hook uctx scope kind =
   let r = match scope with
     | Discharge ->
       let c = SectionLocalDef const in
-      let () = declare_variable ~name ~kind (Lib.cwd(), c) in
+      let () = declare_variable ~name ~kind c in
       VarRef name
     | Global local ->
       let kn = declare_constant ~name ~kind ~local (DefinitionEntry const) in
diff --git a/tactics/declare.ml b/tactics/declare.ml
index 91c55cacb0..c0eae7503c 100644
--- a/tactics/declare.ml
+++ b/tactics/declare.ml
@@ -308,19 +308,17 @@ let declare_private_constant ?role ?(local = ImportDefaultBehavior) ~name ~kind
   kn, eff
 
 (** Declaration of section variables and local definitions *)
-type section_variable_entry =
+type variable_declaration =
   | SectionLocalDef of Evd.side_effects Proof_global.proof_entry
   | SectionLocalAssum of { typ:Constr.types; univs:Univ.ContextSet.t; poly:bool; impl:bool }
 
-type variable_declaration = DirPath.t * section_variable_entry
-
 (* This object is only for things which iterate over objects to find
    variables (only Prettyp.print_context AFAICT) *)
 let inVariable : unit -> obj =
   declare_object { (default_object "VARIABLE") with
     classify_function = (fun () -> Dispose)}
 
-let declare_variable ~name ~kind (path,d) =
+let declare_variable ~name ~kind d =
   (* Constr raisonne sur les noms courts *)
   if Decls.variable_exists name then
     raise (AlreadyDeclared (None, name));
@@ -359,7 +357,7 @@ let declare_variable ~name ~kind (path,d) =
   in
   Nametab.push (Nametab.Until 1) (Libnames.make_path DirPath.empty name) (GlobRef.VarRef name);
   add_section_variable ~name ~kind:impl ~poly univs;
-  Decls.(add_variable_data name {path;opaque;kind});
+  Decls.(add_variable_data name {opaque;kind});
   add_anonymous_leaf (inVariable ());
   Impargs.declare_var_implicits name;
   Notation.declare_ref_arguments_scope Evd.empty (GlobRef.VarRef name)
diff --git a/tactics/declare.mli b/tactics/declare.mli
index 3edb3f29cd..89b41076f7 100644
--- a/tactics/declare.mli
+++ b/tactics/declare.mli
@@ -21,7 +21,7 @@ open Entries
 
 (** Declaration of local constructions (Variable/Hypothesis/Local) *)
 
-type section_variable_entry =
+type variable_declaration =
   | SectionLocalDef of Evd.side_effects Proof_global.proof_entry
   | SectionLocalAssum of { typ:types; univs:Univ.ContextSet.t; poly:bool; impl:bool }
 
@@ -30,8 +30,6 @@ type 'a constant_entry =
   | ParameterEntry of parameter_entry
   | PrimitiveEntry of primitive_entry
 
-type variable_declaration = DirPath.t * section_variable_entry
-
 val declare_variable
   :  name:variable
   -> kind:Decls.logical_kind
diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml
index 520df1c21e..c561d4a2a4 100644
--- a/vernac/comAssumption.ml
+++ b/vernac/comAssumption.ml
@@ -51,7 +51,7 @@ match scope with
     | Polymorphic_entry (_, univs) -> Univ.ContextSet.of_context univs
   in
   let kind = Decls.IsAssumption kind in
-  let decl = Lib.cwd(), SectionLocalAssum {typ; univs; poly; impl} in
+  let decl = SectionLocalAssum {typ; univs; poly; impl} in
   let () = declare_variable ~name ~kind decl in
   let () = assumption_message name in
   let r = VarRef name in
diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml
index 2aa96fa8ed..69338c0ba6 100644
--- a/vernac/declareDef.ml
+++ b/vernac/declareDef.ml
@@ -49,7 +49,7 @@ let declare_definition ~name ~scope ~kind ?hook_data udecl ce imps =
   let gr = match scope with
   | Discharge ->
       let () =
-        declare_variable ~name ~kind:Decls.(IsDefinition kind) (Lib.cwd(), SectionLocalDef ce)
+        declare_variable ~name ~kind:Decls.(IsDefinition kind) (SectionLocalDef ce)
       in
       VarRef name
   | Global local ->
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index d6ee0b96f2..ea735dd7f9 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -266,7 +266,7 @@ let save_remaining_recthms env sigma ~poly ~scope norm univs body opaq i
           | Monomorphic_entry univs -> univs
         in
         let c = Declare.SectionLocalAssum {typ=t_i; univs; poly; impl} in
-        let () = Declare.declare_variable ~name ~kind (Lib.cwd(),c) in
+        let () = Declare.declare_variable ~name ~kind c in
         (VarRef name,impargs)
       | Global local ->
         let kind = Decls.(IsAssumption Conjectural) in
@@ -289,7 +289,7 @@ let save_remaining_recthms env sigma ~poly ~scope norm univs body opaq i
       | Discharge ->
         let const = Declare.definition_entry ~types:t_i ~opaque:opaq ~univs body_i in
         let c = Declare.SectionLocalDef const in
-        let () = Declare.declare_variable ~name ~kind (Lib.cwd(), c) in
+        let () = Declare.declare_variable ~name ~kind c in
         (VarRef name,impargs)
       | Global local ->
         let const = Declare.definition_entry ~types:t_i ~univs ~opaque:opaq body_i in
@@ -499,7 +499,7 @@ let finish_proved env sigma idopt po info =
       let r = match scope with
         | Discharge ->
           let c = Declare.SectionLocalDef const in
-          let () = Declare.declare_variable ~name ~kind (Lib.cwd(), c) in
+          let () = Declare.declare_variable ~name ~kind c in
           let () = if should_suggest
             then Proof_using.suggest_variable (Global.env ()) name
           in