Extraction: global reference should be indexed on their user part (fix #2540)

 Since in Extract_env we recreate constant and mind whose canonical part
 might be inaccurate, we shouldn't use an Hashtbl on global_reference
 derived from these constant and mind, otherwise equivalent refs could be
 considered distinct.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14141 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 14 insertions, 4 deletions

diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml
index 35873f5a9b..66ec446f03 100644
--- a/plugins/extraction/common.ml
+++ b/plugins/extraction/common.ml
@@ -175,6 +175,16 @@ let mktable autoclean =
   if autoclean then register_cleanup (fun () -> Hashtbl.clear h);
   (Hashtbl.add h, Hashtbl.find h, fun () -> Hashtbl.clear h)
 
+(* We might have built [global_reference] whose canonical part is
+   inaccurate. We must hence compare only the user part,
+   hence using a Hashtbl might be incorrect *)
+
+let mktable_ref autoclean =
+  let m = ref Refmap'.empty in
+  let clear () = m := Refmap'.empty in
+  if autoclean then register_cleanup clear;
+  (fun r v -> m := Refmap'.add r v !m), (fun r -> Refmap'.find r !m), clear
+
 (* A table recording objects in the first level of all MPfile *)
 
 let add_mpfiles_content,get_mpfiles_content,clear_mpfiles_content =
@@ -351,10 +361,10 @@ let ref_renaming_fun (k,r) =
 (* Cached version of the last function *)
 
 let ref_renaming =
-  let add,get,_ = mktable true in
-  fun x ->
-    try if is_mp_bound (base_mp (modpath_of_r (snd x))) then raise Not_found; get x
-    with Not_found -> let y = ref_renaming_fun x in add x y; y
+  let add,get,_ = mktable_ref true in
+  fun ((k,r) as x) ->
+    try if is_mp_bound (base_mp (modpath_of_r r)) then raise Not_found; get r
+    with Not_found -> let y = ref_renaming_fun x in add r y; y
 
 (* [visible_clash mp0 (k,s)] checks if [mp0-s] of kind [k]
    can be printed as [s] in the current context of visible