diff --git a/src/kernel_services/ast_printing/printer_api.mli b/src/kernel_services/ast_printing/printer_api.mli
index 1233d42b73586802126e51ea795269819aee63ae..78de7bf360627e7a59de0c7a2c9d6143ee61b95c 100644
--- a/src/kernel_services/ast_printing/printer_api.mli
+++ b/src/kernel_services/ast_printing/printer_api.mli
@@ -366,7 +366,7 @@ type state =
 (** {2 Functions for pretty printing} *)
 (* ********************************************************************* *)
 
-module type S = sig
+module type S_pp = sig
 
   val pp_varname: Format.formatter -> string -> unit
 
@@ -474,8 +474,14 @@ module type S = sig
     Format.formatter ->
     'a ->
     unit
-  (** [self#force_brace printer fmt x] pretty prints [x] by using [printer],
-      but add some extra braces '\{' and '\}' which are hidden by default. *)
+    (** [self#force_brace printer fmt x] pretty prints [x] by using [printer],
+        but add some extra braces '\{' and '\}' which are hidden by default. *)
+
+end
+
+module type S = sig
+
+  include S_pp
 
   (* ********************************************************************* *)
   (** {3 Extensible printer} *)
diff --git a/src/kernel_services/ast_printing/printer_builder.ml b/src/kernel_services/ast_printing/printer_builder.ml
index 06450f9994a53aaff8fec339d71455cd4f90676a..bba10960ff4b6230c9e9f06c7bf1ab1b3302d263 100644
--- a/src/kernel_services/ast_printing/printer_builder.ml
+++ b/src/kernel_services/ast_printing/printer_builder.ml
@@ -20,54 +20,15 @@
 (*                                                                        *)
 (**************************************************************************)
 
-module Make
-    (P: sig class printer: unit -> Printer_api.extensible_printer_type end) =
+module Make_pp
+    (P: sig val printer : unit -> Printer_api.extensible_printer_type end) =
 struct
 
-  module type PrinterClass = sig
-    class printer : Printer_api.extensible_printer_type
-  end
-
-  let printer_class_ref =
-    ref (module struct class printer = P.printer () end: PrinterClass)
-
-  let printer_ref = ref None
-
-  module type PrinterExtension = functor (X: PrinterClass) -> PrinterClass
-
-  let set_printer p =
-    printer_class_ref := p;
-    printer_ref := None
-
-  let update_printer x =
-    let module X = (val x: PrinterExtension) in
-    let module Cur = (val !printer_class_ref: PrinterClass) in
-    let module Updated = X(Cur) in
-    set_printer (module Updated: PrinterClass)
-
-  let printer () : Printer_api.extensible_printer_type =
-    match !printer_ref with
-    | None ->
-      let module Printer = (val !printer_class_ref: PrinterClass) in
-      let p = new Printer.printer in
-      printer_ref := Some p;
-      p#reset ();
-      p
-    | Some p ->
-      p#reset ();
-      p
-
-  let current_printer () = !printer_class_ref
-
-  class extensible_printer = P.printer
+  let printer = P.printer
 
   let without_annot f fmt x = (printer ())#without_annot f fmt x
   let force_brace f fmt x = (printer ())#force_brace f fmt x
-
-  let pp_varname fmt x = (printer())#varname fmt x
-
-  (* eta-expansion required for applying side-effect of [printer ()] at the
-     right time *)
+  let pp_varname fmt x = (printer ())#varname fmt x
   let pp_location fmt x = (printer ())#location fmt x
   let pp_constant fmt x = (printer ())#constant fmt x
   let pp_ikind fmt x = (printer ())#ikind fmt x
@@ -113,7 +74,7 @@ struct
   let pp_variant fmt x = (printer ())#variant fmt x
   let pp_from fmt x = (printer ())#from "assigns" fmt x
   let pp_full_assigns fmt x = (printer ())#assigns fmt x
-  let pp_assigns = pp_full_assigns "assigns"
+  let pp_assigns fmt x = pp_full_assigns "assigns" fmt x
   let pp_allocation fmt x = (printer ())#allocation ~isloop:false fmt x
   let pp_loop_from fmt x = (printer ())#from "loop assigns" fmt x
   let pp_loop_assigns fmt x = (printer ())#assigns "loop assigns" fmt x
@@ -129,6 +90,53 @@ struct
   let pp_logic_constant fmt x = (printer ())#logic_constant fmt x
   let pp_term_lhost fmt x = (printer ())#term_lhost fmt x
   let pp_fundec fmt x = (printer ())#fundec fmt x
+
+end
+
+
+module Make
+    (P: sig class printer: unit -> Printer_api.extensible_printer_type end) =
+struct
+
+  module type PrinterClass = sig
+    class printer : Printer_api.extensible_printer_type
+  end
+
+  let printer_class_ref =
+    ref (module struct class printer = P.printer () end: PrinterClass)
+
+  let printer_ref = ref None
+
+  module type PrinterExtension = functor (X: PrinterClass) -> PrinterClass
+
+  let set_printer p =
+    printer_class_ref := p;
+    printer_ref := None
+
+  let update_printer x =
+    let module X = (val x: PrinterExtension) in
+    let module Cur = (val !printer_class_ref: PrinterClass) in
+    let module Updated = X(Cur) in
+    set_printer (module Updated: PrinterClass)
+
+  let printer () : Printer_api.extensible_printer_type =
+    match !printer_ref with
+    | None ->
+      let module Printer = (val !printer_class_ref: PrinterClass) in
+      let p = new Printer.printer in
+      printer_ref := Some p;
+      p#reset ();
+      p
+    | Some p ->
+      p#reset ();
+      p
+
+  let current_printer () = !printer_class_ref
+
+  class extensible_printer = P.printer
+
+  include Make_pp(struct let printer = printer end)
+
 end
 
 (*
diff --git a/src/kernel_services/ast_printing/printer_builder.mli b/src/kernel_services/ast_printing/printer_builder.mli
index d9af78ade52b93e4a3ad14784fe95d02e0d62e1b..1816cc0ec4249e5e32dfb6c64a87bd1e141110e3 100644
--- a/src/kernel_services/ast_printing/printer_builder.mli
+++ b/src/kernel_services/ast_printing/printer_builder.mli
@@ -20,6 +20,13 @@
 (*                                                                        *)
 (**************************************************************************)
 
+(** Build a dynamic printer that bind all pretty-printers to the
+    object obtained by (P()) *)
+
+module Make_pp
+    (P: sig val printer: unit -> Printer_api.extensible_printer_type end):
+  Printer_api.S_pp
+
 (** Build a full pretty-printer from a pretty-printing class.
     @since Fluorine-20130401 *)