Fix pretty printing problem for substfree variables

types/types.ml

@@ -2608,7 +2608,7 @@ struct
       try Hashtbl.find h d
       with Not_found -> begin
         let id = Printf.sprintf "_%s_%d" (Var.id d) !idx in
-        let x = var (Var.mk ~fresh:false id) in
+        let x = var (Var.mk ~fresh:false ~repr:(Var.id d) id) in
         incr idx;
         Hashtbl.add h d x ;
         x

types/var.ml

 
 module V = struct
-  type t = { fresh : bool; id : string; }
-  let dump ppf t = Format.fprintf ppf "{id=%s;fresh=%b}" t.id t.fresh
+  type t = { fresh : bool; id : string; repr : string }
+  let dump ppf t = 
+    let r = if t.repr = t.id then "" else Format.sprintf ";repr=%s" t.repr in
+    Format.fprintf ppf "{id=%s;fresh=%b%s}" t.id t.fresh r
   let compare x y = Pervasives.compare x.id y.id
   let equal x y = Pervasives.compare x.id y.id = 0
   let hash x = Hashtbl.hash x.id
   let check _ = ()
 
-  let make_id ?(fresh=false) id = { id = id ; fresh = fresh }
+  let make_id ?(fresh=false) ?repr id =
+    match repr with
+    |None -> { id = id ; fresh = fresh ; repr = id }
+    |Some r -> { id = id ; fresh = fresh ; repr = r }
 end
 
 type var = [ `Var of V.t ]
 type t = var
 let dump ppf (`Var x) = Format.fprintf ppf "%a" V.dump x
-let pp ppf (`Var x) = Format.fprintf ppf "'%s" x.V.id
+let pp ppf (`Var x) = Format.fprintf ppf "'%s" x.V.repr
 let compare (`Var x) (`Var y) = V.compare x y
 let equal v1 v2 = (compare v1 v2) = 0
 let hash (`Var x) = V.hash x
 let check _ = ()
 
-let mk ?fresh id = `Var (V.make_id ?fresh id)
+let mk ?fresh ?repr id = `Var (V.make_id ?fresh ?repr id)
 let fresh : ?pre: string -> unit -> [> var ] =
   let counter = ref 0 in
   fun ?(pre="_fresh_") -> fun _ ->

types/var.mli

 module V : sig
   include Custom.T
-  val make_id : ?fresh:bool -> string -> t
+  val make_id : ?fresh:bool -> ?repr:string -> string -> t
 end
 
 type var = [ `Var of V.t ]
@@ -8,7 +8,7 @@ type var = [ `Var of V.t ]
 include Custom.T with type t = var
 
 val pp : Format.formatter -> var -> unit
-val mk : ?fresh:bool -> string -> var
+val mk : ?fresh:bool -> ?repr:string -> string -> var
 val fresh : ?pre:string -> unit -> var
 val id : var -> string
 val is_fresh : var -> bool