diff --git a/src/kernel_services/abstract_interp/abstract_interp.ml b/src/kernel_services/abstract_interp/abstract_interp.ml
index 0569d8fe257e55f6c88fe4d94ddaba55feeaca44..80cc254535621d943c7102c997d0ef64ca0938c1 100644
--- a/src/kernel_services/abstract_interp/abstract_interp.ml
+++ b/src/kernel_services/abstract_interp/abstract_interp.ml
@@ -223,7 +223,6 @@ module Make_Generic_Lattice_Set
          let rehash = Datatype.identity
          let copy = Datatype.undefined
          let pretty = pretty
-         let varname = Datatype.undefined
          let mem_project = Datatype.never_any_project
        end) :
        Datatype.S with type t := t)
@@ -364,7 +363,6 @@ module Make_Lattice_Base (V:Lattice_Value):(Lattice_Base with type l = V.t) = st
          let rehash = Datatype.identity
          let copy = Datatype.undefined
          let pretty = pretty
-         let varname = Datatype.undefined
          let mem_project = Datatype.never_any_project
        end) :
        Datatype.S with type t := t)
@@ -515,7 +513,6 @@ module Bool = struct
                let rehash = Datatype.identity
                let copy = Datatype.identity
                let pretty = pretty
-                     let varname = Datatype.undefined
                let mem_project = Datatype.never_any_project
              end) :
              Datatype.S with type t := t)
@@ -675,7 +672,6 @@ struct
                let rehash = Datatype.identity
                let copy = Datatype.undefined
                      let pretty = pretty
-               let varname = Datatype.undefined
                let mem_project = Datatype.never_any_project
              end) :
              Datatype.S with type t := t)
@@ -774,7 +770,6 @@ struct
          let rehash = Datatype.identity
          let copy = Datatype.undefined
          let pretty = pretty
-         let varname = Datatype.undefined
          let mem_project = Datatype.never_any_project
        end):
        Datatype.S with type t := t)
@@ -943,7 +938,6 @@ struct
         let rehash = Datatype.undefined
         let copy = Datatype.undefined
         let pretty = pretty
-        let varname = Datatype.undefined
         let mem_project = Datatype.never_any_project
       end)
   let () = Type.set_ml_name ty None
diff --git a/src/kernel_services/abstract_interp/base.ml b/src/kernel_services/abstract_interp/base.ml
index 4734eef370604d213ef841ba76e96ba3a4994843..e0b94048054efd2e308450022bdc9a7c79de202d 100644
--- a/src/kernel_services/abstract_interp/base.ml
+++ b/src/kernel_services/abstract_interp/base.ml
@@ -101,7 +101,6 @@ module Validity = Datatype.Make
       let mem_project = Datatype.never_any_project
       let rehash = Datatype.identity
       let copy (x:t) = x
-      let varname _ = "v"
     end)
 
 type cstring = CSString of string | CSWstring of Escape.wstring
@@ -451,7 +450,6 @@ module Base = struct
         let mem_project = Datatype.never_any_project
         let rehash = Datatype.identity
         let copy = Datatype.undefined
-        let varname = Datatype.undefined
       end)
   let id = id
   let pretty_debug = pretty
diff --git a/src/kernel_services/abstract_interp/int_Base.ml b/src/kernel_services/abstract_interp/int_Base.ml
index f75a06568c36414d32a66364e708112c3caf33a7..fe28f63e41cea44cbeb040aa697d45b1cb9d2807 100644
--- a/src/kernel_services/abstract_interp/int_Base.ml
+++ b/src/kernel_services/abstract_interp/int_Base.ml
@@ -56,7 +56,7 @@ include Datatype.Make
       let rehash = Datatype.identity
       let copy = Extlib.id
       let pretty = pretty
-      let varname = Datatype.undefined
+
       let mem_project = Datatype.never_any_project
     end)
 
diff --git a/src/kernel_services/abstract_interp/int_interval.ml b/src/kernel_services/abstract_interp/int_interval.ml
index 4900196abcd0e8828504e03535e43c56706dc600..f6cd553dac211d6d1c2e26f745e8420e35e24b8a 100644
--- a/src/kernel_services/abstract_interp/int_interval.ml
+++ b/src/kernel_services/abstract_interp/int_interval.ml
@@ -96,7 +96,7 @@ include Datatype.Make_with_collections
       let rehash = Datatype.identity
       let mem_project = Datatype.never_any_project
       let copy = Datatype.undefined
-      let varname = Datatype.undefined
+
     end)
 
 (* ------------------------------ Building ---------------------------------- *)
diff --git a/src/kernel_services/abstract_interp/int_set.ml b/src/kernel_services/abstract_interp/int_set.ml
index e1fe0de05909a39dee7f02dc70400cae957fa131..474944295dbd9ffbcb4999a636d0a860a55f2491 100644
--- a/src/kernel_services/abstract_interp/int_set.ml
+++ b/src/kernel_services/abstract_interp/int_set.ml
@@ -132,7 +132,7 @@ include Datatype.Make_with_collections
       let rehash x = x
       let mem_project = Datatype.never_any_project
       let copy = Datatype.undefined
-      let varname = Datatype.undefined
+
     end)
 
 (* ---------------------------------- Utils --------------------------------- *)
diff --git a/src/kernel_services/abstract_interp/int_val.ml b/src/kernel_services/abstract_interp/int_val.ml
index 424ba043ea0e9dad37f038eba0104cf0d3742c8b..23f49a22f592912ee95666e79bab7dd79d3ebca8 100644
--- a/src/kernel_services/abstract_interp/int_val.ml
+++ b/src/kernel_services/abstract_interp/int_val.ml
@@ -77,7 +77,7 @@ include Datatype.Make_with_collections
       let rehash x = x
       let mem_project = Datatype.never_any_project
       let copy = Datatype.undefined
-      let varname = Datatype.undefined
+
     end)
 
 (* ------------------------------- Constructors ----------------------------  *)
diff --git a/src/kernel_services/abstract_interp/ival.ml b/src/kernel_services/abstract_interp/ival.ml
index 233c6f19fc22e47eee46b6fe9aa80b35af9a682a..ac2cec82d0ef3a3f59b4b2a380cc586014c4e4e3 100644
--- a/src/kernel_services/abstract_interp/ival.ml
+++ b/src/kernel_services/abstract_interp/ival.ml
@@ -826,7 +826,7 @@ include (
       let rehash = rehash
       let mem_project = Datatype.never_any_project
       let copy = Datatype.undefined
-      let varname = Datatype.undefined
+
     end):
     Datatype.S_with_collections with type t := t)
 
diff --git a/src/kernel_services/abstract_interp/lmap.ml b/src/kernel_services/abstract_interp/lmap.ml
index 483210b38356b616ed5fdcd9d54d873c75edcd97..063250f501c1212f084098fdba314e2d6e8122ca 100644
--- a/src/kernel_services/abstract_interp/lmap.ml
+++ b/src/kernel_services/abstract_interp/lmap.ml
@@ -593,7 +593,7 @@ struct
         let pretty = pretty
         let rehash = Datatype.identity
         let copy = Datatype.undefined
-        let varname = Datatype.undefined
+
         let mem_project = Datatype.never_any_project
       end)
   let () = Type.set_ml_name ty None
diff --git a/src/kernel_services/abstract_interp/lmap_bitwise.ml b/src/kernel_services/abstract_interp/lmap_bitwise.ml
index 72515172d0ec47b7300de80ba4825aab8e7fc521..ea853b5e86d0f66d133193d2a875e7f46a9ebe48 100644
--- a/src/kernel_services/abstract_interp/lmap_bitwise.ml
+++ b/src/kernel_services/abstract_interp/lmap_bitwise.ml
@@ -240,7 +240,7 @@ struct
         let pretty = pretty
         let rehash = Datatype.identity
         let copy = Datatype.undefined
-        let varname = Datatype.undefined
+
         let mem_project = Datatype.never_any_project
       end)
 
diff --git a/src/kernel_services/abstract_interp/map_lattice.ml b/src/kernel_services/abstract_interp/map_lattice.ml
index 0d0d31d9e90fe234611f8378f0d1b77bb50640d8..caec2966924caf26f50a7b4f257c6265f57f2e70 100644
--- a/src/kernel_services/abstract_interp/map_lattice.ml
+++ b/src/kernel_services/abstract_interp/map_lattice.ml
@@ -500,7 +500,7 @@ module Make_MapSet_Lattice
          let copy = Datatype.undefined
          let pretty = pretty
          let mem_project = Datatype.never_any_project
-         let varname = Datatype.undefined
+
        end): Datatype.S_with_collections with type t := t)
 
 
diff --git a/src/kernel_services/abstract_interp/offsetmap.ml b/src/kernel_services/abstract_interp/offsetmap.ml
index 0bc43658600ab137d32f6681a8031bea49dee8be..ed8d1b9080b0404e169e8fa34e1114b9cbdd0534 100644
--- a/src/kernel_services/abstract_interp/offsetmap.ml
+++ b/src/kernel_services/abstract_interp/offsetmap.ml
@@ -230,7 +230,7 @@ module Make (V : module type of Offsetmap_lattice_with_isotropy) = struct
             let rehash x = !rehash_ref x
             let copy = Datatype.undefined
             let pretty = pretty
-            let varname = Datatype.undefined
+
             let mem_project = Datatype.never_any_project
           end)
       include D
@@ -2459,7 +2459,6 @@ module Int_Intervals = struct
                 Int.packed_descr; Int.packed_descr |] |]
 
       let mem_project = Datatype.never_any_project
-      let varname _ = "i"
       let copy = Datatype.undefined
     end)
 
diff --git a/src/kernel_services/abstract_interp/origin.ml b/src/kernel_services/abstract_interp/origin.ml
index c6cdb0fd21cf0f3aae1c36136d824b9fd4b3c2dc..4603d837ecda66614875f0fcb82cf2e6a80bd350 100644
--- a/src/kernel_services/abstract_interp/origin.ml
+++ b/src/kernel_services/abstract_interp/origin.ml
@@ -136,7 +136,7 @@ include Datatype.Make
       let rehash = Datatype.undefined
       let copy = Datatype.undefined
       let pretty = pretty
-      let varname = Datatype.undefined
+
       let mem_project = Datatype.never_any_project
     end)
 
diff --git a/src/kernel_services/ast_data/alarms.ml b/src/kernel_services/ast_data/alarms.ml
index 3ccb9304cb3ac6e9e2608c82530878deba39d769..1878a37f634992f679d953ca4b9479fe0179b978 100644
--- a/src/kernel_services/ast_data/alarms.ml
+++ b/src/kernel_services/ast_data/alarms.ml
@@ -240,7 +240,7 @@ module D =
 
       let structural_descr = Structural_descr.t_abstract
       let rehash = Datatype.identity
-      let varname = Datatype.undefined
+
 
       let pretty fmt = function
         | Division_by_zero e ->
diff --git a/src/kernel_services/ast_data/property_status.ml b/src/kernel_services/ast_data/property_status.ml
index ba440a42ed53764e29cbef756fd3fed480d6cbe2..46c82aeca51a4f89ebbc231346f44927c49b4da1 100644
--- a/src/kernel_services/ast_data/property_status.ml
+++ b/src/kernel_services/ast_data/property_status.ml
@@ -80,7 +80,6 @@ module Emitter_with_properties =
 
       let copy = Datatype.undefined
       let pretty fmt e = Usable_emitter.pretty fmt e.emitter
-      let varname _ = assert false
       let mem_project = Datatype.never_any_project
     end)
 
diff --git a/src/kernel_services/ast_queries/ast_diff.ml b/src/kernel_services/ast_queries/ast_diff.ml
index 96a1eb0a076324d4cc1aab1eaaa1ef039b7df6da..ffa3ca42bd6e2993e9d6151e8c80e019c8297c6d 100644
--- a/src/kernel_services/ast_queries/ast_diff.ml
+++ b/src/kernel_services/ast_queries/ast_diff.ml
@@ -62,9 +62,6 @@ struct
   let mk_pretty pp fmt = function
     | `Not_present -> Format.pp_print_string fmt "N/A"
     | `Same x -> Format.fprintf fmt " => %a" pp x
-  let mk_varname v = function
-    | `Not_present -> "x"
-    | `Same x -> v x ^ "_c"
   let mk_mem_project mem query = function
     | `Not_present -> false
     | `Same x -> mem query x
@@ -157,10 +154,6 @@ struct
       Format.fprintf fmt "-> %a %a" pp x pretty_pc flags
     | #correspondance as x -> Correspondance_input.mk_pretty pp fmt x
 
-  let mk_varname f = function
-    | `Partial (x,_) -> f x ^ "_pc"
-    | #correspondance as x -> Correspondance_input.mk_varname f x
-
   let mk_mem_project f p = function
     | `Partial (x,_) -> f p x
     | #correspondance as x -> Correspondance_input.mk_mem_project f p x
diff --git a/src/kernel_services/ast_queries/cil_builtins.ml b/src/kernel_services/ast_queries/cil_builtins.ml
index 8d224fd39bfe2b10a8ebd9de8b1b5185bc06b440..9a825e39a8e08641d6d7de780e0b363fbed8d1cc 100644
--- a/src/kernel_services/ast_queries/cil_builtins.ml
+++ b/src/kernel_services/ast_queries/cil_builtins.ml
@@ -168,7 +168,6 @@ module Builtin_template = struct
         let rehash = Datatype.identity
         let structural_descr = Structural_descr.t_abstract
         let mem_project = Datatype.never_any_project
-        let varname b = "_cb_" ^ b.name
       end)
 end
 module Builtin_templates =
diff --git a/src/kernel_services/ast_queries/cil_datatype.ml b/src/kernel_services/ast_queries/cil_datatype.ml
index 3e9dfcb0c49d6a360967825c6dcff5f712e16064..8dfc722a6cf48dc965edb658b1a22dfe86dcb519 100644
--- a/src/kernel_services/ast_queries/cil_datatype.ml
+++ b/src/kernel_services/ast_queries/cil_datatype.ml
@@ -49,7 +49,6 @@ module Make
        val name: string
        val reprs: t list
        val pretty: Format.formatter -> t -> unit
-       val varname: t -> string
      end) =
   Datatype.Make
     (struct
@@ -69,7 +68,6 @@ module Make_with_collections
        val compare: t -> t -> int
        val equal: t -> t -> bool
        val pretty: Format.formatter -> t -> unit
-       val varname: t -> string
        val hash: t -> int
        val copy: t -> t
      end) =
@@ -158,7 +156,6 @@ module Cabs_file = struct
         let name = "Cabs_file"
         let reprs = [ Datatype.Filepath.dummy, [];
                       Datatype.Filepath.dummy, [ true, Cabs.GLOBANNOT [] ] ]
-        let varname (s, _) = "cabs_" ^ (Filepath.Normalized.to_pretty_string s)
         let pretty fmt cabs = !pretty_ref fmt cabs
       end)
 end
@@ -197,7 +194,7 @@ module Position =  struct
         let copy = Datatype.identity
         let equal: t -> t -> bool = ( = )
         let pretty = Filepath.pp_pos
-        let varname _ = "pos"
+
       end)
   let pp_with_col fmt pos =
     Format.fprintf fmt "%a char %d" pretty pos
@@ -221,7 +218,7 @@ module Location = struct
         let copy = Datatype.identity (* immutable strings *)
         let equal : t -> t -> bool = ( = )
         let pretty fmt loc = !pretty_ref fmt loc
-        let varname _ = "loc"
+
       end)
 
   let pretty_long fmt loc =
@@ -270,7 +267,7 @@ module Instr = struct
         let name = "Instr"
         let reprs = List.map (fun l -> Skip l) Location.reprs
         let pretty fmt x = !pretty_ref fmt x
-        let varname = Datatype.undefined
+
       end)
 
   let loc = function
@@ -294,7 +291,7 @@ module File =
             globinit = None;
             globinitcalled = false } ]
       include Datatype.Undefined
-      let varname _ = "ast"
+
     end)
 
 module Stmt_Id = struct
@@ -316,7 +313,7 @@ module Stmt_Id = struct
         let equal t1 t2 = t1.sid = t2.sid
         let copy = Datatype.undefined
         let pretty fmt s = !pretty_ref fmt s
-        let varname _ = "stmt"
+
       end)
   let id stmt = stmt.sid
 end
@@ -369,7 +366,7 @@ module Kinstr = struct
           | Kglobal ->
             Format.fprintf fmt "Kglobal"
           | Kstmt s -> Stmt.pretty fmt s
-        let varname _ = "ki"
+
       end)
 
   let loc = function
@@ -596,7 +593,6 @@ module Attribute=struct
         let equal = Datatype.from_compare
         let copy = Datatype.undefined
         let pretty fmt t = !pretty_ref fmt t
-        let varname = Datatype.undefined
       end)
 end
 
@@ -620,7 +616,7 @@ struct
         let equal = Datatype.from_compare
         let copy = Datatype.undefined
         let pretty fmt t = !pretty_typ_ref fmt t
-        let varname = Datatype.undefined
+
       end)
 end
 
@@ -713,7 +709,7 @@ module Label = struct
         let reprs =
           [ Label("", Location.unknown, false); Default Location.unknown ]
         let pretty fmt l = !pretty_ref fmt l
-        let varname = Datatype.undefined
+
         let hash = function
           | Default _ -> 7
           | Case (e, _) -> Exp.hash e
@@ -773,7 +769,6 @@ module Varinfo_Id = struct
         let equal v1 v2 = v1.vid = v2.vid
         let copy = Datatype.undefined
         let pretty fmt v = !pretty_ref fmt v
-        let varname v = "vi_" ^ v.vorig_name
       end)
   let id v = v.vid
 end
@@ -809,7 +804,7 @@ module Compinfo = struct
         let equal v1 v2 = v1.ckey = v2.ckey
         let copy = Datatype.undefined
         let pretty fmt f = !pretty_ref fmt f
-        let varname = Datatype.undefined
+
       end)
 end
 
@@ -851,7 +846,7 @@ module Fieldinfo = struct
         let equal f1 f2 = (fid f1) = (fid f2)
         let copy = Datatype.undefined
         let pretty fmt f = !pretty_ref fmt f
-        let varname = Datatype.undefined
+
       end)
 end
 
@@ -1127,7 +1122,7 @@ module Block = struct
           [{battrs=[]; blocals=Varinfo.reprs; bstatics = [];
             bstmts=Stmt.reprs; bscoping=true}]
         let pretty fmt b = !pretty_ref fmt b
-        let varname = Datatype.undefined
+
       end)
   let equal b1 b2 = (b1 == b2)
 end
@@ -1195,7 +1190,7 @@ module Lval = struct
         let hash = hash_lval
         let copy = Datatype.undefined
         let pretty fmt x = !pretty_ref fmt x
-        let varname _ = "lv"
+
       end)
 end
 
@@ -1210,7 +1205,7 @@ module LvalStructEq_input = struct
   let hash = StructEq.hash_lval 13598
   let copy = Datatype.undefined
   let pretty fmt x = !Lval.pretty_ref fmt x
-  let varname _ = "lv"
+
 end
 
 module LvalStructEq = Make_compare_non_strict(LvalStructEq_input)
@@ -1229,7 +1224,7 @@ module Offset = struct
         let hash = hash_offset
         let copy = Datatype.undefined
         let pretty fmt x = !pretty_ref fmt x
-        let varname _ = "offs"
+
       end)
 end
 
@@ -1244,7 +1239,7 @@ module OffsetStructEq_input = struct
   let hash = StructEq.hash_offset 75489
   let copy = Datatype.undefined
   let pretty fmt x = !Offset.pretty_ref fmt x
-  let varname _ = "offs"
+
 end
 
 module OffsetStructEq = Make_compare_non_strict(OffsetStructEq_input)
@@ -1278,7 +1273,7 @@ module Logic_var = struct
         let equal v1 v2 = v1.lv_id = v2.lv_id
         let copy = Datatype.undefined
         let pretty fmt t = !pretty_ref fmt t
-        let varname _ = "logic_var"
+
       end)
 end
 
@@ -1299,7 +1294,7 @@ module Builtin_logic_info = struct
         let equal i1 i2 = i1.bl_name = i2.bl_name
         let copy = Datatype.identity (* works only if an AST is never modified *)
         let pretty fmt li = !pretty_ref fmt li
-        let varname = Datatype.undefined
+
       end)
 end
 
@@ -1316,7 +1311,7 @@ module Logic_type_info = struct
         let hash t = Hashtbl.hash t.lt_name
         let copy = Datatype.identity (* works only if an AST is never modified *)
         let pretty fmt lt = !pretty_ref fmt lt
-        let varname = Datatype.undefined
+
       end)
 end
 
@@ -1335,7 +1330,7 @@ module Logic_ctor_info = struct
         let hash t = Hashtbl.hash t.ctor_name
         let copy = Datatype.identity (* works only if an AST is never modified *)
         let pretty fmt c = !pretty_ref fmt c
-        let varname = Datatype.undefined
+
       end)
 end
 
@@ -1349,7 +1344,7 @@ module Initinfo = struct
           { init = None } ::
           List.map (fun t -> { init = Some (CompoundInit(t, [])) }) Typ.reprs
         let pretty fmt i = !pretty_ref fmt i
-        let varname = Datatype.undefined
+
       end)
 end
 
@@ -1374,7 +1369,7 @@ module Logic_info = struct
         let hash i = Logic_var.hash i.l_var_info
         let copy = Datatype.undefined
         let pretty fmt li = !pretty_ref fmt li
-        let varname _ = "logic_varinfo"
+
       end)
 end
 
@@ -1458,7 +1453,7 @@ module Logic_info_structural = struct
         let hash i = Logic_var.hash i.l_var_info
         let copy = Datatype.undefined
         let pretty fmt li = !Logic_info.pretty_ref fmt li
-        let varname _ = "logic_varinfo"
+
       end)
 end
 
@@ -2044,7 +2039,7 @@ module Logic_constant = struct
         let hash = hash_logic_constant
         let copy = Datatype.undefined
         let pretty fmt lc = !pretty_ref fmt lc
-        let varname _ = "lconst"
+
       end)
 end
 
@@ -2067,7 +2062,7 @@ module Term = struct
         let copy = Datatype.undefined
         let hash = hash_fct hash_term
         let pretty fmt t = !pretty_ref fmt t
-        let varname _ = "term"
+
       end)
 end
 
@@ -2086,7 +2081,7 @@ module Identified_term = struct
           { it_id = x.it_id; it_content = Term.copy x.it_content }
         let hash x = x.it_id
         let pretty fmt t = !pretty_ref fmt t
-        let varname _ = "id_term"
+
       end)
 end
 
@@ -2110,7 +2105,7 @@ module Term_lhost = struct
         let hash = hash_fct hash_tlhost
         let copy = Datatype.undefined
         let pretty fmt h = !pretty_ref fmt h
-        let varname = Datatype.undefined
+
       end)
 end
 
@@ -2126,7 +2121,7 @@ module Term_offset = struct
         let hash = hash_fct hash_toffset
         let copy = Datatype.undefined
         let pretty fmt t_o = !pretty_ref fmt t_o
-        let varname = Datatype.undefined
+
       end)
 end
 
@@ -2153,7 +2148,7 @@ module Logic_label = struct
         let copy = Datatype.undefined
         let hash = hash_label
         let pretty fmt l = !pretty_ref fmt l
-        let varname _ = "logic_label"
+
       end)
 end
 
@@ -2173,7 +2168,7 @@ module Logic_real = struct
         let equal r1 r2 = compare r1 r2 = 0
         let copy = Datatype.undefined
         let pretty fmt t = !pretty_ref fmt t
-        let varname _ = "logic_real"
+
       end)
 end
 
@@ -2185,7 +2180,7 @@ module Global_annotation = struct
         let name = "Global_annotation"
         let reprs = List.map (fun l -> Daxiomatic ("", [],[], l)) Location.reprs
         let pretty fmt v = !pretty_ref fmt v
-        let varname = Datatype.undefined
+
 
         let rec compare g1 g2 =
           match g1,g2 with
@@ -2275,7 +2270,7 @@ module Global = struct
         let name = "Global"
         let reprs = [ GText "" ]
         let pretty fmt v = !pretty_ref fmt v
-        let varname = Datatype.undefined
+
 
         let compare g1 g2 =
           match g1, g2 with
@@ -2428,10 +2423,8 @@ module Kf = struct
           | Declaration (_, v, Some args, _) ->
             !set_formal_decls v args;
             x
-        let get_name_kf kf = (vi kf).Cil_types.vname
         let pretty fmt kf = Varinfo.pretty fmt (vi kf)
         let mem_project = Datatype.never_any_project
-        let varname kf = "kf_" ^ (get_name_kf kf)
       end)
   let () = Type.set_ml_name ty (Some "Kernel_function.ty")
 
@@ -2452,7 +2445,7 @@ module Code_annotation = struct
         let compare x y = Datatype.Int.compare x.annot_id y.annot_id
         let copy = Datatype.undefined
         let pretty fmt ca = !pretty_ref fmt ca
-        let varname _ = "code_annot"
+
       end)
 
   let loc ca = match ca.annot_content with
@@ -2475,7 +2468,7 @@ module Predicate = struct
               pred_loc = Location.unknown;
               pred_content = Pfalse } ]
         let pretty fmt x = !pretty_ref fmt x
-        let varname _ = "p"
+
       end)
 end
 
@@ -2488,7 +2481,7 @@ module Toplevel_predicate = struct
         let reprs =
           [ { tp_statement = List.hd Predicate.reprs; tp_kind = Assert }]
         let pretty fmt x = !pretty_ref fmt x
-        let varname _ = "p"
+
       end)
 end
 
@@ -2505,7 +2498,7 @@ module Identified_predicate = struct
         let copy = Datatype.undefined
         let hash x = x.ip_id
         let pretty fmt x = !pretty_ref fmt x
-        let varname _ = "id_predyes"
+
       end)
 end
 
@@ -2524,7 +2517,7 @@ module PredicateStructEq = struct
         let copy = Datatype.undefined
         let hash = hash_fct hash_predicate
         let pretty fmt x = !pretty_ref fmt x
-        let varname _ = "p"
+
       end)
 end
 
@@ -2590,7 +2583,6 @@ module Fundec = struct
       (struct
         type t = fundec
         let name = "Fundec"
-        let varname v = "fd_" ^ v.svar.vorig_name
         let reprs = reprs
         let structural_descr = Structural_descr.t_abstract
         let compare v1 v2 = Datatype.Int.compare v1.svar.vid v2.svar.vid
@@ -2616,7 +2608,7 @@ module Lexpr = Make
       let name = "Lexpr"
       let reprs = [ { lexpr_node = PLvar ""; lexpr_loc = Location.unknown } ]
       let pretty = Datatype.undefined (* TODO *)
-      let varname = Datatype.undefined
+
     end)
 
 (**************************************************************************)
diff --git a/src/kernel_services/cmdline_parameters/typed_parameter.ml b/src/kernel_services/cmdline_parameters/typed_parameter.ml
index 8a9e8f585ace764499020dc00dd1b4cacc7a9989..7d25ed3ce6510e77f360752e2445a2f6c76bbb05 100644
--- a/src/kernel_services/cmdline_parameters/typed_parameter.ml
+++ b/src/kernel_services/cmdline_parameters/typed_parameter.ml
@@ -67,7 +67,7 @@ include
       let hash x = Datatype.String.hash x.name
       let copy x = x (* The representation of the parameter is immutable *)
       let pretty fmt x = Format.pp_print_string fmt x.name
-      let varname _ = assert false
+
       let mem_project = Datatype.never_any_project
     end)
 
diff --git a/src/kernel_services/plugin_entry_points/emitter.ml b/src/kernel_services/plugin_entry_points/emitter.ml
index fd379811e4179e1a7888fe5bcd48d4428ee8d8a5..63cd6fade3443275b1c75426dad7babc7f715738 100644
--- a/src/kernel_services/plugin_entry_points/emitter.ml
+++ b/src/kernel_services/plugin_entry_points/emitter.ml
@@ -103,7 +103,7 @@ module D =
       let hash x = Datatype.String.hash x.name
       let copy x = x (* strings are immutable here *)
       let pretty fmt x = Format.pp_print_string fmt x.name
-      let varname _ = assert false
+
       let mem_project = Datatype.never_any_project
     end)
 
@@ -147,7 +147,7 @@ module Usable_emitter = struct
             Format.fprintf fmt "%s (v%d)" name x.version
           else
             Format.pp_print_string fmt name
-        let varname _ = assert false
+
         let mem_project = Datatype.never_any_project
       end)
 
diff --git a/src/libraries/datatype/datatype.ml b/src/libraries/datatype/datatype.ml
index 9ae247627dfe4ff5c72df5e9944242d883eb78e4..73a64e236999349175c7d5a58230654659ced653 100644
--- a/src/libraries/datatype/datatype.ml
+++ b/src/libraries/datatype/datatype.ml
@@ -30,7 +30,6 @@ type 'a t =
     hash: 'a -> int;
     copy: 'a -> 'a;
     pretty: Format.formatter -> 'a -> unit;
-    varname: 'a -> string;
     mem_project: (Project_skeleton.t -> bool) -> 'a -> bool }
 
 type 'a info = 'a t
@@ -50,7 +49,6 @@ module type S_no_copy = sig
   val compare: t -> t -> int
   val hash: t -> int
   val pretty: Format.formatter -> t -> unit
-  val varname: t -> string
   val mem_project: (Project_skeleton.t -> bool) -> t -> bool
 end
 
@@ -79,7 +77,6 @@ let compare ty = (internal_info "compare" ty).compare
 let hash ty = (internal_info "hash" ty).hash
 let copy ty = (internal_info "copy" ty).copy
 let pretty ty = (internal_info "pretty" ty).pretty
-let varname ty = (internal_info "varname" ty).varname
 let mem_project ty = (internal_info "mem_project" ty).mem_project
 
 let info ty = internal_info "info" ty
@@ -101,7 +98,6 @@ module type Undefined = sig
   val rehash: 'a -> 'a
   val copy: 'a -> 'a
   val pretty: Format.formatter -> 'a -> unit
-  val varname: 'a -> string
   val mem_project: (Project_skeleton.t -> bool) -> 'a -> bool
 end
 
@@ -111,7 +107,6 @@ module Partial_undefined = struct
   let hash = undefined
   let copy = undefined
   let pretty = undefined
-  let varname = undefined
   let mem_project = undefined
 end
 
@@ -132,11 +127,6 @@ end
 (** {2 Generic builders} *)
 (* ********************************************************************** *)
 
-let valid_varname s =
-  let r = Str.regexp "[^A-Za-z0-9_]+" in
-  let s = Str.global_replace r "__" s in
-  String.uncapitalize_ascii s
-
 let check f fname tname fstr =
   assert
     (if f == undefined && Type.may_use_obj () then begin
@@ -158,7 +148,6 @@ module Build
        val rehash: t -> t
        val copy: t -> t
        val pretty: Format.formatter -> t -> unit
-       val varname: t -> string
        val mem_project: (Project_skeleton.t -> bool) -> t -> bool
      end) =
 struct
@@ -174,13 +163,7 @@ struct
   let hash = T.hash
   let rehash = T.rehash
   let copy = T.copy
-
   let pretty = T.pretty
-
-  let varname =
-    if T.varname == undefined then undefined
-    else fun x -> valid_varname (T.varname x)
-
   let mem_project = T.mem_project
 
   let info =
@@ -189,7 +172,6 @@ struct
       hash = hash;
       copy = copy;
       pretty = pretty;
-      varname = varname;
       mem_project = mem_project }
 
   let () = Infos.add info_tbl T.ty info
@@ -232,7 +214,6 @@ module type Make_input = sig
   val hash: t -> int
   val copy: t -> t
   val pretty: Format.formatter -> t -> unit
-  val varname: t -> string
   val mem_project: (Project_skeleton.t -> bool) -> t -> bool
 end
 
@@ -325,7 +306,6 @@ module type Polymorphic2_input = sig
   val mk_pretty:
     (Format.formatter -> 'a -> unit) -> (Format.formatter -> 'b -> unit) ->
     Format.formatter -> ('a, 'b) t -> unit
-  val mk_varname: ('a -> string) -> ('b -> string) -> ('a, 'b) t -> string
   val mk_mem_project:
     ((Project_skeleton.t -> bool) -> 'a -> bool) ->
     ((Project_skeleton.t -> bool) -> 'b -> bool) ->
@@ -389,7 +369,6 @@ module Polymorphic2(P: Polymorphic2_input) = struct
             in
             build mk T1.copy T2.copy
           let pretty = build P.mk_pretty T1.pretty T2.pretty
-          let varname = build P.mk_varname T1.varname T2.varname
           let mem_project =
             let mk f1 f2 =
               if P.mk_mem_project == undefined then undefined
@@ -439,9 +418,6 @@ module Polymorphic3
          (Format.formatter -> 'b -> unit) ->
          (Format.formatter -> 'c -> unit) ->
          Format.formatter -> ('a, 'b, 'c) t -> unit
-       val mk_varname:
-         ('a -> string) -> ('b -> string) -> ('c -> string) ->
-         ('a, 'b, 'c) t -> string
        val mk_mem_project:
          ((Project_skeleton.t -> bool) -> 'a -> bool) ->
          ((Project_skeleton.t -> bool) -> 'b -> bool) ->
@@ -509,7 +485,6 @@ struct
             in
             build mk T1.copy T2.copy T3.copy
           let pretty = build P.mk_pretty T1.pretty T2.pretty T3.pretty
-          let varname = build P.mk_varname T1.varname T2.varname T3.varname
           let mem_project =
             let mk f1 f2 f3 =
               if P.mk_mem_project == undefined then undefined
@@ -570,9 +545,6 @@ module Polymorphic4
          (Format.formatter -> 'c -> unit) ->
          (Format.formatter -> 'd -> unit) ->
          Format.formatter -> ('a, 'b, 'c, 'd) t -> unit
-       val mk_varname:
-         ('a -> string) -> ('b -> string) -> ('c -> string) -> ('d -> string) ->
-         ('a, 'b, 'c, 'd) t -> string
        val mk_mem_project:
          ((Project_skeleton.t -> bool) -> 'a -> bool) ->
          ((Project_skeleton.t -> bool) -> 'b -> bool) ->
@@ -644,8 +616,6 @@ struct
             in
             build mk T1.copy T2.copy T3.copy T4.copy
           let pretty = build P.mk_pretty T1.pretty T2.pretty T3.pretty T4.pretty
-          let varname =
-            build P.mk_varname T1.varname T2.varname T3.varname T4.varname
           let mem_project =
             let mk f1 f2 f3 f4 =
               if P.mk_mem_project == undefined then undefined
@@ -694,7 +664,6 @@ module Pair_arg = struct
   let mk_pretty f1 f2 fmt (x1, x2) =
     let pp fmt = Format.fprintf fmt "@[<hv 2>%a,@;%a@]" f1 x1 f2 x2 in
     Type.par Type.Basic Type.Tuple fmt pp
-  let mk_varname = undefined
   let mk_mem_project mem1 mem2 f (x1, x2) = mem1 f x1 && mem2 f x2
 end
 
@@ -742,7 +711,6 @@ let pair (type typ1) (type typ2) (ty1: typ1 Type.t) (ty2: typ2 Type.t) =
     let hash = hash X.ty
     let copy = copy X.ty
     let pretty = pretty X.ty
-    let varname = varname ty
     let mem_project = mem_project X.ty
   end
   in
@@ -769,7 +737,6 @@ struct
     let rehash = undefined
     let copy = undefined
     let pretty = undefined
-    let varname _ = "f"
     let mem_project = never_any_project
     let reprs =
       if Type.may_use_obj () then Type.reprs ty else [ fun _ -> assert false ]
@@ -811,7 +778,6 @@ module type Polymorphic_input = sig
   val map: ('a -> 'a) -> 'a t -> 'a t
   val mk_pretty:
     (Format.formatter -> 'a -> unit) -> Format.formatter -> 'a t -> unit
-  val mk_varname: ('a -> string) -> 'a t -> string
   val mk_mem_project:
     ((Project_skeleton.t -> bool) -> 'a -> bool) ->
     (Project_skeleton.t -> bool) -> 'a t -> bool
@@ -875,7 +841,6 @@ module Polymorphic_gen(P: Polymorphic_input) = struct
               fun x -> P.map X.copy x
           let rehash = R.rehash
           let pretty = build P.mk_pretty X.pretty
-          let varname = build P.mk_varname X.varname
           let mem_project =
             let mk f =
               if P.mk_mem_project == undefined then undefined
@@ -926,7 +891,6 @@ module Poly_ref =
       let mk_pretty f fmt x =
         let pp fmt = Format.fprintf fmt "@[<hv 2>ref@;%a@]" f !x in
         Type.par Type.Basic Type.Call fmt pp
-      let mk_varname = undefined
       let mk_mem_project mem f x = mem f !x
     end)
 
@@ -946,7 +910,6 @@ let t_ref (type typ) (ty: typ Type.t) =
       let hash = hash ty
       let copy = copy ty
       let pretty = pretty ty
-      let varname = varname ty
       let mem_project = mem_project ty
     end)
   in
@@ -985,7 +948,6 @@ module Poly_option =
             Format.fprintf fmt "@[<hv 2>Some@;%a@]" f x
           in
           Type.par Type.Basic Type.Call fmt pp
-      let mk_varname = undefined
       let mk_mem_project mem f = function None -> false | Some x -> mem f x
     end)
 
@@ -1006,7 +968,6 @@ let option (type typ) (ty: typ Type.t) =
       let hash = hash ty
       let copy = copy ty
       let pretty = pretty ty
-      let varname = varname ty
       let mem_project = mem_project ty
     end)
   in
@@ -1059,7 +1020,6 @@ module Poly_list =
                print fmt l)
         in
         Type.par Type.Basic Type.Basic fmt pp (* Never enclose lists in parentheses *)
-      let mk_varname = undefined
       let mk_mem_project mem f = List.exists (mem f)
     end)
 
@@ -1080,7 +1040,6 @@ let list (type typ) (ty: typ Type.t) =
       let hash = hash ty
       let copy = copy ty
       let pretty = pretty ty
-      let varname = varname ty
       let mem_project = mem_project ty
     end)
   in
@@ -1144,7 +1103,6 @@ module Poly_array =
                        done))
         in
         Type.par Type.Basic Type.Basic fmt pp (* Never enclose arrays in parentheses *)
-      let mk_varname = undefined
       let mk_mem_project mem f a =
         try
           for i = 0 to (Array.length a - 1) do
@@ -1170,7 +1128,6 @@ let array (type typ) (ty: typ Type.t) =
       let hash = hash ty
       let copy = copy ty
       let pretty = pretty ty
-      let varname = varname ty
       let mem_project = mem_project ty
     end)
   in
@@ -1198,7 +1155,6 @@ module Poly_queue =
       let mk_hash = undefined
       let map = undefined
       let mk_pretty = undefined
-      let mk_varname = undefined
       let mk_mem_project mem f q =
         try Queue.iter (fun x -> if mem f x then raise Exit) q; false
         with Exit -> true
@@ -1220,7 +1176,6 @@ let queue (type typ) (ty: typ Type.t) =
       let hash = hash ty
       let copy = copy ty
       let pretty = pretty ty
-      let varname = varname ty
       let mem_project = mem_project ty
     end)
   in
@@ -1273,7 +1228,6 @@ struct
             ~pre:"@[<hov 2>{@ " ~sep:";@ " ~suf:"@ }@]"
             S.iter (pp_elt E.pretty) fmt s
 
-        let varname = undefined
         let mem_project p s =
           try S.iter (fun x -> if E.mem_project p x then raise Exit) s; false
           with Exit -> true
@@ -1294,7 +1248,6 @@ struct
   let compare = P.compare
   let hash = P.hash
   let pretty = P.pretty
-  let varname = P.varname
   let mem_project = P.mem_project
   let copy = P.copy
 
@@ -1335,9 +1288,6 @@ struct
                  f_value v)
             map;
           Format.fprintf fmt  " }}@]"
-        let mk_varname _ =
-          if Key.varname == undefined then undefined
-          else fun _ -> Format.sprintf "%s_map" Key.name
         let mk_mem_project =
           if Key.mem_project == undefined then undefined
           else
@@ -1416,7 +1366,6 @@ struct
           H.iter (fun k v -> H.add h2 k v) h;
           h2
         let mk_pretty = undefined
-        let mk_varname = undefined
         let mk_mem_project =
           if Key.mem_project == undefined then undefined
           else
@@ -1572,7 +1521,6 @@ module Simple_type
        val reprs: t list
        val pretty: Format.formatter -> t -> unit
        val copy: t -> t
-       val varname: t -> string
        val compare: t -> t -> int
        val equal: t -> t -> bool
      end) =
@@ -1592,7 +1540,6 @@ struct
          let rehash = identity
          let copy = X.copy
          let pretty = X.pretty
-         let varname = X.varname
          let mem_project = never_any_project
        end))
       (struct let module_name = module_name end)
@@ -1611,7 +1558,6 @@ module Unit =
       let compare () () = 0
       let equal () () = true
       let pretty fmt () = Format.fprintf fmt "()"
-      let varname = undefined
     end)
 let unit = Unit.ty
 
@@ -1625,7 +1571,6 @@ module Bool =
       let compare : bool -> bool -> int = Stdlib.compare
       let equal : bool -> bool -> bool = (=)
       let pretty fmt b = Format.fprintf fmt "%B" b
-      let varname _ = "b"
     end)
 let bool = Bool.ty
 
@@ -1639,7 +1584,6 @@ module Int = struct
         let compare : int -> int -> int = Stdlib.compare
         let equal : int -> int -> bool = (=)
         let pretty fmt n = Format.fprintf fmt "%d" n
-        let varname _ = "n"
       end)
   let compare : int -> int -> int = Stdlib.compare
 end
@@ -1655,7 +1599,6 @@ module Int32 =
       let compare = Int32.compare
       let equal : int32 -> int32 -> bool = (=)
       let pretty fmt n = Format.fprintf fmt "%ld" n
-      let varname _ = "n32"
     end)
 let int32 = Int32.ty
 
@@ -1669,7 +1612,6 @@ module Int64 =
       let compare = Int64.compare
       let equal : int64 -> int64 -> bool = (=)
       let pretty fmt n = Format.fprintf fmt "%Ld" n
-      let varname _ = "n64"
     end)
 let int64 = Int64.ty
 
@@ -1683,7 +1625,6 @@ module Nativeint =
       let compare = Nativeint.compare
       let equal : nativeint -> nativeint -> bool = (=)
       let pretty fmt n = Format.fprintf fmt "%nd" n
-      let varname _ = "native_n"
     end)
 let nativeint = Nativeint.ty
 
@@ -1697,7 +1638,6 @@ module Float =
       let compare : float -> float -> int = Stdlib.compare
       let equal : float -> float -> bool = (=)
       let pretty fmt f = Format.fprintf fmt "%f" f
-      let varname _ = "f"
     end)
 let float = Float.ty
 
@@ -1711,7 +1651,6 @@ module Char =
       let compare = Char.compare
       let equal : char -> char -> bool = (=)
       let pretty fmt c = Format.fprintf fmt "%c" c
-      let varname _ = "c"
     end)
 let char = Char.ty
 
@@ -1725,7 +1664,6 @@ module String =
       let compare = String.compare
       let equal : string -> string -> bool = (=)
       let pretty fmt s = Format.fprintf fmt "%S" s
-      let varname _ = "s"
     end)
 let string = String.ty
 
@@ -1742,7 +1680,6 @@ module Formatter =
       let rehash = undefined
       let copy = undefined
       let pretty = undefined
-      let varname _ = "fmt"
       let mem_project = never_any_project
     end)
 let formatter = Formatter.ty
@@ -1761,7 +1698,6 @@ module Integer =
       let copy = identity
       (* TODO: this should take into account kernel's option -big-ints-hex *)
       let pretty = Integer.pretty
-      let varname _ = "integer_n"
       let mem_project = never_any_project
     end)
 let integer = Integer.ty
@@ -1776,7 +1712,6 @@ module Filepath = struct
         let compare = Filepath.Normalized.compare
         let equal : t -> t -> bool = (=)
         let pretty = Filepath.Normalized.pretty
-        let varname _ = "p"
       end)
   let dummy = Filepath.Normalized.empty
   let of_string ?existence ?base_name s =
@@ -1814,7 +1749,6 @@ module Triple_arg = struct
       Format.fprintf fmt "@[<hv 2>%a,@;%a,@;%a@]" f1 x1 f2 x2 f3 x3
     in
     Type.par Type.Basic Type.Tuple fmt pp
-  let mk_varname = undefined
   let mk_mem_project mem1 mem2 mem3 f (x1, x2, x3) =
     mem1 f x1 && mem2 f x2 && mem3 f x3
 end
@@ -1866,7 +1800,6 @@ let triple
     let hash = hash X.ty
     let copy = copy X.ty
     let pretty = pretty X.ty
-    let varname = varname ty
     let mem_project = mem_project X.ty
   end
   in
@@ -1912,7 +1845,6 @@ module Quadruple_arg = struct
       Format.fprintf fmt "@[<hv 2>%a,@;%a,@;%a,@;%a@]" f1 x1 f2 x2 f3 x3 f4 x4
     in
     Type.par Type.Basic Type.Tuple fmt pp
-  let mk_varname = undefined
   let mk_mem_project mem1 mem2 mem3 mem4 f (x1, x2, x3, x4) =
     mem1 f x1 && mem2 f x2 && mem3 f x3 && mem4 f x4
 end
@@ -1969,7 +1901,6 @@ let quadruple
     let hash = hash X.ty
     let copy = copy X.ty
     let pretty = pretty X.ty
-    let varname = varname ty
     let mem_project = mem_project X.ty
   end
   in
diff --git a/src/libraries/datatype/datatype.mli b/src/libraries/datatype/datatype.mli
index 057a592dff5fbc54bf93733e866cd5a111591c47..6f06777de1fdb1622b9c982c38b6f40aee4731dd 100644
--- a/src/libraries/datatype/datatype.mli
+++ b/src/libraries/datatype/datatype.mli
@@ -37,7 +37,6 @@ type 'a t = private
     hash: 'a -> int;
     copy: 'a -> 'a;
     pretty: Format.formatter -> 'a -> unit;
-    varname: 'a -> string;
     mem_project: (Project_skeleton.t -> bool) -> 'a -> bool }
 
 (** A type with its type value. *)
@@ -75,10 +74,6 @@ module type S_no_copy = sig
   val pretty: Format.formatter -> t -> unit
   (** Pretty print each value in an user-friendly way. *)
 
-  val varname: t -> string
-  (** A good prefix name to use for an OCaml variable of this type. Only useful
-      for journalisation. *)
-
   val mem_project: (Project_skeleton.t -> bool) -> t -> bool
   (** [mem_project f x] must return [true] iff there is a value [p] of type
       [Project.t] in [x] such that [f p] returns [true]. *)
@@ -102,7 +97,6 @@ val compare: 'a Type.t -> 'a -> 'a -> int
 val hash: 'a Type.t -> 'a -> int
 val copy: 'a Type.t -> 'a -> 'a
 val pretty: 'a Type.t -> Format.formatter -> 'a -> unit
-val varname: 'a Type.t -> 'a -> string
 val mem_project: 'a Type.t -> (Project_skeleton.t -> bool) -> 'a -> bool
 
 (* ********************************************************************** *)
@@ -137,7 +131,6 @@ module type Undefined = sig
   val rehash: 'a -> 'a
   val copy: 'a -> 'a
   val pretty: Format.formatter -> 'a -> unit
-  val varname: 'a -> string
   val mem_project: (Project_skeleton.t -> bool) -> 'a -> bool
 end
 
@@ -193,7 +186,6 @@ module type Make_input = sig
   val hash: t -> int
   val copy: t -> t
   val pretty: Format.formatter -> t -> unit
-  val varname: t -> string
   val mem_project: (Project_skeleton.t -> bool) -> t -> bool
 
 end
@@ -352,7 +344,6 @@ module Polymorphic
        val map: ('a -> 'a) -> 'a t -> 'a t
        val mk_pretty:
          (Format.formatter -> 'a -> unit) -> Format.formatter -> 'a t -> unit
-       val mk_varname: ('a -> string) -> 'a t -> string
        val mk_mem_project:
          ((Project_skeleton.t -> bool) -> 'a -> bool) ->
          (Project_skeleton.t -> bool) -> 'a t -> bool
@@ -380,7 +371,6 @@ module Polymorphic2
        val mk_pretty:
          (Format.formatter -> 'a -> unit) -> (Format.formatter -> 'b -> unit) ->
          Format.formatter -> ('a, 'b) t -> unit
-       val mk_varname: ('a -> string) -> ('b -> string) -> ('a, 'b) t -> string
        val mk_mem_project:
          ((Project_skeleton.t -> bool) -> 'a -> bool) ->
          ((Project_skeleton.t -> bool) -> 'b -> bool) ->
@@ -417,9 +407,6 @@ module Polymorphic3
          (Format.formatter -> 'b -> unit) ->
          (Format.formatter -> 'c -> unit) ->
          Format.formatter -> ('a, 'b, 'c) t -> unit
-       val mk_varname:
-         ('a -> string) -> ('b -> string) -> ('c -> string) ->
-         ('a, 'b, 'c) t -> string
        val mk_mem_project:
          ((Project_skeleton.t -> bool) -> 'a -> bool) ->
          ((Project_skeleton.t -> bool) -> 'b -> bool) ->
@@ -463,9 +450,6 @@ module Polymorphic4
          (Format.formatter -> 'c -> unit) ->
          (Format.formatter -> 'd -> unit) ->
          Format.formatter -> ('a, 'b, 'c, 'd) t -> unit
-       val mk_varname:
-         ('a -> string) -> ('b -> string) -> ('c -> string) -> ('d -> string) ->
-         ('a, 'b, 'c, 'd) t -> string
        val mk_mem_project:
          ((Project_skeleton.t -> bool) -> 'a -> bool) ->
          ((Project_skeleton.t -> bool) -> 'b -> bool) ->
diff --git a/src/libraries/project/project.ml b/src/libraries/project/project.ml
index 0d47edbedc46ba14b6c969458e9d61f5d9bac06d..f5d4e2a837b94806d8d26895f6362f19711455ca 100644
--- a/src/libraries/project/project.ml
+++ b/src/libraries/project/project.ml
@@ -52,7 +52,6 @@ module D =
       let rehash x = !rehash_ref x
       let copy = Datatype.undefined
       let pretty fmt p = Format.fprintf fmt "project %S" p.unique_name
-      let varname p = "p_" ^ p.name
       let mem_project f x = f x
     end)
 include (D: Datatype.S_no_copy with type t = Project_skeleton.t)
diff --git a/src/libraries/project/state.ml b/src/libraries/project/state.ml
index 0ad6eafe40dfdc63b244ec978ba02893fea76f9c..11e05b3eefeea2b113f0315340a646fd9ed61006 100644
--- a/src/libraries/project/state.ml
+++ b/src/libraries/project/state.ml
@@ -105,7 +105,7 @@ include Datatype.Make_with_collections
       let copy = Datatype.undefined
       let rehash = Datatype.undefined
       let pretty fmt s = Format.fprintf fmt "state %S" s.unique_name
-      let varname = Datatype.undefined
+
       let mem_project = Datatype.never_any_project
     end)
 
diff --git a/src/libraries/utils/hptmap.ml b/src/libraries/utils/hptmap.ml
index d1e5ef01cfc800320c04d84a656d92693ad617be..332c480a6677b154b78fae6c9db6e47499ab9be0 100644
--- a/src/libraries/utils/hptmap.ml
+++ b/src/libraries/utils/hptmap.ml
@@ -681,7 +681,7 @@ struct
 
         let copy = Datatype.undefined
         let pretty = pretty
-        let varname = Datatype.undefined
+
         let mem_project = Datatype.never_any_project
       end)
   let () = Type.set_ml_name D.ty None
diff --git a/src/libraries/utils/rangemap.ml b/src/libraries/utils/rangemap.ml
index a6bd7aa47447265271c9cea525bbb715ef557870..cd50b6aff9f12d4c5430dc6fa4263bc7fca9ec09 100644
--- a/src/libraries/utils/rangemap.ml
+++ b/src/libraries/utils/rangemap.ml
@@ -534,7 +534,7 @@ module Make(Ord: Datatype.S)(Value: Value) = struct
             in aux
 
         let pretty = Datatype.undefined
-        let varname = Datatype.undefined
+
         let mem_project =
           if Ord.mem_project == Datatype.never_any_project &&
              Value.mem_project == Datatype.never_any_project then
diff --git a/src/plugins/aorai/data_for_aorai.ml b/src/plugins/aorai/data_for_aorai.ml
index f0ec1a3c1b9f8cc3da2a9238e9fc88dea54b797a..bafd391331daa282a4e83308df5c4e85932ef93e 100644
--- a/src/plugins/aorai/data_for_aorai.ml
+++ b/src/plugins/aorai/data_for_aorai.ml
@@ -46,7 +46,7 @@ module Aorai_state =
     let compare x y = Datatype.Int.compare x.nums y.nums
     let copy = Datatype.identity
     let pretty fmt x = Format.fprintf fmt "state_%d" x.nums
-    let varname _ = assert false
+
     let mem_project = Datatype.never_any_project
   end
   )
@@ -66,7 +66,7 @@ module Aorai_typed_trans =
     let compare x y = Datatype.Int.compare x.numt y.numt
     let copy = Datatype.identity
     let pretty = Promelaoutput.Typed.print_transition
-    let varname _ = assert false
+
     let mem_project = Datatype.never_any_project
   end)
 
@@ -1821,7 +1821,7 @@ module Range = Datatype.Make_with_collections
             Cil_datatype.Term.pretty c2
         | Unbounded c1 -> Format.fprintf fmt "[%d..]" c1
         | Unknown -> Format.fprintf fmt "[..]"
-      let varname _ = "r"
+
       let mem_project = Datatype.never_any_project
     end)
 
diff --git a/src/plugins/e-acsl/src/analyses/analyses_datatype.ml b/src/plugins/e-acsl/src/analyses/analyses_datatype.ml
index 99645c1fefece09541eeab47ee7f74a0e3412235..7d518f77beeadbf5e13922fef48ee097164f6ec1 100644
--- a/src/plugins/e-acsl/src/analyses/analyses_datatype.ml
+++ b/src/plugins/e-acsl/src/analyses/analyses_datatype.ml
@@ -82,7 +82,7 @@ module Pred_or_term =
         | PoT_pred p -> Printer.pp_predicate fmt p
         | PoT_term t -> Printer.pp_term fmt t
 
-      let varname _ = "pred_or_term"
+
     end)
 
 (** [Ext_logic_label] associates a statement to a label when necessary. For
diff --git a/src/plugins/obfuscator/obfuscator_kind.ml b/src/plugins/obfuscator/obfuscator_kind.ml
index c6902760336c482f5c103dafd3dd78173382c2fd..92896d1c8af3e71feb2c632c29bc5884c63cf722 100644
--- a/src/plugins/obfuscator/obfuscator_kind.ml
+++ b/src/plugins/obfuscator/obfuscator_kind.ml
@@ -85,7 +85,7 @@ include Datatype.Make_with_collections
       let hash (k:k) = Hashtbl.hash k
       let equal (k1:k) k2 = k1 = k2
       let compare (k1:k) k2 = Stdlib.compare k1 k2
-      let varname _ = "k"
+
       let copy = Datatype.identity
       let structural_descr = Structural_descr.t_abstract
       let rehash = Datatype.identity
diff --git a/src/plugins/pdg_types/pdgTypes.ml b/src/plugins/pdg_types/pdgTypes.ml
index 89cbb18c701df356e5399c9990666c50707db0ed..3f215477f38d87124f0462a720180721b8cf4d19 100644
--- a/src/plugins/pdg_types/pdgTypes.ml
+++ b/src/plugins/pdg_types/pdgTypes.ml
@@ -80,7 +80,7 @@ end
          let pretty = print_id
          let rehash = Datatype.identity
          let copy = Datatype.undefined
-         let varname = Datatype.undefined
+
          let mem_project = Datatype.never_any_project
        end)
      : Datatype.S_with_collections with type t := t)
diff --git a/src/plugins/slicing/Slicing.mli b/src/plugins/slicing/Slicing.mli
old mode 100644
new mode 100755
diff --git a/src/plugins/slicing/slicingTypes.ml b/src/plugins/slicing/slicingTypes.ml
index 5391e63fc7871e53ab98f03aad91be8b6e3ae4a5..74a1954e1560c16577e1c63fa60b8e4a8492a2ec 100644
--- a/src/plugins/slicing/slicingTypes.ml
+++ b/src/plugins/slicing/slicingTypes.ml
@@ -65,7 +65,7 @@ module Fct_user_crit =
       let reprs = [ SlicingInternals.dummy_fct_user_crit ]
       let name = "SlicingTypes.Fct_user_crit"
       let mem_project = Datatype.never_any_project
-      let varname _ = "user_criteria"
+
     end)
 
 (** Function slice *)
@@ -88,7 +88,6 @@ module Sl_project =
       type t = sl_project
       let reprs = [ SlicingInternals.dummy_project ]
       let name = "SlicingTypes.Sl_project"
-      let varname _s = "sl_project_"
       let mem_project = Datatype.never_any_project
     end)
 
@@ -102,7 +101,6 @@ module Sl_select =
           (fun v -> v, SlicingInternals.dummy_fct_user_crit)
           Cil_datatype.Varinfo.reprs
       let name = "SlicingTypes.Sl_select"
-      let varname _s = "sl_select"
       let mem_project = Datatype.never_any_project
     end)
 
@@ -175,7 +173,7 @@ module Sl_mark =
       let rehash = Datatype.undefined
       let pretty = pp_sl_mark
       let mem_project = Datatype.never_any_project
-      let varname = Datatype.undefined
+
     end)
 
 let dyn_sl_mark = Sl_mark.ty
diff --git a/src/plugins/value/partitioning/split_strategy.ml b/src/plugins/value/partitioning/split_strategy.ml
index c99e49e1754ef8734e1c0c41bcc0121070da8a3d..2bd967b0b95739cbad939ab3570aea0c098271f0 100644
--- a/src/plugins/value/partitioning/split_strategy.ml
+++ b/src/plugins/value/partitioning/split_strategy.ml
@@ -64,7 +64,7 @@ include
       | SplitEqList l ->
         Format.fprintf fmt "Split on \\result == %a"
           (Pretty_utils.pp_list ~sep:",@ " Datatype.Integer.pretty) l
-    let varname _ = "v"
+
     let mem_project = Datatype.never_any_project
   end)
 
diff --git a/src/plugins/value/values/offsm_value.ml b/src/plugins/value/values/offsm_value.ml
index 4408fd246315f1c962ab9ca2082117b80583a4a7..28b0cbfff37816d9e7e23416893d87704a75ecae 100644
--- a/src/plugins/value/values/offsm_value.ml
+++ b/src/plugins/value/values/offsm_value.ml
@@ -375,7 +375,7 @@ module Datatype_Offsm_or_top = Datatype.Make_with_collections(struct
     let pretty fmt = function
       | Top -> Format.pp_print_string fmt "TopO"
       | O o -> Format.fprintf fmt "O @[%a@]" V_Offsetmap.pretty o
-    let varname _ = "o"
+
     let mem_project = Datatype.never_any_project
   end)
 
diff --git a/src/plugins/value_types/cvalue.ml b/src/plugins/value_types/cvalue.ml
index e1fc93ee85a0f9a53603e027839f68a585f03a9d..3640e3bc0f5714f61e7a1a7051c2fcc8673faa55 100644
--- a/src/plugins/value_types/cvalue.ml
+++ b/src/plugins/value_types/cvalue.ml
@@ -857,7 +857,7 @@ module V_Or_Uninitialized = struct
          let copy = Datatype.undefined
          let rehash = Datatype.identity
          let pretty = pretty
-         let varname = Datatype.undefined
+
          let mem_project = Datatype.never_any_project
        end)
      : Datatype.S with type t := t)
diff --git a/src/plugins/value_types/function_Froms.ml b/src/plugins/value_types/function_Froms.ml
index 00d0cfa6ad486c2052c0d3deccc68804d7075df8..e894f38ca7bfe8bfc2eaa1d0aacec86320d4f8bd 100644
--- a/src/plugins/value_types/function_Froms.ml
+++ b/src/plugins/value_types/function_Froms.ml
@@ -57,7 +57,7 @@ struct
       let rehash = Datatype.identity
 
       let mem_project = Datatype.never_any_project
-      let varname _ = "da"
+
 
       let copy = Datatype.undefined
     end)
@@ -177,7 +177,7 @@ module DepsOrUnassigned = struct
       let rehash = Datatype.identity
 
       let mem_project = Datatype.never_any_project
-      let varname _ = "d"
+
 
       let copy = Datatype.undefined
 
@@ -625,7 +625,7 @@ include Datatype.Make
       let pretty = pretty
       let rehash = Datatype.identity
       let copy = Datatype.undefined
-      let varname = Datatype.undefined
+
       let mem_project = Datatype.never_any_project
     end)
 
diff --git a/src/plugins/wp/Lang.ml b/src/plugins/wp/Lang.ml
index bf35e910cd26b721b40d38a5100f0118a4d0852b..74b70f769ec85136aff93f5bc9c1ad685a0bc9bf 100644
--- a/src/plugins/wp/Lang.ml
+++ b/src/plugins/wp/Lang.ml
@@ -682,7 +682,7 @@ struct
         let compare = Datatype.undefined
         let hash = Datatype.undefined
         let copy _old = QZERO.create ()
-        let varname = Datatype.undefined
+
         let pretty = Datatype.undefined
         let mem_project _ _ = false
       end)
diff --git a/src/plugins/wp/ctypes.ml b/src/plugins/wp/ctypes.ml
index befde6664008ca58bcf8b9f20465631294c59169..31e45621337fae346e0a748fef4e81718708fb84 100644
--- a/src/plugins/wp/ctypes.ml
+++ b/src/plugins/wp/ctypes.ml
@@ -584,7 +584,7 @@ module C_object = Datatype.Make(struct
 
     let mem_project = Datatype.Undefined.mem_project
 
-    let varname _ = "co"
+
   end)
 
 let rec compare_ptr_conflated a b =
diff --git a/src/plugins/wp/wpPropId.ml b/src/plugins/wp/wpPropId.ml
index ec12ebe8695b4e50e4084c767b18c02d0425c2a6..0a6356d6aef4ba0a2653ee0e24ba71a5534ffbe6 100644
--- a/src/plugins/wp/wpPropId.ml
+++ b/src/plugins/wp/wpPropId.ml
@@ -262,7 +262,7 @@ module PropIdRaw =
     let rehash = Datatype.identity
     let pretty = Datatype.undefined
     let mem_project = Datatype.never_any_project
-    let varname = Datatype.undefined
+
   end)
 
 (* -------------------------------------------------------------------------- *)