diff --git a/Makefile.generating b/Makefile.generating
index a79f857a468f474500ee7737a551e5b1905e3082..568a02af72e64b3b4a4a3dc5eb59f60f86d3aa3f 100644
--- a/Makefile.generating
+++ b/Makefile.generating
@@ -153,8 +153,16 @@ endif
 
 ifeq ($(HAS_OCAML408),yes)
   DYNLINK_INIT=fun () -> ()
+  FORMAT_STAG=stag
+  FORMAT_STRING_OF_STAG=match s with\n\
+      | Format.String_tag str -> str\n\
+      | _ -> raise (Invalid_argument "unsupported tag extension")
+  FORMAT_STAG_OF_STRING=Format.String_tag s
 else
   DYNLINK_INIT=Dynlink.init
+  FORMAT_STAG=tag
+  FORMAT_STRING_OF_STAG=s
+  FORMAT_STAG_OF_STRING=s
 endif
 
 src/libraries/stdlib/transitioning.ml: \
@@ -170,6 +178,9 @@ src/libraries/stdlib/transitioning.ml: \
          -e 's/@ASSOC_OPT@/$(ASSOC_OPT)/g' \
          -e 's/@ASSQ_OPT@/$(ASSQ_OPT)/g' \
          -e 's/@DYNLINK_INIT@/$(DYNLINK_INIT)/g' \
+         -e 's/@FORMAT_STAG@/$(FORMAT_STAG)/g' \
+         -e 's/@FORMAT_STRING_OF_STAG@/$(FORMAT_STRING_OF_STAG)/g' \
+         -e 's/@FORMAT_STAG_OF_STRING@/$(FORMAT_STAG_OF_STRING)/g' \
         $< > $@
 	$(CHMOD_RO) $@
 
diff --git a/src/libraries/stdlib/transitioning.ml.in b/src/libraries/stdlib/transitioning.ml.in
index 5dac32656eb7b41f7d6474f6a0d7d9a6a8d5f470..2d0204a65326b6494f21c6dbc14535db0190c8e4 100644
--- a/src/libraries/stdlib/transitioning.ml.in
+++ b/src/libraries/stdlib/transitioning.ml.in
@@ -93,6 +93,42 @@ module Dynlink = struct
   let init = @DYNLINK_INIT@
 end
 
+module Format = struct
+  type stag = Format.@FORMAT_STAG@
+  let string_of_stag s = @FORMAT_STRING_OF_STAG@
+  let stag_of_string s = @FORMAT_STAG_OF_STRING@
+  type formatter_stag_functions = {
+    mark_open_stag : stag -> string;
+    mark_close_stag : stag -> string;
+    print_open_stag : stag -> unit;
+    print_close_stag : stag -> unit;
+  }
+  let pp_set_formatter_stag_functions fmt set_formatter_stag_functions =
+    Format.pp_set_formatter_@FORMAT_STAG@_functions fmt
+      {
+        Format.mark_open_@FORMAT_STAG@ =
+          set_formatter_stag_functions.mark_open_stag;
+        Format.mark_close_@FORMAT_STAG@ =
+          set_formatter_stag_functions.mark_close_stag;
+        Format.print_open_@FORMAT_STAG@ =
+          set_formatter_stag_functions.print_open_stag;
+        Format.print_close_@FORMAT_STAG@ =
+          set_formatter_stag_functions.print_close_stag;
+      }
+  let pp_get_formatter_stag_functions fmt () =
+    let st = Format.pp_get_formatter_@FORMAT_STAG@_functions fmt () in
+    {
+      mark_open_stag = st.Format.mark_open_@FORMAT_STAG@;
+      mark_close_stag = st.Format.mark_close_@FORMAT_STAG@;
+      print_open_stag = st.Format.print_open_@FORMAT_STAG@;
+      print_close_stag = st.Format.print_close_@FORMAT_STAG@;
+    }
+  let pp_open_stag fmt s =
+    Format.pp_open_@FORMAT_STAG@ fmt s
+  let pp_close_stag fmt () =
+    Format.pp_close_@FORMAT_STAG@ fmt ()
+end
+
 module Q = struct
 
   let round_to_float x exact =
diff --git a/src/libraries/stdlib/transitioning.mli b/src/libraries/stdlib/transitioning.mli
index 5b542fd7b9ff88d9934154d40b6c854c69f5c2f2..55a64b4d91bee1fbdeb5bc1de23a9318cf7f27b6 100644
--- a/src/libraries/stdlib/transitioning.mli
+++ b/src/libraries/stdlib/transitioning.mli
@@ -73,6 +73,24 @@ module Dynlink: sig
   val init: unit -> unit
 end
 
+module Format: sig
+  type stag
+  val string_of_stag: stag -> string
+  val stag_of_string: string -> stag
+  type formatter_stag_functions = {
+    mark_open_stag : stag -> string;
+    mark_close_stag : stag -> string;
+    print_open_stag : stag -> unit;
+    print_close_stag : stag -> unit;
+  }
+  val pp_set_formatter_stag_functions:
+    Format.formatter -> formatter_stag_functions -> unit
+  val pp_get_formatter_stag_functions:
+    Format.formatter -> unit -> formatter_stag_functions
+  val pp_open_stag : Format.formatter -> stag -> unit
+  val pp_close_stag : Format.formatter -> unit -> unit
+end
+
 (** {1 Zarith} *)
 
 (** Function [Q.to_float] was introduced in Zarith 1.5 *)
diff --git a/src/libraries/utils/rich_text.ml b/src/libraries/utils/rich_text.ml
index 3a15771b965c85bb62c45878e0e82a8d9cdfc76c..cfba39cf308cdc83bd4ac1147c409caf48e75042 100644
--- a/src/libraries/utils/rich_text.ml
+++ b/src/libraries/utils/rich_text.ml
@@ -27,7 +27,7 @@
 type tag = {
   p : int ; (* first position *)
   q : int ; (* last position (excluded) *)
-  tag : Format.tag ;
+  tag : Transitioning.Format.stag ;
   children : tag list ;
 }
 
@@ -50,8 +50,8 @@ let tags_at (_,tags) k = lookup [] k tags
 type env = {
   text : string ;
   output : (string -> int -> int -> unit) option ;
-  open_tag : (Format.tag -> int -> int -> unit) option ;
-  close_tag : (Format.tag -> int -> int -> unit) option ;
+  open_tag : (Transitioning.Format.stag -> int -> int -> unit) option ;
+  close_tag : (Transitioning.Format.stag -> int -> int -> unit) option ;
 }
 
 let signal f tag p q =
@@ -86,8 +86,8 @@ let rec output_vbox fmt text k n =
       end
 
 let output_fmt fmt text k n = Format.pp_print_string fmt (String.sub text k n)
-let open_tag fmt tag _k _n = Format.pp_open_tag fmt tag
-let close_tag fmt _tag _k _n = Format.pp_close_tag fmt ()
+let open_tag fmt tag _k _n = Transitioning.Format.pp_open_stag fmt tag
+let close_tag fmt _tag _k _n = Transitioning.Format.pp_close_stag fmt ()
 
 let pretty ?vbox fmt message =
   let open_tag = open_tag fmt in
@@ -209,11 +209,11 @@ let create ?indent ?margin () =
       Format.pp_set_max_indent fmt (max 0 (min k (m-10)))
   end ;
   let open Format in
-  pp_set_formatter_tag_functions fmt {
-    print_open_tag = push_tag buffer ;
-    print_close_tag = pop_tag buffer ;
-    mark_open_tag = no_mark ;
-    mark_close_tag = no_mark ;
+  Transitioning.Format.pp_set_formatter_stag_functions fmt {
+    Transitioning.Format.print_open_stag = push_tag buffer ;
+    print_close_stag = pop_tag buffer ;
+    mark_open_stag = no_mark ;
+    mark_close_stag = no_mark ;
   } ;
   pp_set_print_tags fmt true ;
   pp_set_mark_tags fmt false ;
diff --git a/src/libraries/utils/rich_text.mli b/src/libraries/utils/rich_text.mli
index 415d3e3ef32a1a708b89b5606c1104812786e13f..172a9dd3513b02aadb4ea64e21ec57b3eb8a55f1 100644
--- a/src/libraries/utils/rich_text.mli
+++ b/src/libraries/utils/rich_text.mli
@@ -31,14 +31,14 @@ val char_at : message -> int -> char
 val string : message -> string
 val substring : message -> int -> int -> string
 
-val tags_at : message -> int -> (Format.tag * int * int) list
+val tags_at : message -> int -> (Transitioning.Format.stag * int * int) list
 (** Returns the list of tags at the given position.
     Inner tags come first, outer tags last. *)
 
 val visit :
   ?output:(string -> int -> int -> unit) ->
-  ?open_tag:(Format.tag -> int -> int -> unit) ->
-  ?close_tag:(Format.tag -> int -> int -> unit) ->
+  ?open_tag:(Transitioning.Format.stag -> int -> int -> unit) ->
+  ?close_tag:(Transitioning.Format.stag -> int -> int -> unit) ->
   message -> unit
 (** Visit the message, with depth-first recursion on tags.
     All methods are called with text or tag, position and length. *)
diff --git a/src/plugins/gui/pretty_source.ml b/src/plugins/gui/pretty_source.ml
index c17460dafd93064ba107970be47df602c24ab43e..d7fb0efbdcd99194ec3005eb963ad86b9fdc77eb 100644
--- a/src/plugins/gui/pretty_source.ml
+++ b/src/plugins/gui/pretty_source.ml
@@ -274,12 +274,14 @@ let localizable_from_locs state ~file ~line =
 let buffer_formatter state source =
   let starts = Stack.create () in
   let emit_open_tag s =
+    let s = Transitioning.Format.string_of_stag s in
     (* Ignore tags that are not ours *)
     if Extlib.string_prefix "guitag:" s then
       Stack.push (source#end_iter#offset, Tag.get s) starts ;
     ""
   in
   let emit_close_tag s =
+    let s = Transitioning.Format.string_of_stag s in
     (try
        if Extlib.string_prefix "guitag:" s then
          let (p,sid) = Stack.pop starts in
@@ -292,10 +294,12 @@ let buffer_formatter state source =
   Format.pp_set_tags gtk_fmt true;
   Format.pp_set_print_tags gtk_fmt false;
   Format.pp_set_mark_tags gtk_fmt true;
-  Format.pp_set_formatter_tag_functions
-    gtk_fmt {(Format.pp_get_formatter_tag_functions gtk_fmt ()) with
-             Format.mark_open_tag = emit_open_tag;
-             Format.mark_close_tag = emit_close_tag;};
+  let open Transitioning.Format in
+  pp_set_formatter_stag_functions
+    gtk_fmt {(pp_get_formatter_stag_functions gtk_fmt ())
+             with
+              mark_open_stag = emit_open_tag;
+              mark_close_stag = emit_close_tag;};
 
   Format.pp_set_margin gtk_fmt 79;
   gtk_fmt
diff --git a/src/plugins/gui/wtext.ml b/src/plugins/gui/wtext.ml
index 53537274b92620d81cca223a4145bb68aaf8c66d..e87caf583e28717555dbfc1f7d23bbefa7837d6d 100644
--- a/src/plugins/gui/wtext.ml
+++ b/src/plugins/gui/wtext.ml
@@ -244,6 +244,7 @@ class text ?(autoscroll=false) ?(width=80) ?(indent=60) () =
         end
 
     method private open_tag name =
+      let name = Transitioning.Format.string_of_stag name in
       self#flush () ; style <- self#tag name :: style ; ""
 
     method private close_tag _name =
@@ -254,13 +255,14 @@ class text ?(autoscroll=false) ?(width=80) ?(indent=60) () =
       | (TAG _ | PLAIN) :: sty -> style <- sty ; ""
 
     method fmt = match fmtref with Some fmt -> fmt | None ->
+      let open Transitioning.Format in
       let output_string s a b = if b > 0 then Buffer.add_substring text s a b in
       let fmt = Format.make_formatter output_string self#flush in
-      let tagger = Format.pp_get_formatter_tag_functions fmt () in
-      Format.pp_set_formatter_tag_functions fmt
+      let tagger = pp_get_formatter_stag_functions fmt () in
+      pp_set_formatter_stag_functions fmt
         { tagger with
-          Format.mark_open_tag = self#open_tag ;
-          Format.mark_close_tag = self#close_tag ;
+          mark_open_stag = self#open_tag;
+          mark_close_stag = self#close_tag ;
         } ;
       Format.pp_set_print_tags fmt false ;
       Format.pp_set_mark_tags fmt true ;
@@ -306,9 +308,10 @@ class text ?(autoscroll=false) ?(width=80) ?(indent=60) () =
       begin
         let sid = hid <- succ hid ; Printf.sprintf ">%X" hid in
         Hashtbl.add marks sid (fun p q -> Hashtbl.remove marks sid ; f p q) ;
-        Format.pp_open_tag fmt sid ;
+        Transitioning.Format.pp_open_stag fmt
+          (Transitioning.Format.stag_of_string sid) ;
         let () = pp fmt in
-        Format.pp_close_tag fmt () ;
+        Transitioning.Format.pp_close_stag fmt () ;
       end
 
     (* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/metrics/metrics_acsl.ml b/src/plugins/metrics/metrics_acsl.ml
index ebba36bb4033ebaf551f4c050edcbbd8174ce1c5..0e107134a784d1f7a3c16b7cd547882865513f9d 100644
--- a/src/plugins/metrics/metrics_acsl.ml
+++ b/src/plugins/metrics/metrics_acsl.ml
@@ -284,7 +284,7 @@ let dump_acsl_stats fmt =
     
 
 let dump_acsl_stats_html fmt =
-  Format.pp_set_formatter_tag_functions fmt Metrics_base.html_tag_functions;
+  Transitioning.Format.pp_set_formatter_stag_functions fmt Metrics_base.html_stag_functions;
   Format.fprintf fmt
     "@[<v 0> <!DOCTYPE HTML PUBLIC \"-//W3C//DTD HTML 4.01//EN\"\
           \"http://www.w3.org/TR/html4/strict.dtd\">@ \
diff --git a/src/plugins/metrics/metrics_base.ml b/src/plugins/metrics/metrics_base.ml
index f10bf8fd03428dab4164c037d96e01dad29dd005..b55a6772f17b53bf04d984bce393b164d1e52edf 100644
--- a/src/plugins/metrics/metrics_base.ml
+++ b/src/plugins/metrics/metrics_base.ml
@@ -24,22 +24,22 @@ open Cil_types (* vname, vaddrof *)
 ;;
 
 (* Formatting html with Format.formatters *)
-let html_tag_functions =
-  let mark_open_tag t = Format.sprintf "<%s>" t
-  and mark_close_tag t =
+let html_stag_functions =
+  let mark_open_stag t =
+    let t = Transitioning.Format.string_of_stag t in
+    Format.sprintf "<%s>" t
+  and mark_close_stag t =
+    let t = Transitioning.Format.string_of_stag t in
     try
       let index = String.index t ' ' in
       Format.sprintf "</%s>" (String.sub t 0 index)
     with
       | Not_found -> Format.sprintf "</%s>" t
-  and print_open_tag _ = ()
-  and print_close_tag _ = ()
+  and print_open_stag _ = ()
+  and print_close_stag _ = ()
   in
-  { Format.mark_open_tag = mark_open_tag;
-    Format.mark_close_tag = mark_close_tag;
-    Format.print_open_tag = print_open_tag;
-    Format.print_close_tag = print_close_tag;
-  }
+  { Transitioning.Format.mark_open_stag; mark_close_stag;
+    print_open_stag; print_close_stag; }
 ;;
 
 (* Utility function to have underlines the same length as the title.
diff --git a/src/plugins/metrics/metrics_base.mli b/src/plugins/metrics/metrics_base.mli
index 6976f2c9c73fae948a022030d2ad5d2c0ac439ae..9ff77090ef5cd259d487cb74769de152e8424113 100644
--- a/src/plugins/metrics/metrics_base.mli
+++ b/src/plugins/metrics/metrics_base.mli
@@ -21,7 +21,7 @@
 (**************************************************************************)
 
 (** Tag functions handling html tags for Format *)
-val html_tag_functions : Format.formatter_tag_functions;;
+val html_stag_functions : Transitioning.Format.formatter_stag_functions;;
 
 (** mk_hdr [level] [ppf] [hdr_strg] produces a title from [hdr_strg] with an
     underline of the same length.
diff --git a/src/plugins/metrics/metrics_cilast.ml b/src/plugins/metrics/metrics_cilast.ml
index 6474c0e06191a96073c31f18f4a0a7047b69f939..9ccc80eb23103cbb27441673f342fe6a8687730f 100644
--- a/src/plugins/metrics/metrics_cilast.ml
+++ b/src/plugins/metrics/metrics_cilast.ml
@@ -135,7 +135,7 @@ class slocVisitor ~libc : sloc_visitor = object(self)
         Format.fprintf fmt "%a" self#pp_file_metrics filename) metrics_map
 
   method print_stats fmt =
-    Format.pp_set_formatter_tag_functions fmt Metrics_base.html_tag_functions;
+    Transitioning.Format.pp_set_formatter_stag_functions fmt Metrics_base.html_stag_functions;
     Format.pp_set_tags fmt true;
     let pr_hdr fmt hdr_name =
       Format.fprintf fmt "@{<th>%s@}" hdr_name in
@@ -547,7 +547,7 @@ let pretty_used_files used_files =
 
 let dump_html fmt cil_visitor =
   (* Activate tagging for html *)
-  Format.pp_set_formatter_tag_functions fmt html_tag_functions;
+  Transitioning.Format.pp_set_formatter_stag_functions fmt html_stag_functions;
   Format.pp_set_tags fmt true;
 
   let pr_row s fmt n =