From 5a9d5ea4e93cd41d4c80453500d231bad9804ffc Mon Sep 17 00:00:00 2001
From: Kilyan Le Gallic <kilyan.legallic@cea.fr>
Date: Mon, 22 Apr 2024 16:51:37 +0200
Subject: [PATCH] [wp] Applied infix conversion only to last element of scopes
 when building name

---
 src/plugins/wp/Why3Import.ml | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

diff --git a/src/plugins/wp/Why3Import.ml b/src/plugins/wp/Why3Import.ml
index 7b4cbf501c1..f1c9457f57a 100644
--- a/src/plugins/wp/Why3Import.ml
+++ b/src/plugins/wp/Why3Import.ml
@@ -56,8 +56,12 @@ let of_infix s =
 
 let construct_acsl_name (id : W.Ident.ident) =
   let (paths,name,scopes) = T.restore_path id in
-  let modscopes = "::" ^ name ^ "::" ^ (String.concat "::" (List.map (of_infix) scopes)) in
-  (String.concat "::" paths) ^ modscopes
+  match List.rev scopes with
+  |  (t::q) ->
+    let modscopes = "::" ^ name ^ "::" ^ (String.concat "::" (List.rev_append q [(of_infix t)])) in
+    (String.concat "::" paths) ^ modscopes
+  | [] -> ""
+
 
 (* For debug only*)
 let pp_id fmt (id: W.Ident.ident) =
-- 
GitLab