diff --git a/src/kernel_services/ast_printing/cil_printer.ml b/src/kernel_services/ast_printing/cil_printer.ml
index 611431bf0239b02bcf18ea472fca5be39e3bc526..fa0a5d3969928f51681492f6e7a86488a8573da8 100644
--- a/src/kernel_services/ast_printing/cil_printer.ml
+++ b/src/kernel_services/ast_printing/cil_printer.ml
@@ -1263,9 +1263,9 @@ class cil_printer () = object (self)
   method builtin_logic_info fmt bli =
     fprintf fmt "%a" self#varname bli.bl_name
 
-  method logic_type_info fmt s = fprintf fmt "%a" self#logic_name s.lt_name
+  method logic_type_info fmt s = self#logic_name fmt s.lt_name
 
-  method logic_ctor_info fmt ci =  fprintf fmt "%a" self#logic_name ci.ctor_name
+  method logic_ctor_info fmt ci = self#logic_name fmt ci.ctor_name
 
   method initinfo fmt io =
     match io.init with
diff --git a/src/kernel_services/ast_printing/printer_api.ml b/src/kernel_services/ast_printing/printer_api.ml
index 14c22c78d8050bd3269f7f19dc6d4707e0a6aa14..1066405ee1370032b09b63f49fdc32b550ddd261 100644
--- a/src/kernel_services/ast_printing/printer_api.ml
+++ b/src/kernel_services/ast_printing/printer_api.ml
@@ -274,8 +274,13 @@ class type extensible_printer_type = object
   method builtin_logic_info: Format.formatter -> builtin_logic_info -> unit
   method logic_type_info: Format.formatter -> logic_type_info -> unit
   method logic_ctor_info: Format.formatter -> logic_ctor_info -> unit
-  method logic_name: Format.formatter -> string -> unit
   method logic_var: Format.formatter -> logic_var -> unit
+
+  (** logic names, with full module path if needed (eg. "foo::bar::jazz")
+      Defaults to [self#varname], with the full name truncated to the currently
+      opened module, if any. *)
+  method logic_name: Format.formatter -> string -> unit
+
   method quantifiers: Format.formatter -> quantifiers -> unit
   method predicate_node: Format.formatter -> predicate_node -> unit
   method predicate: Format.formatter -> predicate -> unit