From 1b8ce11a8cca8deca4409fa9e9e2c8d56e9180f2 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 30 May 2020 20:49:33 +0200
Subject: Extraction: At declaration point of a global, use its declaring name.

If we need to print the name of an inlined constant (as in "let name =",
"val name :" or "type name ="), we need its name without inlining nor
qualification.

In particular, we introduce a function pp_global_name to make it
clearer that printing a name at declaration point of a global is only
about printing the basename (formerly, Common.pp_global was correctly
printing the basename without qualification thanks to the
"top_visible_mp ()" test, but OCaml.pp_global was wrongly inlining).
---
 plugins/extraction/common.ml | 7 +++++++
 1 file changed, 7 insertions(+)

(limited to 'plugins/extraction/common.ml')

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 =
-- 
cgit v1.2.3