Merge PR #12851: Extraction: At declaration point of a global, use its declaring name

Reviewed-by: maximedenes

1 files changed, 7 insertions, 0 deletions

diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml
index 4a41f4c890..d215a7673d 100644
--- a/plugins/extraction/common.ml
+++ b/plugins/extraction/common.ml
@@ -604,6 +604,13 @@ let pp_global k r =
       | Haskell -> if modular () then pp_haskell_gen k mp rls else s
       | Ocaml -> pp_ocaml_gen k mp rls (Some l)
 
+(* Main name printing function for declaring a reference *)
+
+let pp_global_name k r =
+  let ls = ref_renaming (k,r) in
+  assert (List.length ls > 1);
+  List.hd ls
+
 (* The next function is used only in Ocaml extraction...*)
 
 let pp_module mp =