Fix proverif backend with new naming.

cryspen · Jan 30, 2025 · 051c4eb · 051c4eb
1 parent 0eb63e5
commit 051c4eb
Show file tree

Hide file tree

Showing 3 changed files with 7 additions and 9 deletions.
diff --git a/engine/backends/proverif/proverif_backend.ml b/engine/backends/proverif/proverif_backend.ml
@@ -651,9 +651,8 @@ module Make (Options : OPTS) : MAKE = struct
           fun id ->
             if under_current_ns then print#name_of_concrete_ident id
             else
-              let crate, path = print#namespace_of_concrete_ident id in
-              let full_path = crate :: path in
-              separate_map (underscore ^^ underscore) utf8string full_path
+              let path = print#namespace_of_concrete_ident id in
+              separate_map (underscore ^^ underscore) utf8string path
               ^^ underscore ^^ underscore
               ^^ print#name_of_concrete_ident id
 

diff --git a/engine/lib/deprecated_generic_printer/deprecated_generic_printer.ml b/engine/lib/deprecated_generic_printer/deprecated_generic_printer.ml
@@ -29,11 +29,10 @@ module Make (F : Features.T) (View : Concrete_ident.RENDER_API) = struct
               AlreadyPar
           | _ -> NeedsPar
 
-        method namespace_of_concrete_ident
-            : concrete_ident -> string * string list =
+        method namespace_of_concrete_ident : concrete_ident -> string list =
           fun i ->
             let rendered = View.render i in
-            (rendered.name, rendered.path)
+            rendered.path
 
         method concrete_ident' ~(under_current_ns : bool) : concrete_ident fn =
           fun id ->

diff --git a/engine/lib/deprecated_generic_printer/deprecated_generic_printer_base.ml b/engine/lib/deprecated_generic_printer/deprecated_generic_printer_base.ml
@@ -88,7 +88,7 @@ module Make (F : Features.T) = struct
     object (print)
       val mutable current_span = Span.default
       val mutable span_data : Annotation.t list = []
-      val mutable current_namespace : (string * string list) option = None
+      val mutable current_namespace : string list option = None
       method get_span_data () = span_data
 
       method with_span ~span f =
@@ -118,7 +118,7 @@ module Make (F : Features.T) = struct
           let id_ns = print#namespace_of_concrete_ident id in
           print#concrete_ident'
             ~under_current_ns:
-              ([%equal: (string * string list) option] current_ns (Some id_ns))
+              ([%equal: string list option] current_ns (Some id_ns))
             id
       (** Print a concrete identifier.
 
@@ -281,7 +281,7 @@ module Make (F : Features.T) = struct
     method printer_name : string
     method get_span_data : unit -> Annotation.t list
 
-    method namespace_of_concrete_ident : concrete_ident -> string * string list
+    method namespace_of_concrete_ident : concrete_ident -> string list
     (** The namespace a concrete identifier was defined in. *)
 
     method par_state : ast_position -> par_state