Horrible hack to fix #18516 (refs to section variables in glob files)

This somewhat fixes the refs in glob files in many cases but is still
buggy. For instance, the following still fails:

Section Sec.
Context (foo : forall x, x <> 0) (bar : bool).
Definition f := bar.
End Sec.

But at least it should work for section variables without binders.

An actual fix would probably require some actual refactoring of the
use of Dumglob.dump_binder at least, which I don't have the time to do
right now.

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

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

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 *)

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