diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 8e80a9e38f431..5f19bb44b7969 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -57,9 +57,11 @@ type var_internalization_type =
 
 type var_unique_id = string
 
+(* dumpglob for binders should probably just not happen in contrintern *)
 let var_uid =
   let count = ref 0 in
-  fun id -> incr count; Id.to_string id ^ ":" ^ string_of_int !count
+  fun id -> incr count; Decls.set_variable_uid !count;
+    Id.to_string id ^ ":" ^ string_of_int !count
 
 type var_internalization_data =
     (* type of the "free" variable, for coqdoc, e.g. while typing the
diff --git a/interp/decls.ml b/interp/decls.ml
index a9f40d7bd6420..f16a2a3684982 100644
--- a/interp/decls.ml
+++ b/interp/decls.ml
@@ -12,7 +12,6 @@
      associated declarations *)
 
 open Names
-open Libnames
 
 type theorem_kind =
   | Theorem
@@ -65,16 +64,21 @@ type variable_data = {
 }
 
 let vartab =
-  Summary.ref (Id.Map.empty : (variable_data*DirPath.t) Id.Map.t) ~name:"VARIABLE"
+  Summary.ref (Id.Map.empty : (variable_data*int) Id.Map.t) ~name:"VARIABLE"
 
-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_uid = ref []
+let set_variable_uid uid = variable_uid := !variable_uid @ [uid]
+let add_variable_data id o =
+  let uid = match !variable_uid with
+    | [] -> 0
+    | uid :: l -> variable_uid := l; uid in
+  vartab := Id.Map.add id (o,uid) !vartab
 
 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 = Id.Map.find id !vartab in
-  make_qualid dir id
+let variable_uid id =
+  let _, uid = Id.Map.find id !vartab in
+  uid
 
 let variable_exists id = Id.Map.mem id !vartab
diff --git a/interp/decls.mli b/interp/decls.mli
index 57ea678a13bb8..39b2311ddfdad 100644
--- a/interp/decls.mli
+++ b/interp/decls.mli
@@ -9,7 +9,6 @@
 (************************************************************************)
 
 open Names
-open Libnames
 
 type theorem_kind =
   | Theorem
@@ -68,7 +67,8 @@ type variable_data = {
 val add_variable_data : variable -> variable_data -> unit
 
 (* Only used in dumpglob *)
-val variable_secpath : variable -> qualid
+val set_variable_uid : int -> unit
+val variable_uid : variable -> int
 val variable_kind : variable -> logical_kind
 
 (* User in Lemma, Very dubious *)
diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml
index adb405e2f8768..83ecd996a7be7 100644
--- a/interp/dumpglob.ml
+++ b/interp/dumpglob.ml
@@ -175,7 +175,9 @@ let dump_reference ?loc modpath ident ty =
   dump_ref ?loc filepath modpath ident ty
 
 let dump_secvar ?loc id =
-  dump_reference ?loc "<>" (Libnames.string_of_qualid (Decls.variable_secpath id)) "var"
+  let uid = Decls.variable_uid id in
+  let id = Names.Id.to_string id ^ ":" ^ string_of_int uid in
+  dump_reference ?loc "<>" id "var"
 
 let dump_modref ?loc mp ty =
   let (dp, l) = Lib.split_modpath mp in