diff --git a/infer/src/IR/Sil.ml b/infer/src/IR/Sil.ml
index 0314f5073..3e2d6cf6b 100644
--- a/infer/src/IR/Sil.ml
+++ b/infer/src/IR/Sil.ml
@@ -1078,46 +1078,33 @@ type ident_exp = Ident.t * Exp.t [@@deriving compare]
 
 let compare_ident_exp_ids (id1, _) (id2, _) = Ident.compare id1 id2
 
-type exp_subst = ident_exp list [@@deriving compare]
+type subst = ident_exp list [@@deriving compare]
 
-type subst = [`Exp of exp_subst | `Typ of Typ.type_subst_t] [@@deriving compare]
+type subst_fun = Ident.t -> Exp.t
 
-type subst_fun = [`Exp of Ident.t -> Exp.t | `Typ of (Typ.t -> Typ.t) * (Typ.Name.t -> Typ.Name.t)]
-
-let equal_exp_subst = [%compare.equal: exp_subst]
+let equal_subst = [%compare.equal: subst]
 
 let sub_no_duplicated_ids sub = not (List.contains_dup ~compare:compare_ident_exp_ids sub)
 
 (** Create a substitution from a list of pairs.
     For all (id1, e1), (id2, e2) in the input list,
     if id1 = id2, then e1 = e2. *)
-let exp_subst_of_list sub =
+let subst_of_list sub =
   let sub' = List.dedup_and_sort ~compare:compare_ident_exp sub in
   assert (sub_no_duplicated_ids sub') ;
   sub'
 
 
-let subst_of_list sub = `Exp (exp_subst_of_list sub)
-
-(** like exp_subst_of_list, but allow duplicate ids and only keep the first occurrence *)
-let exp_subst_of_list_duplicates sub = List.dedup_and_sort ~compare:compare_ident_exp_ids sub
+(** like subst_of_list, but allow duplicate ids and only keep the first occurrence *)
+let subst_of_list_duplicates sub = List.dedup_and_sort ~compare:compare_ident_exp_ids sub
 
 (** Convert a subst to a list of pairs. *)
 let sub_to_list sub = sub
 
 (** The empty substitution. *)
-let exp_sub_empty = exp_subst_of_list []
-
-let sub_empty = `Exp exp_sub_empty
-
-let is_sub_empty = function
-  | `Exp [] ->
-      true
-  | `Exp _ ->
-      false
-  | `Typ sub ->
-      Typ.is_type_subst_empty sub
+let sub_empty = subst_of_list []
 
+let is_sub_empty = List.is_empty
 
 (** Join two substitutions into one.
     For all id in dom(sub1) cap dom(sub2), sub1(id) = sub2(id). *)
@@ -1150,11 +1137,11 @@ let sub_symmetric_difference sub1_in sub2_in =
 
 (** [sub_find filter sub] returns the expression associated to the first identifier
     that satisfies [filter]. Raise [Not_found] if there isn't one. *)
-let sub_find filter (sub : exp_subst) = snd (List.find_exn ~f:(fun (i, _) -> filter i) sub)
+let sub_find filter (sub : subst) = snd (List.find_exn ~f:(fun (i, _) -> filter i) sub)
 
 (** [sub_filter filter sub] restricts the domain of [sub] to the
     identifiers satisfying [filter]. *)
-let sub_filter filter (sub : exp_subst) = List.filter ~f:(fun (i, _) -> filter i) sub
+let sub_filter filter (sub : subst) = List.filter ~f:(fun (i, _) -> filter i) sub
 
 (** [sub_filter_pair filter sub] restricts the domain of [sub] to the
     identifiers satisfying [filter(id, sub(id))]. *)
@@ -1162,15 +1149,11 @@ let sub_filter_pair = List.filter
 
 (** [sub_range_partition filter sub] partitions [sub] according to
     whether range expressions satisfy [filter]. *)
-let sub_range_partition filter (sub : exp_subst) =
-  List.partition_tf ~f:(fun (_, e) -> filter e) sub
-
+let sub_range_partition filter (sub : subst) = List.partition_tf ~f:(fun (_, e) -> filter e) sub
 
 (** [sub_domain_partition filter sub] partitions [sub] according to
     whether domain identifiers satisfy [filter]. *)
-let sub_domain_partition filter (sub : exp_subst) =
-  List.partition_tf ~f:(fun (i, _) -> filter i) sub
-
+let sub_domain_partition filter (sub : subst) = List.partition_tf ~f:(fun (i, _) -> filter i) sub
 
 (** Return the list of identifiers in the domain of the substitution. *)
 let sub_domain sub = List.map ~f:fst sub
@@ -1179,42 +1162,36 @@ let sub_domain sub = List.map ~f:fst sub
 let sub_range sub = List.map ~f:snd sub
 
 (** [sub_range_map f sub] applies [f] to the expressions in the range of [sub]. *)
-let sub_range_map f sub = exp_subst_of_list (List.map ~f:(fun (i, e) -> (i, f e)) sub)
+let sub_range_map f sub = subst_of_list (List.map ~f:(fun (i, e) -> (i, f e)) sub)
 
 (** [sub_map f g sub] applies the renaming [f] to identifiers in the domain
     of [sub] and the substitution [g] to the expressions in the range of [sub]. *)
-let sub_map f g sub = exp_subst_of_list (List.map ~f:(fun (i, e) -> (f i, g e)) sub)
+let sub_map f g sub = subst_of_list (List.map ~f:(fun (i, e) -> (f i, g e)) sub)
 
 let mem_sub id sub = List.exists ~f:(fun (id1, _) -> Ident.equal id id1) sub
 
 (** Extend substitution and return [None] if not possible. *)
-let extend_sub sub id exp : exp_subst option =
+let extend_sub sub id exp : subst option =
   let compare (id1, _) (id2, _) = Ident.compare id1 id2 in
   if mem_sub id sub then None else Some (List.merge ~compare sub [(id, exp)])
 
 
 (** Free auxilary variables in the domain and range of the substitution. *)
-let exp_subst_gen_free_vars sub =
+let subst_gen_free_vars sub =
   let open Sequence.Generator in
   ISequence.gen_sequence_list sub ~f:(fun (id, e) -> yield id >>= fun () -> Exp.gen_free_vars e)
 
 
-let exp_subst_free_vars sub = Sequence.Generator.run (exp_subst_gen_free_vars sub)
+let subst_free_vars sub = Sequence.Generator.run (subst_gen_free_vars sub)
 
 let rec exp_sub_ids (f : subst_fun) exp =
-  let f_typ x = match f with `Exp _ -> x | `Typ (f, _) -> f x in
-  let f_tname x = match f with `Exp _ -> x | `Typ (_, f) -> f x in
   match (exp : Exp.t) with
   | Var id -> (
-    match f with
-    | `Exp f_exp -> (
-      match f_exp id with
-      | Exp.Var id' when Ident.equal id id' ->
-          exp (* it will preserve physical equality when needed *)
-      | exp' ->
-          exp' )
-    | _ ->
-        exp )
+    match f id with
+    | Exp.Var id' when Ident.equal id id' ->
+        exp (* it will preserve physical equality when needed *)
+    | exp' ->
+        exp' )
   | Lvar _ ->
       exp
   | Exn e ->
@@ -1225,8 +1202,7 @@ let rec exp_sub_ids (f : subst_fun) exp =
         IList.map_changed ~equal:[%compare.equal: Exp.t * Pvar.t * Typ.t]
           ~f:(fun ((e, pvar, typ) as captured) ->
             let e' = exp_sub_ids f e in
-            let typ' = f_typ typ in
-            if phys_equal e' e && phys_equal typ typ' then captured else (e', pvar, typ') )
+            if phys_equal e' e then captured else (e', pvar, typ) )
           c.captured_vars
       in
       if phys_equal captured_vars c.captured_vars then exp else Exp.Closure {c with captured_vars}
@@ -1234,54 +1210,31 @@ let rec exp_sub_ids (f : subst_fun) exp =
       exp
   | Cast (t, e) ->
       let e' = exp_sub_ids f e in
-      let t' = f_typ t in
-      if phys_equal e' e && phys_equal t' t then exp else Exp.Cast (t', e')
+      if phys_equal e' e then exp else Exp.Cast (t, e')
   | UnOp (op, e, typ_opt) ->
       let e' = exp_sub_ids f e in
-      let typ_opt' =
-        match typ_opt with
-        | Some t ->
-            let t' = f_typ t in
-            if phys_equal t t' then typ_opt else Some t'
-        | None ->
-            typ_opt
-      in
-      if phys_equal e' e && phys_equal typ_opt typ_opt' then exp else Exp.UnOp (op, e', typ_opt')
+      if phys_equal e' e then exp else Exp.UnOp (op, e', typ_opt)
   | BinOp (op, e1, e2) ->
       let e1' = exp_sub_ids f e1 in
       let e2' = exp_sub_ids f e2 in
       if phys_equal e1' e1 && phys_equal e2' e2 then exp else Exp.BinOp (op, e1', e2')
   | Lfield (e, fld, typ) ->
       let e' = exp_sub_ids f e in
-      let typ' = f_typ typ in
-      let fld' = Typ.Fieldname.class_name_replace ~f:f_tname fld in
-      if phys_equal e' e && phys_equal typ typ' && phys_equal fld fld' then exp
-      else Exp.Lfield (e', fld', typ')
+      if phys_equal e' e then exp else Exp.Lfield (e', fld, typ)
   | Lindex (e1, e2) ->
       let e1' = exp_sub_ids f e1 in
       let e2' = exp_sub_ids f e2 in
       if phys_equal e1' e1 && phys_equal e2' e2 then exp else Exp.Lindex (e1', e2')
-  | Sizeof ({typ; dynamic_length= Some l; subtype} as sizeof_data) ->
+  | Sizeof ({dynamic_length= Some l} as sizeof_data) ->
       let l' = exp_sub_ids f l in
-      let typ' = f_typ typ in
-      let subtype' = Subtype.sub_type f_tname subtype in
-      if phys_equal l' l && phys_equal typ typ' && phys_equal subtype subtype' then exp
-      else Exp.Sizeof {sizeof_data with typ= typ'; dynamic_length= Some l'; subtype= subtype'}
-  | Sizeof ({typ; dynamic_length= None; subtype} as sizeof_data) ->
-      let typ' = f_typ typ in
-      let subtype' = Subtype.sub_type f_tname subtype in
-      if phys_equal typ typ' then exp
-      else Exp.Sizeof {sizeof_data with typ= typ'; subtype= subtype'}
+      if phys_equal l' l then exp else Exp.Sizeof {sizeof_data with dynamic_length= Some l'}
+  | Sizeof {dynamic_length= None} ->
+      exp
 
 
 let apply_sub subst : subst_fun =
-  match subst with
-  | `Exp l ->
-      `Exp
-        (fun id ->
-          match List.Assoc.find l ~equal:Ident.equal id with Some x -> x | None -> Exp.Var id )
-  | `Typ typ_subst ->
-      `Typ (Typ.sub_type typ_subst, Typ.sub_tname typ_subst)
+ fun id ->
+  match List.Assoc.find subst ~equal:Ident.equal id with Some x -> x | None -> Exp.Var id
 
 
 let exp_sub (subst : subst) e = exp_sub_ids (apply_sub subst) e
@@ -1291,27 +1244,22 @@ let instr_sub_ids ~sub_id_binders f instr =
   let sub_id id =
     match exp_sub_ids f (Var id) with Var id' when not (Ident.equal id id') -> id' | _ -> id
   in
-  let sub_typ x = match f with `Exp _ -> x | `Typ (f, _) -> f x in
   match instr with
   | Load (id, rhs_exp, typ, loc) ->
       let id' = if sub_id_binders then sub_id id else id in
       let rhs_exp' = exp_sub_ids f rhs_exp in
-      let typ' = sub_typ typ in
-      if phys_equal id' id && phys_equal rhs_exp' rhs_exp && phys_equal typ typ' then instr
-      else Load (id', rhs_exp', typ', loc)
+      if phys_equal id' id && phys_equal rhs_exp' rhs_exp then instr
+      else Load (id', rhs_exp', typ, loc)
   | Store (lhs_exp, typ, rhs_exp, loc) ->
       let lhs_exp' = exp_sub_ids f lhs_exp in
-      let typ' = sub_typ typ in
       let rhs_exp' = exp_sub_ids f rhs_exp in
-      if phys_equal lhs_exp' lhs_exp && phys_equal typ typ' && phys_equal rhs_exp' rhs_exp then
-        instr
-      else Store (lhs_exp', typ', rhs_exp', loc)
+      if phys_equal lhs_exp' lhs_exp && phys_equal rhs_exp' rhs_exp then instr
+      else Store (lhs_exp', typ, rhs_exp', loc)
   | Call (((id, typ) as ret_id_typ), fun_exp, actuals, call_flags, loc) ->
       let ret_id' =
         if sub_id_binders then
           let id' = sub_id id in
-          let typ' = sub_typ typ in
-          if Ident.equal id id' && phys_equal typ typ' then ret_id_typ else (id', typ')
+          if Ident.equal id id' then ret_id_typ else (id', typ)
         else ret_id_typ
       in
       let fun_exp' = exp_sub_ids f fun_exp in
@@ -1319,9 +1267,7 @@ let instr_sub_ids ~sub_id_binders f instr =
         IList.map_changed ~equal:[%compare.equal: Exp.t * Typ.t]
           ~f:(fun ((actual, typ) as actual_pair) ->
             let actual' = exp_sub_ids f actual in
-            let typ' = sub_typ typ in
-            if phys_equal actual' actual && phys_equal typ typ' then actual_pair
-            else (actual', typ') )
+            if phys_equal actual' actual then actual_pair else (actual', typ) )
           actuals
       in
       if
@@ -1549,8 +1495,7 @@ let hpara_instantiate para e1 e2 elist =
     try List.map2_exn ~f:g para.evars ids_evars with Invalid_argument _ -> assert false
   in
   let subst =
-    `Exp
-      (exp_subst_of_list (((para.root, e1) :: (para.next, e2) :: subst_for_svars) @ subst_for_evars))
+    subst_of_list (((para.root, e1) :: (para.next, e2) :: subst_for_svars) @ subst_for_evars)
   in
   (ids_evars, List.map ~f:(hpred_sub subst) para.body)
 
@@ -1574,10 +1519,9 @@ let hpara_dll_instantiate (para : hpara_dll) cell blink flink elist =
     try List.map2_exn ~f:g para.evars_dll ids_evars with Invalid_argument _ -> assert false
   in
   let subst =
-    `Exp
-      (exp_subst_of_list
-         ( ((para.cell, cell) :: (para.blink, blink) :: (para.flink, flink) :: subst_for_svars)
-         @ subst_for_evars ))
+    subst_of_list
+      ( ((para.cell, cell) :: (para.blink, blink) :: (para.flink, flink) :: subst_for_svars)
+      @ subst_for_evars )
   in
   (ids_evars, List.map ~f:(hpred_sub subst) para.body_dll)
 
diff --git a/infer/src/IR/Sil.mli b/infer/src/IR/Sil.mli
index 16871c99f..3951e8402 100644
--- a/infer/src/IR/Sil.mli
+++ b/infer/src/IR/Sil.mli
@@ -385,87 +385,79 @@ val hpara_dll_shallow_free_vars : hpara_dll -> Ident.t Sequence.t
 
 (** {2 Substitution} *)
 
-type exp_subst = private (Ident.t * Exp.t) list [@@deriving compare]
+type subst = private (Ident.t * Exp.t) list [@@deriving compare]
 
-type subst = [`Exp of exp_subst | `Typ of Typ.type_subst_t] [@@deriving compare]
-
-val equal_exp_subst : exp_subst -> exp_subst -> bool
+val equal_subst : subst -> subst -> bool
 (** Equality for substitutions. *)
 
-val exp_subst_of_list : (Ident.t * Exp.t) list -> exp_subst
+val subst_of_list : (Ident.t * Exp.t) list -> subst
 (** Create a substitution from a list of pairs.
     For all (id1, e1), (id2, e2) in the input list,
     if id1 = id2, then e1 = e2. *)
 
-val subst_of_list : (Ident.t * Exp.t) list -> subst
-
-val exp_subst_of_list_duplicates : (Ident.t * Exp.t) list -> exp_subst
-(** like exp_subst_of_list, but allow duplicate ids and only keep the first occurrence *)
+val subst_of_list_duplicates : (Ident.t * Exp.t) list -> subst
+(** like subst_of_list, but allow duplicate ids and only keep the first occurrence *)
 
-val sub_to_list : exp_subst -> (Ident.t * Exp.t) list
+val sub_to_list : subst -> (Ident.t * Exp.t) list
 (** Convert a subst to a list of pairs. *)
 
 val sub_empty : subst
 (** The empty substitution. *)
 
-val exp_sub_empty : exp_subst
-
 val is_sub_empty : subst -> bool
 
-(* let to_exp_subst : [< `Exp exp_subst] => exp_subst; *)
-
-val sub_join : exp_subst -> exp_subst -> exp_subst
+val sub_join : subst -> subst -> subst
 (** Compute the common id-exp part of two inputs [subst1] and [subst2].
     The first component of the output is this common part.
     The second and third components are the remainder of [subst1]
     and [subst2], respectively. *)
 
-val sub_symmetric_difference : exp_subst -> exp_subst -> exp_subst * exp_subst * exp_subst
+val sub_symmetric_difference : subst -> subst -> subst * subst * subst
 (** Compute the common id-exp part of two inputs [subst1] and [subst2].
     The first component of the output is this common part.
     The second and third components are the remainder of [subst1]
     and [subst2], respectively. *)
 
-val sub_find : (Ident.t -> bool) -> exp_subst -> Exp.t
+val sub_find : (Ident.t -> bool) -> subst -> Exp.t
 (** [sub_find filter sub] returns the expression associated to the first identifier
     that satisfies [filter].
     Raise [Not_found] if there isn't one. *)
 
-val sub_filter : (Ident.t -> bool) -> exp_subst -> exp_subst
+val sub_filter : (Ident.t -> bool) -> subst -> subst
 (** [sub_filter filter sub] restricts the domain of [sub] to the
     identifiers satisfying [filter]. *)
 
-val sub_filter_pair : exp_subst -> f:(Ident.t * Exp.t -> bool) -> exp_subst
+val sub_filter_pair : subst -> f:(Ident.t * Exp.t -> bool) -> subst
 (** [sub_filter_exp filter sub] restricts the domain of [sub] to the
     identifiers satisfying [filter(id, sub(id))]. *)
 
-val sub_range_partition : (Exp.t -> bool) -> exp_subst -> exp_subst * exp_subst
+val sub_range_partition : (Exp.t -> bool) -> subst -> subst * subst
 (** [sub_range_partition filter sub] partitions [sub] according to
     whether range expressions satisfy [filter]. *)
 
-val sub_domain_partition : (Ident.t -> bool) -> exp_subst -> exp_subst * exp_subst
+val sub_domain_partition : (Ident.t -> bool) -> subst -> subst * subst
 (** [sub_domain_partition filter sub] partitions [sub] according to
     whether domain identifiers satisfy [filter]. *)
 
-val sub_domain : exp_subst -> Ident.t list
+val sub_domain : subst -> Ident.t list
 (** Return the list of identifiers in the domain of the substitution. *)
 
-val sub_range : exp_subst -> Exp.t list
+val sub_range : subst -> Exp.t list
 (** Return the list of expressions in the range of the substitution. *)
 
-val sub_range_map : (Exp.t -> Exp.t) -> exp_subst -> exp_subst
+val sub_range_map : (Exp.t -> Exp.t) -> subst -> subst
 (** [sub_range_map f sub] applies [f] to the expressions in the range of [sub]. *)
 
-val sub_map : (Ident.t -> Ident.t) -> (Exp.t -> Exp.t) -> exp_subst -> exp_subst
+val sub_map : (Ident.t -> Ident.t) -> (Exp.t -> Exp.t) -> subst -> subst
 (** [sub_map f g sub] applies the renaming [f] to identifiers in the domain
     of [sub] and the substitution [g] to the expressions in the range of [sub]. *)
 
-val extend_sub : exp_subst -> Ident.t -> Exp.t -> exp_subst option
+val extend_sub : subst -> Ident.t -> Exp.t -> subst option
 (** Extend substitution and return [None] if not possible. *)
 
-val exp_subst_free_vars : exp_subst -> Ident.t Sequence.t
+val subst_free_vars : subst -> Ident.t Sequence.t
 
-val exp_subst_gen_free_vars : exp_subst -> (unit, Ident.t) Sequence.Generator.t
+val subst_gen_free_vars : subst -> (unit, Ident.t) Sequence.Generator.t
 
 (** substitution functions
     WARNING: these functions do not ensure that the results are normalized. *)
diff --git a/infer/src/IR/Subtype.ml b/infer/src/IR/Subtype.ml
index c3739cde9..63741e3b1 100644
--- a/infer/src/IR/Subtype.ml
+++ b/infer/src/IR/Subtype.ml
@@ -32,16 +32,6 @@ type result = No | Unknown | Yes [@@deriving compare]
 
 let equal_result = [%compare.equal: result]
 
-let sub_type tname_subst st_pair =
-  let st, kind = st_pair in
-  match st with
-  | Subtypes tnames ->
-      let tnames' = IList.map_changed ~equal:Typ.Name.equal ~f:tname_subst tnames in
-      if phys_equal tnames tnames' then st_pair else (Subtypes tnames', kind)
-  | Exact ->
-      st_pair
-
-
 let max_result res1 res2 = if compare_result res1 res2 <= 0 then res2 else res1
 
 let is_interface tenv (class_name : Typ.Name.t) =
diff --git a/infer/src/IR/Subtype.mli b/infer/src/IR/Subtype.mli
index a654c0d34..3261c55cd 100644
--- a/infer/src/IR/Subtype.mli
+++ b/infer/src/IR/Subtype.mli
@@ -15,8 +15,6 @@ type t [@@deriving compare]
 
 val pp : F.formatter -> t -> unit
 
-val sub_type : (Typ.Name.t -> Typ.Name.t) -> t -> t
-
 val exact : t
 
 val subtypes : t
diff --git a/infer/src/IR/Typ.ml b/infer/src/IR/Typ.ml
index ec64051a4..dd51aa728 100644
--- a/infer/src/IR/Typ.ml
+++ b/infer/src/IR/Typ.ml
@@ -150,8 +150,6 @@ module T = struct
 
   let equal_quals = [%compare.equal: type_quals]
 
-  let equal_template_arg = [%compare.equal: template_arg]
-
   let equal = [%compare.equal: t]
 end
 
@@ -186,12 +184,6 @@ let void = mk Tvoid
 
 let void_star = mk (Tptr (mk Tvoid, Pk_pointer))
 
-let merge_quals quals1 quals2 =
-  { is_const= quals1.is_const || quals2.is_const
-  ; is_restrict= quals1.is_restrict || quals2.is_restrict
-  ; is_volatile= quals1.is_volatile || quals2.is_volatile }
-
-
 let escape pe = if Pp.equal_print_kind pe.Pp.kind Pp.HTML then Escape.escape_xml else ident
 
 (** Pretty print a type with all the details, using the C syntax. *)
@@ -269,51 +261,6 @@ let to_string typ =
   F.asprintf "%t" pp
 
 
-type type_subst_t = (string * t) list [@@deriving compare]
-
-let is_type_subst_empty = List.is_empty
-
-(** Given the template type mapping and the type, substitute tvars within the type. *)
-let rec sub_type subst generic_typ : t =
-  match generic_typ.desc with
-  | TVar tname -> (
-    match List.Assoc.find subst ~equal:String.equal tname with
-    | Some t ->
-        (* Type qualifiers may come from original type or be part of substitution. Merge them *)
-        mk ~quals:(merge_quals t.quals generic_typ.quals) t.desc
-    | None ->
-        generic_typ )
-  | Tarray {elt= typ; length; stride} ->
-      let typ' = sub_type subst typ in
-      if phys_equal typ typ' then generic_typ
-      else mk_array ~default:generic_typ typ' ?length ?stride
-  | Tptr (typ, arg) ->
-      let typ' = sub_type subst typ in
-      if phys_equal typ typ' then generic_typ else mk ~default:generic_typ (Tptr (typ', arg))
-  | Tstruct tname ->
-      let tname' = sub_tname subst tname in
-      if phys_equal tname tname' then generic_typ else mk ~default:generic_typ (Tstruct tname')
-  | _ ->
-      generic_typ
-
-
-and sub_tname subst tname =
-  match tname with
-  | CppClass (name, Template {mangled; args}) ->
-      let sub_typ_opt typ_opt =
-        match typ_opt with
-        | TType typ ->
-            let typ' = sub_type subst typ in
-            if phys_equal typ typ' then typ_opt else TType typ'
-        | TInt _ | TNull | TNullPtr | TOpaque ->
-            typ_opt
-      in
-      let args' = IList.map_changed ~equal:equal_template_arg ~f:sub_typ_opt args in
-      if phys_equal args args' then tname else CppClass (name, Template {mangled; args= args'})
-  | _ ->
-      tname
-
-
 module Name = struct
   type t = name [@@deriving compare]
 
@@ -1348,16 +1295,6 @@ module Fieldname = struct
 
   let pp f = function Java field_name | Clang {field_name} -> Format.pp_print_string f field_name
 
-  let class_name_replace fname ~f =
-    match fname with
-    | Clang {class_name; field_name} ->
-        let class_name' = f class_name in
-        if phys_equal class_name class_name' then fname
-        else Clang {class_name= class_name'; field_name}
-    | _ ->
-        fname
-
-
   let clang_get_qual_class = function
     | Clang {class_name} ->
         Some (Name.qual_name class_name)
diff --git a/infer/src/IR/Typ.mli b/infer/src/IR/Typ.mli
index 07fb23676..c2e608655 100644
--- a/infer/src/IR/Typ.mli
+++ b/infer/src/IR/Typ.mli
@@ -120,9 +120,6 @@ val void : t
 val void_star : t
 (** void* type *)
 
-(** Stores information about type substitution *)
-type type_subst_t [@@deriving compare]
-
 module Name : sig
   (** Named types. *)
   type t = name [@@deriving compare]
@@ -228,12 +225,6 @@ val equal_desc : desc -> desc -> bool
 
 val equal_quals : type_quals -> type_quals -> bool
 
-val sub_type : type_subst_t -> t -> t
-
-val sub_tname : type_subst_t -> Name.t -> Name.t
-
-val is_type_subst_empty : type_subst_t -> bool
-
 val pp_full : Pp.env -> F.formatter -> t -> unit
 (** Pretty print a type with all the details. *)
 
@@ -611,8 +602,6 @@ module Fieldname : sig
 
   val to_full_string : t -> string
 
-  val class_name_replace : t -> f:(Name.t -> Name.t) -> t
-
   val to_simplified_string : t -> string
   (** Convert a fieldname to a simplified string with at most one-level path. *)
 
diff --git a/infer/src/biabduction/Abs.ml b/infer/src/biabduction/Abs.ml
index 5808ccffe..34cd66902 100644
--- a/infer/src/biabduction/Abs.ml
+++ b/infer/src/biabduction/Abs.ml
@@ -20,8 +20,8 @@ type rule =
   ; r_sigma: Match.hpred_pat list
   ; (* sigma should be in a specific order *)
     r_new_sigma: Sil.hpred list
-  ; r_new_pi: Prop.normal Prop.t -> Prop.normal Prop.t -> Sil.exp_subst -> Sil.atom list
-  ; r_condition: Prop.normal Prop.t -> Sil.exp_subst -> bool }
+  ; r_new_pi: Prop.normal Prop.t -> Prop.normal Prop.t -> Sil.subst -> Sil.atom list
+  ; r_condition: Prop.normal Prop.t -> Sil.subst -> bool }
 
 let sigma_rewrite tenv p r : Prop.normal Prop.t option =
   match Match.prop_match_with_impl tenv p r.r_condition r.r_vars r.r_root r.r_sigma with
@@ -31,7 +31,7 @@ let sigma_rewrite tenv p r : Prop.normal Prop.t option =
       if not (r.r_condition p_leftover sub) then None
       else
         let res_pi = r.r_new_pi p p_leftover sub in
-        let res_sigma = Prop.sigma_sub (`Exp sub) r.r_new_sigma in
+        let res_sigma = Prop.sigma_sub sub r.r_new_sigma in
         let p_with_res_pi = List.fold ~f:(Prop.prop_atom_and tenv) ~init:p_leftover res_pi in
         let p_new = Prop.prop_sigma_star p_with_res_pi res_sigma in
         Some (Prop.normalize tenv p_new)
@@ -56,7 +56,7 @@ let create_fresh_primeds_ls para =
   (ids_tuple, exps_tuple)
 
 
-let create_condition_ls ids_private id_base p_leftover (inst : Sil.exp_subst) =
+let create_condition_ls ids_private id_base p_leftover (inst : Sil.subst) =
   let insts_of_private_ids, insts_of_public_ids, inst_of_base =
     let f id' = List.exists ~f:(fun id'' -> Ident.equal id' id'') ids_private in
     let inst_private, inst_public = Sil.sub_domain_partition f inst in
@@ -117,7 +117,7 @@ let mk_rule_ptspts_ls tenv impl_ok1 impl_ok2 (para : Sil.hpara) =
     (ids, para_body_hpats)
   in
   let lseg_res = Prop.mk_lseg tenv Sil.Lseg_NE para exp_base exp_end exps_shared in
-  let gen_pi_res _ _ (_ : Sil.exp_subst) = [] in
+  let gen_pi_res _ _ (_ : Sil.subst) = [] in
   let condition =
     let ids_private = id_next :: (ids_exist_fst @ ids_exist_snd) in
     create_condition_ls ids_private id_base
@@ -148,7 +148,7 @@ let mk_rule_ptsls_ls tenv k2 impl_ok1 impl_ok2 para =
     {Match.hpred= Prop.mk_lseg tenv k2 para exp_next exp_end exps_shared; Match.flag= impl_ok2}
   in
   let lseg_res = Prop.mk_lseg tenv Sil.Lseg_NE para exp_base exp_end exps_shared in
-  let gen_pi_res _ _ (_ : Sil.exp_subst) = [] in
+  let gen_pi_res _ _ (_ : Sil.subst) = [] in
   let condition =
     let ids_private = id_next :: ids_exist in
     create_condition_ls ids_private id_base
@@ -175,7 +175,7 @@ let mk_rule_lspts_ls tenv k1 impl_ok1 impl_ok2 para =
     (ids, para_body_pat)
   in
   let lseg_res = Prop.mk_lseg tenv Sil.Lseg_NE para exp_base exp_end exps_shared in
-  let gen_pi_res _ _ (_ : Sil.exp_subst) = [] in
+  let gen_pi_res _ _ (_ : Sil.subst) = [] in
   let condition =
     let ids_private = id_next :: ids_exist in
     create_condition_ls ids_private id_base
@@ -208,7 +208,7 @@ let mk_rule_lsls_ls tenv k1 k2 impl_ok1 impl_ok2 para =
   in
   let k_res = lseg_kind_add k1 k2 in
   let lseg_res = Prop.mk_lseg tenv k_res para exp_base exp_end exps_shared in
-  let gen_pi_res _ _ (_ : Sil.exp_subst) =
+  let gen_pi_res _ _ (_ : Sil.subst) =
     []
     (*
   let inst_base, inst_next, inst_end =
@@ -295,7 +295,7 @@ let mk_rule_ptspts_dll tenv impl_ok1 impl_ok2 para =
     (ids, para_body_hpats)
   in
   let dllseg_res = Prop.mk_dllseg tenv Sil.Lseg_NE para exp_iF exp_oB exp_oF exp_iF' exps_shared in
-  let gen_pi_res _ _ (_ : Sil.exp_subst) = [] in
+  let gen_pi_res _ _ (_ : Sil.subst) = [] in
   let condition =
     (* for the case of ptspts since iF'=iB therefore iF' cannot be private*)
     let ids_private = ids_exist_fst @ ids_exist_snd in
@@ -346,7 +346,7 @@ let mk_rule_ptsdll_dll tenv k2 impl_ok1 impl_ok2 para =
     ; Match.flag= impl_ok2 }
   in
   let dllseg_res = Prop.mk_dllseg tenv Sil.Lseg_NE para exp_iF exp_oB exp_oF exp_iB exps_shared in
-  let gen_pi_res _ _ (_ : Sil.exp_subst) = [] in
+  let gen_pi_res _ _ (_ : Sil.subst) = [] in
   let condition =
     let ids_private = id_iF' :: ids_exist in
     create_condition_dll ids_private id_iF
@@ -386,7 +386,7 @@ let mk_rule_dllpts_dll tenv k1 impl_ok1 impl_ok2 para =
     ; Match.flag= impl_ok1 }
   in
   let dllseg_res = Prop.mk_dllseg tenv Sil.Lseg_NE para exp_iF exp_oB exp_oF exp_iF' exps_shared in
-  let gen_pi_res _ _ (_ : Sil.exp_subst) = [] in
+  let gen_pi_res _ _ (_ : Sil.subst) = [] in
   let condition =
     let ids_private = id_oB' :: ids_exist in
     create_condition_dll ids_private id_iF
@@ -428,7 +428,7 @@ let mk_rule_dlldll_dll tenv k1 k2 impl_ok1 impl_ok2 para =
   in
   let k_res = lseg_kind_add k1 k2 in
   let lseg_res = Prop.mk_dllseg tenv k_res para exp_iF exp_oB exp_oF exp_iB exps_shared in
-  let gen_pi_res _ _ (_ : Sil.exp_subst) = [] in
+  let gen_pi_res _ _ (_ : Sil.subst) = [] in
   let condition =
     let ids_private = [id_iF'; id_oB'] in
     create_condition_dll ids_private id_iF
@@ -677,11 +677,11 @@ let set_current_rules rules = Global.current_rules := rules
 let reset_current_rules () = Global.current_rules := []
 
 let eqs_sub subst eqs =
-  List.map ~f:(fun (e1, e2) -> (Sil.exp_sub (`Exp subst) e1, Sil.exp_sub (`Exp subst) e2)) eqs
+  List.map ~f:(fun (e1, e2) -> (Sil.exp_sub subst e1, Sil.exp_sub subst e2)) eqs
 
 
 let eqs_solve ids_in eqs_in =
-  let rec solve (sub : Sil.exp_subst) (eqs : (Exp.t * Exp.t) list) : Sil.exp_subst option =
+  let rec solve (sub : Sil.subst) (eqs : (Exp.t * Exp.t) list) : Sil.subst option =
     let do_default id e eqs_rest =
       if not (List.exists ~f:(fun id' -> Ident.equal id id') ids_in) then None
       else
@@ -719,7 +719,7 @@ let eqs_solve ids_in eqs_in =
     let filter id = not (List.exists ~f:(fun id' -> Ident.equal id id') sub_dom) in
     List.filter ~f:filter ids_in
   in
-  match solve Sil.exp_sub_empty eqs_in with None -> None | Some sub -> Some (compute_ids sub, sub)
+  match solve Sil.sub_empty eqs_in with None -> None | Some sub -> Some (compute_ids sub, sub)
 
 
 let sigma_special_cases_eqs sigma =
@@ -757,7 +757,7 @@ let sigma_special_cases ids sigma : (Ident.t list * Sil.hpred list) list =
       | None ->
           acc
       | Some (ids_res, sub) ->
-          (ids_res, List.map ~f:(Sil.hpred_sub (`Exp sub)) sigma_cur) :: acc
+          (ids_res, List.map ~f:(Sil.hpred_sub sub) sigma_cur) :: acc
     in
     List.fold ~f ~init:[] special_cases_eqs
   in
@@ -891,7 +891,7 @@ let abstract_pure_part tenv p ~(from_abstract_footprint : bool) =
     List.rev new_pure
   in
   let new_pure = do_pure (Prop.get_pure p) in
-  let eprop' = Prop.set p ~pi:new_pure ~sub:Sil.exp_sub_empty in
+  let eprop' = Prop.set p ~pi:new_pure ~sub:Sil.sub_empty in
   let eprop'' =
     if !BiabductionConfig.footprint && not from_abstract_footprint then
       let new_pi_footprint = do_pure p.Prop.pi_fp in
@@ -1142,7 +1142,7 @@ let check_junk pname tenv prop =
     else remove_junk fp_part fav_root sigma'
   in
   let sigma_new =
-    let fav_sub = Sil.exp_subst_free_vars prop.Prop.sub |> Ident.set_of_sequence in
+    let fav_sub = Sil.subst_free_vars prop.Prop.sub |> Ident.set_of_sequence in
     let fav_sub_sigmafp =
       Prop.sigma_free_vars prop.Prop.sigma_fp |> Ident.set_of_sequence ~init:fav_sub
     in
diff --git a/infer/src/biabduction/Absarray.ml b/infer/src/biabduction/Absarray.ml
index ed86a30a2..f3c3fde5d 100644
--- a/infer/src/biabduction/Absarray.ml
+++ b/infer/src/biabduction/Absarray.ml
@@ -650,8 +650,7 @@ let remove_redundant_elements tenv prop =
   let occurs_at_most_once : Ident.t -> bool =
     let fav_curr =
       let ( @@@ ) = Sequence.append in
-      Sil.exp_subst_free_vars prop.Prop.sub
-      @@@ Prop.pi_free_vars prop.Prop.pi
+      Sil.subst_free_vars prop.Prop.sub @@@ Prop.pi_free_vars prop.Prop.pi
       @@@ Prop.sigma_free_vars prop.Prop.sigma
     in
     let fav_foot =
diff --git a/infer/src/biabduction/Attribute.ml b/infer/src/biabduction/Attribute.ml
index 0c29d1a0e..0f5e3a0ae 100644
--- a/infer/src/biabduction/Attribute.ml
+++ b/infer/src/biabduction/Attribute.ml
@@ -307,8 +307,7 @@ let deallocate_stack_vars tenv (p : 'a Prop.t) pvars =
   let pi = List.map ~f:(Sil.atom_replace_exp exp_replace) (p.pi @ pi1) in
   let p' =
     Prop.normalize tenv
-      (Prop.set p ~sub:Sil.exp_sub_empty
-         ~sigma:(Prop.sigma_replace_exp tenv exp_replace sigma_other))
+      (Prop.set p ~sub:Sil.sub_empty ~sigma:(Prop.sigma_replace_exp tenv exp_replace sigma_other))
   in
   let p'' =
     let res = ref p' in
diff --git a/infer/src/biabduction/Dom.ml b/infer/src/biabduction/Dom.ml
index afa571d4b..b829d861e 100644
--- a/infer/src/biabduction/Dom.ml
+++ b/infer/src/biabduction/Dom.ml
@@ -524,9 +524,9 @@ module Rename : sig
 
   val lookup_list_todo : side -> Exp.t list -> Exp.t list
 
-  val to_subst_proj : side -> unit Ident.HashQueue.t -> Sil.exp_subst
+  val to_subst_proj : side -> unit Ident.HashQueue.t -> Sil.subst
 
-  val to_subst_emb : side -> Sil.exp_subst
+  val to_subst_emb : side -> Sil.subst
   (*
   val get : Exp.t -> Exp.t -> Exp.t option
   val pp : printenv -> Format.formatter -> (Exp.t * Exp.t * Exp.t) list -> unit
@@ -652,7 +652,7 @@ end = struct
     in
     if find_duplicates sub_list_side_sorted then (
       L.d_strln "failure reason 11" ; raise Sil.JoinFail )
-    else Sil.exp_subst_of_list sub_list_side
+    else Sil.subst_of_list sub_list_side
 
 
   let to_subst_emb (side : side) =
@@ -679,7 +679,7 @@ end = struct
           false
     in
     if find_duplicates sub_list_sorted then ( L.d_strln "failure reason 12" ; raise Sil.JoinFail )
-    else Sil.exp_subst_of_list sub_list_sorted
+    else Sil.subst_of_list sub_list_sorted
 
 
   let get_others' f_lookup side e =
@@ -1376,7 +1376,7 @@ let sigma_renaming_check (lhs : side) (sigma : Prop.sigma) (sigma_new : Prop.sig
    * and check that the renaming of primed vars is injective *)
   let fav_sigma = Prop.sigma_free_vars sigma_new |> Ident.hashqueue_of_sequence in
   let sub = Rename.to_subst_proj lhs fav_sigma in
-  let sigma' = Prop.sigma_sub (`Exp sub) sigma_new in
+  let sigma' = Prop.sigma_sub sub sigma_new in
   equal_sigma sigma sigma'
 
 
@@ -1785,7 +1785,7 @@ let pi_partial_meet tenv (p : Prop.normal Prop.t) (ep1 : 'a Prop.t) (ep2 : 'b Pr
   let dom2 = Ident.idlist_to_idset (Sil.sub_domain sub2) in
   let handle_atom sub dom atom =
     if Sil.atom_free_vars atom |> Sequence.for_all ~f:(fun id -> Ident.Set.mem id dom) then
-      Sil.atom_sub (`Exp sub) atom
+      Sil.atom_sub sub atom
     else ( L.d_str "handle_atom failed on " ; Sil.d_atom atom ; L.d_ln () ; raise Sil.JoinFail )
   in
   let f1 p' atom = Prop.prop_atom_and tenv p' (handle_atom sub1 dom1 atom) in
@@ -1815,7 +1815,7 @@ let eprop_partial_meet tenv (ep1 : 'a Prop.t) (ep2 : 'b Prop.t) : 'c Prop.t =
     let sub2 = ep2.Prop.sub in
     let range1 = Sil.sub_range sub1 in
     let f e = Exp.free_vars e |> Sequence.for_all ~f:Ident.is_normal in
-    Sil.equal_exp_subst sub1 sub2 && List.for_all ~f range1
+    Sil.equal_subst sub1 sub2 && List.for_all ~f range1
   in
   if not (sub_check ()) then ( L.d_strln "sub_check() failed" ; raise Sil.JoinFail )
   else
diff --git a/infer/src/biabduction/Match.ml b/infer/src/biabduction/Match.ml
index f64f93093..8c4ee026c 100644
--- a/infer/src/biabduction/Match.ml
+++ b/infer/src/biabduction/Match.ml
@@ -21,9 +21,9 @@ type hpred_pat = {hpred: Sil.hpred; flag: bool}
 
 (** Checks e1 = e2[sub ++ sub'] for some sub' with dom(sub') subseteq vars.
     Returns (sub ++ sub', vars - dom(sub')). *)
-let rec exp_match e1 sub vars e2 : (Sil.exp_subst * Ident.t list) option =
+let rec exp_match e1 sub vars e2 : (Sil.subst * Ident.t list) option =
   let check_equal sub vars e1 e2 =
-    let e2_inst = Sil.exp_sub (`Exp sub) e2 in
+    let e2_inst = Sil.exp_sub sub e2 in
     if Exp.equal e1 e2_inst then Some (sub, vars) else None
   in
   match (e1, e2) with
@@ -97,7 +97,7 @@ let exp_list_match es1 sub vars es2 =
     dom(sub') subseteq vars. Returns (sub ++ sub', vars - dom(sub')).
     WARNING: This function does not consider the fact that the analyzer
     sometimes forgets fields of hpred. It can possibly cause a problem. *)
-let rec strexp_match sexp1 sub vars sexp2 : (Sil.exp_subst * Ident.t list) option =
+let rec strexp_match sexp1 sub vars sexp2 : (Sil.subst * Ident.t list) option =
   match (sexp1, sexp2) with
   | Sil.Eexp (exp1, _), Sil.Eexp (exp2, _) ->
       exp_match exp1 sub vars exp2
@@ -148,7 +148,7 @@ and isel_match isel1 sub vars isel2 =
   | [], _ | _, [] ->
       None
   | (idx1, se1') :: isel1', (idx2, se2') :: isel2' ->
-      let idx2 = Sil.exp_sub (`Exp sub) idx2 in
+      let idx2 = Sil.exp_sub sub idx2 in
       let sanity_check = not (List.exists ~f:(fun id -> Exp.ident_mem idx2 id) vars) in
       if not sanity_check then (
         let pe = Pp.text in
@@ -168,13 +168,13 @@ and isel_match isel1 sub vars isel2 =
 
 
 (* extends substitution sub by creating a new substitution for vars *)
-let sub_extend_with_ren (sub : Sil.exp_subst) vars =
+let sub_extend_with_ren (sub : Sil.subst) vars =
   let f id = (id, Exp.Var (Ident.create_fresh Ident.kprimed)) in
-  let renaming_for_vars = Sil.exp_subst_of_list (List.map ~f vars) in
+  let renaming_for_vars = Sil.subst_of_list (List.map ~f vars) in
   Sil.sub_join sub renaming_for_vars
 
 
-type sidecondition = Prop.normal Prop.t -> Sil.exp_subst -> bool
+type sidecondition = Prop.normal Prop.t -> Sil.subst -> bool
 
 let rec execute_with_backtracking = function
   | [] ->
@@ -186,7 +186,7 @@ let rec execute_with_backtracking = function
       match res_f with None -> execute_with_backtracking fs | Some _ -> res_f )
 
 
-let rec instantiate_to_emp p condition (sub : Sil.exp_subst) vars = function
+let rec instantiate_to_emp p condition (sub : Sil.subst) vars = function
   | [] ->
       if condition p sub then Some (sub, p) else None
   | hpat :: hpats -> (
@@ -201,7 +201,7 @@ let rec instantiate_to_emp p condition (sub : Sil.exp_subst) vars = function
             let fully_instantiated = not (List.exists ~f:(fun id -> Exp.ident_mem e1 id) vars) in
             if not fully_instantiated then None
             else
-              let e1' = Sil.exp_sub (`Exp sub) e1 in
+              let e1' = Sil.exp_sub sub e1 in
               match exp_match e1' sub vars e2 with
               | None ->
                   None
@@ -213,8 +213,8 @@ let rec instantiate_to_emp p condition (sub : Sil.exp_subst) vars = function
             in
             if not fully_instantiated then None
             else
-              let iF' = Sil.exp_sub (`Exp sub) iF in
-              let oB' = Sil.exp_sub (`Exp sub) oB in
+              let iF' = Sil.exp_sub sub iF in
+              let oB' = Sil.exp_sub sub oB in
               match exp_list_match [iF'; oB'] sub vars [oF; iB] with
               | None ->
                   None
@@ -333,7 +333,7 @@ let rec iter_match_with_impl tenv iter condition sub vars hpat hpats =
         in
         if not fully_instantiated_start2 then None
         else
-          let e_start2' = Sil.exp_sub (`Exp sub) e_start2 in
+          let e_start2' = Sil.exp_sub sub e_start2 in
           match (exp_match e_start2' sub vars e_end2, hpats) with
           | None, _ ->
               (*
@@ -402,8 +402,8 @@ let rec iter_match_with_impl tenv iter condition sub vars hpat hpats =
         in
         if not fully_instantiated_iFoB2 then None
         else
-          let iF2' = Sil.exp_sub (`Exp sub) iF2 in
-          let oB2' = Sil.exp_sub (`Exp sub) oB2 in
+          let iF2' = Sil.exp_sub sub iF2 in
+          let oB2' = Sil.exp_sub sub oB2 in
           match (exp_list_match [iF2'; oB2'] sub vars [oF2; iB2], hpats) with
           | None, _ ->
               None
@@ -419,7 +419,7 @@ let rec iter_match_with_impl tenv iter condition sub vars hpat hpats =
         let fully_instantiated_iF2 = not (List.exists ~f:(fun id -> Exp.ident_mem iF2 id) vars) in
         if not fully_instantiated_iF2 then None
         else
-          let iF2' = Sil.exp_sub (`Exp sub) iF2 in
+          let iF2' = Sil.exp_sub sub iF2 in
           match exp_match iF2' sub vars iB2 with
           | None ->
               None
@@ -495,23 +495,19 @@ and hpara_common_match_with_impl tenv impl_ok ids1 sigma1 eids2 ids2 sigma2 =
       let sub_eids = List.map ~f:(fun (id2, id1) -> (id2, Exp.Var id1)) ren_eids in
       (sub_eids, eids_fresh)
     in
-    let sub = Sil.exp_subst_of_list (sub_ids @ sub_eids) in
+    let sub = Sil.subst_of_list (sub_ids @ sub_eids) in
     match sigma2 with
     | [] ->
         if List.is_empty sigma1 then true else false
     | hpred2 :: sigma2 -> (
         let hpat2, hpats2 =
-          let hpred2_ren, sigma2_ren =
-            (Sil.hpred_sub (`Exp sub) hpred2, Prop.sigma_sub (`Exp sub) sigma2)
-          in
+          let hpred2_ren, sigma2_ren = (Sil.hpred_sub sub hpred2, Prop.sigma_sub sub sigma2) in
           let allow_impl hpred = {hpred; flag= impl_ok} in
           (allow_impl hpred2_ren, List.map ~f:allow_impl sigma2_ren)
         in
         let condition _ _ = true in
         let p1 = Prop.normalize tenv (Prop.from_sigma sigma1) in
-        match
-          prop_match_with_impl_sub tenv p1 condition Sil.exp_sub_empty eids_fresh hpat2 hpats2
-        with
+        match prop_match_with_impl_sub tenv p1 condition Sil.sub_empty eids_fresh hpat2 hpats2 with
         | None ->
             false
         | Some (_, p1') when Prop.prop_is_emp p1' ->
@@ -551,7 +547,7 @@ and hpara_dll_match_with_impl tenv impl_ok para1 para2 : bool =
     2) [p |- (hpat.hpred * hpats.hpred)[subst] * p_leftover].
     Using the flag [field], we can control the strength of |-. *)
 let prop_match_with_impl tenv p condition vars hpat hpats =
-  prop_match_with_impl_sub tenv p condition Sil.exp_sub_empty vars hpat hpats
+  prop_match_with_impl_sub tenv p condition Sil.sub_empty vars hpat hpats
 
 
 let sigma_remove_hpred eq sigma e =
diff --git a/infer/src/biabduction/Match.mli b/infer/src/biabduction/Match.mli
index 68a0a25c7..9e90e422c 100644
--- a/infer/src/biabduction/Match.mli
+++ b/infer/src/biabduction/Match.mli
@@ -25,7 +25,7 @@ val hpara_dll_match_with_impl : Tenv.t -> bool -> Sil.hpara_dll -> Sil.hpara_dll
     considered during pattern matching. *)
 type hpred_pat = {hpred: Sil.hpred; flag: bool}
 
-type sidecondition = Prop.normal Prop.t -> Sil.exp_subst -> bool
+type sidecondition = Prop.normal Prop.t -> Sil.subst -> bool
 
 val prop_match_with_impl :
      Tenv.t
@@ -34,7 +34,7 @@ val prop_match_with_impl :
   -> Ident.t list
   -> hpred_pat
   -> hpred_pat list
-  -> (Sil.exp_subst * Prop.normal Prop.t) option
+  -> (Sil.subst * Prop.normal Prop.t) option
 (** [prop_match_with_impl p condition vars hpat hpats]
     returns [(subst, p_leftover)] such that
     1) [dom(subst) = vars]
diff --git a/infer/src/biabduction/Prop.ml b/infer/src/biabduction/Prop.ml
index ab0b613cb..3c9f228bc 100644
--- a/infer/src/biabduction/Prop.ml
+++ b/infer/src/biabduction/Prop.ml
@@ -41,7 +41,7 @@ module Core : sig
   (** the kind 'a should range over [normal] and [exposed] *)
   type 'a t = private
     { sigma: sigma  (** spatial part *)
-    ; sub: Sil.exp_subst  (** substitution *)
+    ; sub: Sil.subst  (** substitution *)
     ; pi: pi  (** pure part *)
     ; sigma_fp: sigma  (** abduced spatial part *)
     ; pi_fp: pi  (** abduced pure part *) }
@@ -51,13 +51,7 @@ module Core : sig
   (** Proposition [true /\ emp]. *)
 
   val set :
-       ?sub:Sil.exp_subst
-    -> ?pi:pi
-    -> ?sigma:sigma
-    -> ?pi_fp:pi
-    -> ?sigma_fp:sigma
-    -> 'a t
-    -> exposed t
+    ?sub:Sil.subst -> ?pi:pi -> ?sigma:sigma -> ?pi_fp:pi -> ?sigma_fp:sigma -> 'a t -> exposed t
   (** Set individual fields of the prop. *)
 
   val unsafe_cast_to_normal : exposed t -> normal t
@@ -74,14 +68,14 @@ end = struct
       normalized. *)
   type 'a t =
     { sigma: sigma  (** spatial part *)
-    ; sub: Sil.exp_subst  (** substitution *)
+    ; sub: Sil.subst  (** substitution *)
     ; pi: pi  (** pure part *)
     ; sigma_fp: sigma  (** abduced spatial part *)
     ; pi_fp: pi  (** abduced pure part *) }
   [@@deriving compare]
 
   (** Proposition [true /\ emp]. *)
-  let prop_emp : normal t = {sub= Sil.exp_sub_empty; pi= []; sigma= []; pi_fp= []; sigma_fp= []}
+  let prop_emp : normal t = {sub= Sil.sub_empty; pi= []; sigma= []; pi_fp= []; sigma_fp= []}
 
   let set ?sub ?pi ?sigma ?pi_fp ?sigma_fp p =
     let set_ p ?(sub = p.sub) ?(pi = p.pi) ?(sigma = p.sigma) ?(pi_fp = p.pi_fp)
@@ -134,12 +128,9 @@ let pp_hpred_stackvar pe0 f (hpred : Sil.hpred) =
 
 
 (** Pretty print a substitution. *)
-let pp_sub pe f = function
-  | `Exp sub ->
-      let pi_sub = List.map ~f:(fun (id, e) -> Sil.Aeq (Var id, e)) (Sil.sub_to_list sub) in
-      Pp.semicolon_seq ~print_env:{pe with break_lines= false} (Sil.pp_atom pe) f pi_sub
-  | `Typ _ ->
-      F.pp_print_string f "Printing typ_subst not implemented."
+let pp_sub pe f sub =
+  let pi_sub = List.map ~f:(fun (id, e) -> Sil.Aeq (Var id, e)) (Sil.sub_to_list sub) in
+  Pp.semicolon_seq ~print_env:{pe with break_lines= false} (Sil.pp_atom pe) f pi_sub
 
 
 (** Dump a substitution. *)
@@ -375,7 +366,7 @@ let gen_free_vars {sigma; sigma_fp; sub; pi; pi_fp} =
   >>= fun () ->
   sigma_gen_free_vars sigma_fp
   >>= fun () ->
-  Sil.exp_subst_gen_free_vars sub
+  Sil.subst_gen_free_vars sub
   >>= fun () -> pi_gen_free_vars pi >>= fun () -> pi_gen_free_vars pi_fp
 
 
@@ -1288,7 +1279,7 @@ module Normalize = struct
 
 
   let normalize_and_strengthen_atom tenv (p : normal t) (a : Sil.atom) : Sil.atom =
-    let a' = atom_normalize tenv (`Exp p.sub) a in
+    let a' = atom_normalize tenv p.sub a in
     match a' with
     | Aeq (BinOp (Le, Var id, Const (Cint n)), Const (Cint i)) when IntLit.isone i ->
         let lower = Exp.int (n -- IntLit.one) in
@@ -1678,7 +1669,7 @@ module Normalize = struct
   let sub_normalize sub =
     let f (id, e) = (not (Ident.is_primed id)) && not (Exp.ident_mem e id) in
     let sub' = Sil.sub_filter_pair ~f sub in
-    if Sil.equal_exp_subst sub sub' then sub else sub'
+    if Sil.equal_subst sub sub' then sub else sub'
 
 
   (** Conjoin a pure atomic predicate by normal conjunction. *)
@@ -1692,15 +1683,12 @@ module Normalize = struct
             p
         | Aeq (Var i, e) ->
             let sub_list = [(i, e)] in
-            let mysub = Sil.exp_subst_of_list sub_list in
+            let mysub = Sil.subst_of_list sub_list in
             let p_sub = Sil.sub_filter (fun i' -> not (Ident.equal i i')) p.sub in
-            let exp_sub' =
-              Sil.sub_join mysub (Sil.sub_range_map (Sil.exp_sub (`Exp mysub)) p_sub)
-            in
-            let sub' = `Exp exp_sub' in
+            let sub' = Sil.sub_join mysub (Sil.sub_range_map (Sil.exp_sub mysub) p_sub) in
             let nsub', npi', nsigma' =
               let nsigma' = sigma_normalize tenv sub' p.sigma in
-              (sub_normalize exp_sub', pi_normalize tenv sub' nsigma' p.pi, nsigma')
+              (sub_normalize sub', pi_normalize tenv sub' nsigma' p.pi, nsigma')
             in
             let eqs_zero, nsigma'' = sigma_remove_emptylseg nsigma' in
             let p' = unsafe_cast_to_normal (set p ~sub:nsub' ~pi:npi' ~sigma:nsigma'') in
@@ -1709,10 +1697,10 @@ module Normalize = struct
             p
         | Aneq (e1, e2) ->
             let sigma' = sigma_intro_nonemptylseg e1 e2 p.sigma in
-            let pi' = pi_normalize tenv (`Exp p.sub) sigma' (a' :: p.pi) in
+            let pi' = pi_normalize tenv p.sub sigma' (a' :: p.pi) in
             unsafe_cast_to_normal (set p ~pi:pi' ~sigma:sigma')
         | _ ->
-            let pi' = pi_normalize tenv (`Exp p.sub) p.sigma (a' :: p.pi) in
+            let pi' = pi_normalize tenv p.sub p.sigma (a' :: p.pi) in
             unsafe_cast_to_normal (set p ~pi:pi')
       in
       if not footprint then p'
@@ -1744,7 +1732,7 @@ end
 
 let exp_normalize_prop ?destructive tenv prop exp =
   BiabductionConfig.run_with_abs_val_equal_zero
-    (Normalize.exp_normalize ?destructive tenv (`Exp prop.sub))
+    (Normalize.exp_normalize ?destructive tenv prop.sub)
     exp
 
 
@@ -1762,15 +1750,11 @@ let lexp_normalize_prop tenv p lexp =
 
 
 let atom_normalize_prop tenv prop atom =
-  BiabductionConfig.run_with_abs_val_equal_zero
-    (Normalize.atom_normalize tenv (`Exp prop.sub))
-    atom
+  BiabductionConfig.run_with_abs_val_equal_zero (Normalize.atom_normalize tenv prop.sub) atom
 
 
 let sigma_normalize_prop tenv prop sigma =
-  BiabductionConfig.run_with_abs_val_equal_zero
-    (Normalize.sigma_normalize tenv (`Exp prop.sub))
-    sigma
+  BiabductionConfig.run_with_abs_val_equal_zero (Normalize.sigma_normalize tenv prop.sub) sigma
 
 
 let sigma_replace_exp tenv epairs sigma =
@@ -2004,15 +1988,14 @@ let compute_reindexing_from_indices list =
     (id, exp_new)
   in
   let reindexing = List.map ~f:transform list_passed in
-  Sil.exp_subst_of_list reindexing
+  Sil.subst_of_list reindexing
 
 
-let apply_reindexing tenv (exp_subst : Sil.exp_subst) prop =
-  let subst = `Exp exp_subst in
+let apply_reindexing tenv (subst : Sil.subst) prop =
   let nsigma = Normalize.sigma_normalize tenv subst prop.sigma in
   let npi = Normalize.pi_normalize tenv subst nsigma prop.pi in
   let nsub, atoms =
-    let dom_subst = List.map ~f:fst (Sil.sub_to_list exp_subst) in
+    let dom_subst = List.map ~f:fst (Sil.sub_to_list subst) in
     let in_dom_subst id = List.exists ~f:(Ident.equal id) dom_subst in
     let sub' = Sil.sub_filter (fun id -> not (in_dom_subst id)) prop.sub in
     let contains_substituted_id e = Exp.free_vars e |> Sequence.exists ~f:in_dom_subst in
@@ -2235,8 +2218,8 @@ let prop_sub subst (prop : 'a t) : exposed t =
 
 
 (** Apply renaming substitution to a proposition. *)
-let prop_ren_sub tenv (ren_sub : Sil.exp_subst) (prop : normal t) : normal t =
-  Normalize.normalize tenv (prop_sub (`Exp ren_sub) prop)
+let prop_ren_sub tenv (ren_sub : Sil.subst) (prop : normal t) : normal t =
+  Normalize.normalize tenv (prop_sub ren_sub prop)
 
 
 (** Existentially quantify the [ids] in [prop]. [ids] should not contain any primed variables. If
@@ -2247,7 +2230,7 @@ let exist_quantify tenv ?ids_queue ids (prop : normal t) : normal t =
   if List.is_empty ids then prop
   else
     let gen_fresh_id_sub id = (id, Exp.Var (Ident.create_fresh Ident.kprimed)) in
-    let ren_sub = Sil.exp_subst_of_list (List.map ~f:gen_fresh_id_sub ids) in
+    let ren_sub = Sil.subst_of_list (List.map ~f:gen_fresh_id_sub ids) in
     let prop' =
       (* throw away x=E if x becomes x_ *)
       let filter =
@@ -2259,7 +2242,7 @@ let exist_quantify tenv ?ids_queue ids (prop : normal t) : normal t =
             fun id -> not (List.mem ~equal:Ident.equal ids id)
       in
       let sub = Sil.sub_filter filter prop.sub in
-      if Sil.equal_exp_subst sub prop.sub then prop else unsafe_cast_to_normal (set prop ~sub)
+      if Sil.equal_subst sub prop.sub then prop else unsafe_cast_to_normal (set prop ~sub)
     in
     (*
     L.out "@[<2>.... Existential Quantification ....@\n";
@@ -2296,8 +2279,7 @@ let prop_primed_vars_to_normal_vars tenv (prop : normal t) : normal t =
     |> Ident.hashqueue_of_sequence |> Ident.HashQueue.keys
   in
   let ren_sub =
-    Sil.exp_subst_of_list
-      (List.map ~f:(fun i -> (i, Exp.Var (Ident.create_fresh Ident.knormal))) ids)
+    Sil.subst_of_list (List.map ~f:(fun i -> (i, Exp.Var (Ident.create_fresh Ident.knormal))) ids)
   in
   prop_ren_sub tenv ren_sub prop
 
@@ -2310,7 +2292,7 @@ let from_sigma sigma = set prop_emp ~sigma
 
 (** Iterator state over sigma. *)
 type 'a prop_iter =
-  { pit_sub: Sil.exp_subst  (** substitution for equalities *)
+  { pit_sub: Sil.subst  (** substitution for equalities *)
   ; pit_pi: pi  (** pure part *)
   ; pit_newpi: (bool * Sil.atom) list  (** newly added atoms. *)
   ; (* The first records !BiabductionConfig.footprint. *)
@@ -2362,7 +2344,7 @@ let prop_iter_add_atom footprint iter atom =
     associated to the resulting iterator *)
 let prop_iter_remove_curr_then_to_prop tenv iter : normal t =
   let sigma = List.rev_append iter.pit_old iter.pit_new in
-  let normalized_sigma = Normalize.sigma_normalize tenv (`Exp iter.pit_sub) sigma in
+  let normalized_sigma = Normalize.sigma_normalize tenv iter.pit_sub sigma in
   let prop =
     set prop_emp ~sub:iter.pit_sub ~pi:iter.pit_pi ~sigma:normalized_sigma ~pi_fp:iter.pit_pi_fp
       ~sigma_fp:iter.pit_sigma_fp
@@ -2372,7 +2354,7 @@ let prop_iter_remove_curr_then_to_prop tenv iter : normal t =
 
 (** Return the current hpred and state. *)
 let prop_iter_current tenv iter =
-  let curr = Normalize.hpred_normalize tenv (`Exp iter.pit_sub) iter.pit_curr in
+  let curr = Normalize.hpred_normalize tenv iter.pit_sub iter.pit_curr in
   let prop = unsafe_cast_to_normal (set prop_emp ~sigma:[curr]) in
   let prop' =
     List.fold
@@ -2457,7 +2439,7 @@ let prop_iter_make_id_primed tenv id iter =
     let pairs_unpid, pairs_pid = split [] [] eqs in
     match pairs_pid with
     | [] ->
-        let sub_unpid = Sil.exp_subst_of_list pairs_unpid in
+        let sub_unpid = Sil.subst_of_list pairs_unpid in
         let pairs = (id, Exp.Var pid) :: pairs_unpid in
         (sub_unpid, Sil.subst_of_list pairs, [])
     | (id1, e1) :: _ ->
@@ -2465,7 +2447,7 @@ let prop_iter_make_id_primed tenv id iter =
         let pairs_unpid' =
           List.map ~f:(fun (id', e') -> (id', Sil.exp_sub sub_id1 e')) pairs_unpid
         in
-        let sub_unpid = Sil.exp_subst_of_list pairs_unpid' in
+        let sub_unpid = Sil.subst_of_list pairs_unpid' in
         let pairs = (id, e1) :: pairs_unpid' in
         (sub_unpid, Sil.subst_of_list pairs, get_eqs [] pairs_pid)
   in
@@ -2490,7 +2472,7 @@ let prop_iter_footprint_free_vars iter =
 (** Find fav of the iterator *)
 let prop_iter_gen_free_vars ({pit_sub; pit_pi; pit_newpi; pit_old; pit_new; pit_curr} as iter) =
   let open Sequence.Generator in
-  Sil.exp_subst_gen_free_vars pit_sub
+  Sil.subst_gen_free_vars pit_sub
   >>= fun () ->
   pi_gen_free_vars pit_pi
   >>= fun () ->
diff --git a/infer/src/biabduction/Prop.mli b/infer/src/biabduction/Prop.mli
index 712b2415b..05dba8270 100644
--- a/infer/src/biabduction/Prop.mli
+++ b/infer/src/biabduction/Prop.mli
@@ -30,7 +30,7 @@ type sigma = Sil.hpred list
 (** the kind 'a should range over [normal] and [exposed] *)
 type 'a t = private
   { sigma: sigma  (** spatial part *)
-  ; sub: Sil.exp_subst  (** substitution *)
+  ; sub: Sil.subst  (** substitution *)
   ; pi: pi  (** pure part *)
   ; sigma_fp: sigma  (** abduced spatial part *)
   ; pi_fp: pi  (** abduced pure part *) }
@@ -260,7 +260,7 @@ val from_sigma : sigma -> exposed t
 (** Build an exposed prop from sigma *)
 
 val set :
-  ?sub:Sil.exp_subst -> ?pi:pi -> ?sigma:sigma -> ?pi_fp:pi -> ?sigma_fp:sigma -> 'a t -> exposed t
+  ?sub:Sil.subst -> ?pi:pi -> ?sigma:sigma -> ?pi_fp:pi -> ?sigma_fp:sigma -> 'a t -> exposed t
 (** Set individual fields of the prop. *)
 
 (** {2 Prop iterators} *)
diff --git a/infer/src/biabduction/Prover.ml b/infer/src/biabduction/Prover.ml
index 73b56a93b..ef7df575c 100644
--- a/infer/src/biabduction/Prover.ml
+++ b/infer/src/biabduction/Prover.ml
@@ -1060,7 +1060,7 @@ let check_inconsistency_pi tenv pi =
 
 (** {2 Abduction prover} *)
 
-type subst2 = Sil.exp_subst * Sil.exp_subst
+type subst2 = Sil.subst * Sil.subst
 
 type exc_body =
   | EXC_FALSE
@@ -1310,25 +1310,22 @@ end = struct
     L.d_ln ()
 end
 
-let d_impl (s1, s2) = ProverState.d_implication (`Exp s1, `Exp s2)
-
-let d_impl_err (arg1, (s1, s2), arg3) =
-  ProverState.d_implication_error (arg1, (`Exp s1, `Exp s2), arg3)
+let d_impl (s1, s2) = ProverState.d_implication (s1, s2)
 
+let d_impl_err (arg1, (s1, s2), arg3) = ProverState.d_implication_error (arg1, (s1, s2), arg3)
 
 (** extend a substitution *)
 let extend_sub sub v e =
-  let new_exp_sub = Sil.exp_subst_of_list [(v, e)] in
-  let new_sub = `Exp new_exp_sub in
-  Sil.sub_join new_exp_sub (Sil.sub_range_map (Sil.exp_sub new_sub) sub)
+  let new_exp_sub = Sil.subst_of_list [(v, e)] in
+  Sil.sub_join new_exp_sub (Sil.sub_range_map (Sil.exp_sub new_exp_sub) sub)
 
 
 (** Extend [sub1] and [sub2] to witnesses that each instance of
     [e1[sub1]] is an instance of [e2[sub2]]. Raise IMPL_FALSE if not
     possible. *)
 let exp_imply tenv calc_missing (subs : subst2) e1_in e2_in : subst2 =
-  let e1 = Prop.exp_normalize_noabs tenv (`Exp (fst subs)) e1_in in
-  let e2 = Prop.exp_normalize_noabs tenv (`Exp (snd subs)) e2_in in
+  let e1 = Prop.exp_normalize_noabs tenv (fst subs) e1_in in
+  let e2 = Prop.exp_normalize_noabs tenv (snd subs) e2_in in
   let var_imply (subs : subst2) v1 v2 : subst2 =
     match (Ident.is_primed v1, Ident.is_primed v2) with
     | false, false ->
@@ -1340,7 +1337,7 @@ let exp_imply tenv calc_missing (subs : subst2) e1_in e2_in : subst2 =
     | true, false ->
         raise (IMPL_EXC ("exps", subs, EXC_FALSE_EXPS (e1, e2)))
     | false, true ->
-        let sub2' = extend_sub (snd subs) v2 (Sil.exp_sub (`Exp (fst subs)) (Exp.Var v1)) in
+        let sub2' = extend_sub (snd subs) v2 (Sil.exp_sub (fst subs) (Exp.Var v1)) in
         (fst subs, sub2')
     | true, true ->
         let v1' = Ident.create_fresh Ident.knormal in
@@ -1514,7 +1511,7 @@ let rec sexp_imply tenv source calc_index_frame calc_missing subs se1 se2 typ2 :
       in
       (subs', fld_frame_opt, fld_missing_opt)
   | Sil.Estruct _, Sil.Eexp (e2, _) -> (
-      let e2' = Sil.exp_sub (`Exp (snd subs)) e2 in
+      let e2' = Sil.exp_sub (snd subs) e2 in
       match e2' with
       | Exp.Var id2 when Ident.is_primed id2 ->
           let id2' = Ident.create_fresh Ident.knormal in
@@ -1624,8 +1621,8 @@ and array_imply tenv source calc_index_frame calc_missing subs esel1 esel2 typ2
   | _, [] ->
       (subs, esel1, [])
   | (e1, se1) :: esel1', (e2, se2) :: esel2' ->
-      let e1n = Prop.exp_normalize_noabs tenv (`Exp (fst subs)) e1 in
-      let e2n = Prop.exp_normalize_noabs tenv (`Exp (snd subs)) e2 in
+      let e1n = Prop.exp_normalize_noabs tenv (fst subs) e1 in
+      let e2n = Prop.exp_normalize_noabs tenv (snd subs) e2 in
       let n = Exp.compare e1n e2n in
       if n < 0 then array_imply tenv source calc_index_frame calc_missing subs esel1' esel2 typ2
       else if n > 0 then
@@ -1648,7 +1645,7 @@ and array_imply tenv source calc_index_frame calc_missing subs esel1 esel2 typ2
 and sexp_imply_nolhs tenv source calc_missing (subs : subst2) se2 typ2 =
   match se2 with
   | Sil.Eexp (e2_, _) -> (
-      let e2 = Sil.exp_sub (`Exp (snd subs)) e2_ in
+      let e2 = Sil.exp_sub (snd subs) e2_ in
       match e2 with
       | Exp.Var v2 when Ident.is_primed v2 ->
           let v2' = path_to_id source in
@@ -1694,7 +1691,7 @@ let filter_ne_lhs sub e0 = function
 
 
 let filter_hpred sub hpred2 hpred1 =
-  match (Sil.hpred_sub (`Exp sub) hpred1, hpred2) with
+  match (Sil.hpred_sub sub hpred1, hpred2) with
   | Sil.Hlseg (Sil.Lseg_NE, hpara1, e1, f1, el1), Sil.Hlseg (Sil.Lseg_PE, _, _, _, _) ->
       if Sil.equal_hpred (Sil.Hlseg (Sil.Lseg_PE, hpara1, e1, f1, el1)) hpred2 then Some false
       else None
@@ -1734,9 +1731,9 @@ let move_primed_lhs_from_front subs sigma =
   | [] ->
       sigma
   | hpred :: _ ->
-      if hpred_has_primed_lhs (`Exp (snd subs)) hpred then
+      if hpred_has_primed_lhs (snd subs) hpred then
         let sigma_primed, sigma_unprimed =
-          List.partition_tf ~f:(hpred_has_primed_lhs (`Exp (snd subs))) sigma
+          List.partition_tf ~f:(hpred_has_primed_lhs (snd subs)) sigma
         in
         match sigma_unprimed with
         | [] ->
@@ -2060,7 +2057,7 @@ let rec hpred_imply tenv calc_index_frame calc_missing subs prop1 sigma2 hpred2
     subst2 * Prop.normal Prop.t =
   match hpred2 with
   | Sil.Hpointsto (e2_, se2, texp2) -> (
-      let e2 = Sil.exp_sub (`Exp (snd subs)) e2_ in
+      let e2 = Sil.exp_sub (snd subs) e2_ in
       ( match e2 with
       | Exp.Lvar _ ->
           ()
@@ -2074,7 +2071,7 @@ let rec hpred_imply tenv calc_index_frame calc_missing subs prop1 sigma2 hpred2
       | None ->
           raise (IMPL_EXC ("lhs is empty", subs, EXC_FALSE))
       | Some iter1 -> (
-        match Prop.prop_iter_find iter1 (filter_ne_lhs (`Exp (fst subs)) e2) with
+        match Prop.prop_iter_find iter1 (filter_ne_lhs (fst subs) e2) with
         | None ->
             raise (IMPL_EXC ("lhs does not have e|->", subs, EXC_FALSE_HPRED hpred2))
         | Some iter1' -> (
@@ -2129,7 +2126,7 @@ let rec hpred_imply tenv calc_index_frame calc_missing subs prop1 sigma2 hpred2
               in
               L.d_decrease_indent 1 ; res
           | Sil.Hdllseg (Sil.Lseg_NE, para1, iF1, oB1, oF1, iB1, elist1), _
-            when Exp.equal (Sil.exp_sub (`Exp (fst subs)) iF1) e2 ->
+            when Exp.equal (Sil.exp_sub (fst subs) iF1) e2 ->
               (* Unroll dllseg forward *)
               let n' = Exp.Var (Ident.create_fresh Ident.kprimed) in
               let _, para_inst1 = Sil.hpara_dll_instantiate para1 iF1 oB1 n' elist1 in
@@ -2146,7 +2143,7 @@ let rec hpred_imply tenv calc_index_frame calc_missing subs prop1 sigma2 hpred2
               in
               L.d_decrease_indent 1 ; res
           | Sil.Hdllseg (Sil.Lseg_NE, para1, iF1, oB1, oF1, iB1, elist1), _
-            when Exp.equal (Sil.exp_sub (`Exp (fst subs)) iB1) e2 ->
+            when Exp.equal (Sil.exp_sub (fst subs) iB1) e2 ->
               (* Unroll dllseg backward *)
               let n' = Exp.Var (Ident.create_fresh Ident.kprimed) in
               let _, para_inst1 = Sil.hpara_dll_instantiate para1 iB1 n' oF1 elist1 in
@@ -2166,7 +2163,7 @@ let rec hpred_imply tenv calc_index_frame calc_missing subs prop1 sigma2 hpred2
               assert false ) ) )
   | Sil.Hlseg (k, para2, e2_, f2_, elist2_) -> (
       (* for now ignore implications between PE and NE *)
-      let e2, f2 = (Sil.exp_sub (`Exp (snd subs)) e2_, Sil.exp_sub (`Exp (snd subs)) f2_) in
+      let e2, f2 = (Sil.exp_sub (snd subs) e2_, Sil.exp_sub (snd subs) f2_) in
       ( match e2 with
       | Exp.Lvar _ ->
           ()
@@ -2183,11 +2180,10 @@ let rec hpred_imply tenv calc_index_frame calc_missing subs prop1 sigma2 hpred2
             raise (IMPL_EXC ("lhs is empty", subs, EXC_FALSE))
         | Some iter1 -> (
           match
-            Prop.prop_iter_find iter1
-              (filter_hpred (fst subs) (Sil.hpred_sub (`Exp (snd subs)) hpred2))
+            Prop.prop_iter_find iter1 (filter_hpred (fst subs) (Sil.hpred_sub (snd subs) hpred2))
           with
           | None ->
-              let elist2 = List.map ~f:(fun e -> Sil.exp_sub (`Exp (snd subs)) e) elist2_ in
+              let elist2 = List.map ~f:(fun e -> Sil.exp_sub (snd subs) e) elist2_ in
               let _, para_inst2 = Sil.hpara_instantiate para2 e2 f2 elist2 in
               L.d_increase_indent 1 ;
               let res =
@@ -2197,7 +2193,7 @@ let rec hpred_imply tenv calc_index_frame calc_missing subs prop1 sigma2 hpred2
               (* calc_missing is false as we're checking an instantiation of the original list *)
               L.d_decrease_indent 1 ; res
           | Some iter1' -> (
-              let elist2 = List.map ~f:(fun e -> Sil.exp_sub (`Exp (snd subs)) e) elist2_ in
+              let elist2 = List.map ~f:(fun e -> Sil.exp_sub (snd subs) e) elist2_ in
               (* force instantiation of existentials *)
               let subs' = exp_list_imply tenv calc_missing subs (f2 :: elist2) (f2 :: elist2) in
               let prop1' = Prop.prop_iter_remove_curr_then_to_prop tenv iter1' in
@@ -2234,8 +2230,8 @@ let rec hpred_imply tenv calc_index_frame calc_missing subs prop1 sigma2 hpred2
       raise (Exceptions.Abduction_case_not_implemented __POS__)
   | Sil.Hdllseg (_, para2, iF2, oB2, oF2, iB2, elist2) -> (
       (* for now ignore implications between PE and NE *)
-      let iF2, oF2 = (Sil.exp_sub (`Exp (snd subs)) iF2, Sil.exp_sub (`Exp (snd subs)) oF2) in
-      let iB2, oB2 = (Sil.exp_sub (`Exp (snd subs)) iB2, Sil.exp_sub (`Exp (snd subs)) oB2) in
+      let iF2, oF2 = (Sil.exp_sub (snd subs) iF2, Sil.exp_sub (snd subs) oF2) in
+      let iB2, oB2 = (Sil.exp_sub (snd subs) iB2, Sil.exp_sub (snd subs) oB2) in
       ( match oF2 with
       | Exp.Lvar _ ->
           ()
@@ -2259,11 +2255,10 @@ let rec hpred_imply tenv calc_index_frame calc_missing subs prop1 sigma2 hpred2
           raise (IMPL_EXC ("lhs is empty", subs, EXC_FALSE))
       | Some iter1 -> (
         match
-          Prop.prop_iter_find iter1
-            (filter_hpred (fst subs) (Sil.hpred_sub (`Exp (snd subs)) hpred2))
+          Prop.prop_iter_find iter1 (filter_hpred (fst subs) (Sil.hpred_sub (snd subs) hpred2))
         with
         | None ->
-            let elist2 = List.map ~f:(fun e -> Sil.exp_sub (`Exp (snd subs)) e) elist2 in
+            let elist2 = List.map ~f:(fun e -> Sil.exp_sub (snd subs) e) elist2 in
             let _, para_inst2 =
               if Exp.equal iF2 iB2 then Sil.hpara_dll_instantiate para2 iF2 oB2 oF2 elist2
               else assert false
@@ -2278,7 +2273,7 @@ let rec hpred_imply tenv calc_index_frame calc_missing subs prop1 sigma2 hpred2
             L.d_decrease_indent 1 ; res
         | Some iter1' ->
             (* Only consider implications between identical listsegs for now *)
-            let elist2 = List.map ~f:(fun e -> Sil.exp_sub (`Exp (snd subs)) e) elist2 in
+            let elist2 = List.map ~f:(fun e -> Sil.exp_sub (snd subs) e) elist2 in
             (* force instantiation of existentials *)
             let subs' =
               exp_list_imply tenv calc_missing subs
@@ -2298,7 +2293,7 @@ and sigma_imply tenv calc_index_frame calc_missing subs prop1 sigma2 : subst2 *
   let is_constant_string_class subs = function
     (* if the hpred represents a constant string, return the string *)
     | Sil.Hpointsto (e2_, _, _) -> (
-        let e2 = Sil.exp_sub (`Exp (snd subs)) e2_ in
+        let e2 = Sil.exp_sub (snd subs) e2_ in
         match e2 with
         | Exp.Const (Const.Cstr s) ->
             Some (s, true)
@@ -2432,7 +2427,7 @@ and sigma_imply tenv calc_index_frame calc_missing subs prop1 sigma2 : subst2 *
         | Sil.Hpointsto (e2_, se2, t) ->
             let changed, calc_index_frame', hpred2' =
               expand_hpred_pointer tenv calc_index_frame
-                (Sil.Hpointsto (Prop.exp_normalize_noabs tenv (`Exp (snd subs)) e2_, se2, t))
+                (Sil.Hpointsto (Prop.exp_normalize_noabs tenv (snd subs) e2_, se2, t))
             in
             if changed then
               sigma_imply tenv calc_index_frame' calc_missing subs prop1 (hpred2' :: sigma2')
@@ -2447,15 +2442,15 @@ and sigma_imply tenv calc_index_frame calc_missing subs prop1 sigma2 : subst2 *
 
 
 let prepare_prop_for_implication tenv (_, sub2) pi1 sigma1 =
-  let pi1' = Prop.pi_sub (`Exp sub2) (ProverState.get_missing_pi ()) @ pi1 in
-  let sigma1' = Prop.sigma_sub (`Exp sub2) (ProverState.get_missing_sigma ()) @ sigma1 in
+  let pi1' = Prop.pi_sub sub2 (ProverState.get_missing_pi ()) @ pi1 in
+  let sigma1' = Prop.sigma_sub sub2 (ProverState.get_missing_sigma ()) @ sigma1 in
   let ep = Prop.set Prop.prop_emp ~sub:sub2 ~sigma:sigma1' ~pi:pi1' in
   Prop.normalize tenv ep
 
 
 let imply_pi tenv calc_missing (sub1, sub2) prop pi2 =
   let do_atom a =
-    let a' = Sil.atom_sub (`Exp sub2) a in
+    let a' = Sil.atom_sub sub2 a in
     try
       if not (check_atom tenv prop a') then
         raise (IMPL_EXC ("rhs atom missing in lhs", (sub1, sub2), EXC_FALSE_ATOM a'))
@@ -2480,7 +2475,7 @@ let rec pre_check_pure_implication tenv calc_missing (subs : subst2) pi1 pi2 =
   | [] ->
       subs
   | (Sil.Aeq (e2_in, f2_in) as a) :: pi2' when not (Prop.atom_is_inequality a) -> (
-      let e2, f2 = (Sil.exp_sub (`Exp (snd subs)) e2_in, Sil.exp_sub (`Exp (snd subs)) f2_in) in
+      let e2, f2 = (Sil.exp_sub (snd subs) e2_in, Sil.exp_sub (snd subs) f2_in) in
       if Exp.equal e2 f2 then pre_check_pure_implication tenv calc_missing subs pi1 pi2'
       else
         match (e2, f2) with
@@ -2493,7 +2488,7 @@ let rec pre_check_pure_implication tenv calc_missing (subs : subst2) pi1 pi2 =
             let sub2' = extend_sub (snd subs) v2 e2 in
             pre_check_pure_implication tenv calc_missing (fst subs, sub2') pi1 pi2'
         | _ ->
-            let pi1' = Prop.pi_sub (`Exp (fst subs)) pi1 in
+            let pi1' = Prop.pi_sub (fst subs) pi1 in
             let prop_for_impl = prepare_prop_for_implication tenv subs pi1' [] in
             imply_atom tenv calc_missing subs prop_for_impl (Sil.Aeq (e2_in, f2_in)) ;
             pre_check_pure_implication tenv calc_missing subs pi1 pi2' )
@@ -2501,9 +2496,7 @@ let rec pre_check_pure_implication tenv calc_missing (subs : subst2) pi1 pi2 =
     when (not calc_missing) && match e with Var v -> not (Ident.is_primed v) | _ -> true ->
       raise
         (IMPL_EXC
-           ( "ineq e2=f2 in rhs with e2 not primed var"
-           , (Sil.exp_sub_empty, Sil.exp_sub_empty)
-           , EXC_FALSE ))
+           ("ineq e2=f2 in rhs with e2 not primed var", (Sil.sub_empty, Sil.sub_empty), EXC_FALSE))
   | (Sil.Aeq _ | Aneq _ | Apred _ | Anpred _) :: pi2' ->
       pre_check_pure_implication tenv calc_missing subs pi1 pi2'
 
@@ -2526,8 +2519,8 @@ let check_array_bounds tenv (sub1, sub2) prop =
   in
   let check_bound = function
     | ProverState.BClen_imply (len1_, len2_, _indices2) ->
-        let len1 = Sil.exp_sub (`Exp sub1) len1_ in
-        let len2 = Sil.exp_sub (`Exp sub2) len2_ in
+        let len1 = Sil.exp_sub sub1 len1_ in
+        let len2 = Sil.exp_sub sub2 len2_ in
         (* L.d_strln_color Orange "check_bound ";
            Sil.d_exp len1; L.d_str " "; Sil.d_exp len2; L.d_ln(); *)
         let indices_to_check =
@@ -2536,7 +2529,7 @@ let check_array_bounds tenv (sub1, sub2) prop =
         in
         List.iter ~f:(fail_if_le len1) indices_to_check
     | ProverState.BCfrom_pre atom_ ->
-        let atom_neg = atom_negate tenv (Sil.atom_sub (`Exp sub2) atom_) in
+        let atom_neg = atom_negate tenv (Sil.atom_sub sub2 atom_) in
         (* L.d_strln_color Orange "BCFrom_pre"; Sil.d_atom atom_neg; L.d_ln (); *)
         if check_atom tenv prop atom_neg then check_failed atom_neg
   in
@@ -2575,17 +2568,17 @@ let check_implication_base pname tenv check_frame_empty calc_missing prop1 prop2
     L.d_strln "returns" ;
     L.d_strln "sub1: " ;
     L.d_increase_indent 1 ;
-    Prop.d_sub (`Exp (fst subs)) ;
+    Prop.d_sub (fst subs) ;
     L.d_decrease_indent 1 ;
     L.d_ln () ;
     L.d_strln "sub2: " ;
     L.d_increase_indent 1 ;
-    Prop.d_sub (`Exp (snd subs)) ;
+    Prop.d_sub (snd subs) ;
     L.d_decrease_indent 1 ;
     L.d_ln () ;
     let (sub1, sub2), frame_prop = sigma_imply tenv false calc_missing subs prop1 sigma2 in
-    let pi1' = Prop.pi_sub (`Exp sub1) pi1 in
-    let sigma1' = Prop.sigma_sub (`Exp sub1) sigma1 in
+    let pi1' = Prop.pi_sub sub1 pi1 in
+    let sigma1' = Prop.sigma_sub sub1 sigma1 in
     L.d_ln () ;
     let prop_for_impl = prepare_prop_for_implication tenv (sub1, sub2) pi1' sigma1' in
     (* only deal with pi2 without bound checks *)
@@ -2616,8 +2609,8 @@ let check_implication_base pname tenv check_frame_empty calc_missing prop1 prop2
 type implication_result =
   | ImplOK of
       ( check list
-      * Sil.exp_subst
-      * Sil.exp_subst
+      * Sil.subst
+      * Sil.subst
       * Sil.hpred list
       * Sil.atom list
       * Sil.hpred list
diff --git a/infer/src/biabduction/Prover.mli b/infer/src/biabduction/Prover.mli
index 237b09250..219339f03 100644
--- a/infer/src/biabduction/Prover.mli
+++ b/infer/src/biabduction/Prover.mli
@@ -70,8 +70,8 @@ val d_typings : (Exp.t * Exp.t) list -> unit
 type implication_result =
   | ImplOK of
       ( check list
-      * Sil.exp_subst
-      * Sil.exp_subst
+      * Sil.subst
+      * Sil.subst
       * Sil.hpred list
       * Sil.atom list
       * Sil.hpred list
diff --git a/infer/src/biabduction/Tabulation.ml b/infer/src/biabduction/Tabulation.ml
index c65255777..c382dc36e 100644
--- a/infer/src/biabduction/Tabulation.ml
+++ b/infer/src/biabduction/Tabulation.ml
@@ -198,7 +198,7 @@ let process_splitting actual_pre sub1 sub2 frame missing_pi missing_sigma frame_
     let sub1_inverse_list =
       List.map ~f:(function id, Exp.Var id' -> (id', Exp.Var id) | _ -> assert false) sub1_list'
     in
-    Sil.exp_subst_of_list_duplicates sub1_inverse_list
+    Sil.subst_of_list_duplicates sub1_inverse_list
   in
   let fav_actual_pre =
     let fav_pre = Prop.free_vars actual_pre |> Ident.hashqueue_of_sequence in
@@ -211,19 +211,18 @@ let process_splitting actual_pre sub1 sub2 frame missing_pi missing_sigma frame_
   let fav_missing_primed =
     let filter id = Ident.is_primed id && not (Ident.HashQueue.mem fav_actual_pre id) in
     let fav =
-      Prop.sigma_sub (`Exp sub) missing_sigma
-      |> Prop.sigma_free_vars |> Sequence.filter ~f:filter |> Ident.hashqueue_of_sequence
+      Prop.sigma_sub sub missing_sigma |> Prop.sigma_free_vars |> Sequence.filter ~f:filter
+      |> Ident.hashqueue_of_sequence
     in
-    Prop.pi_sub (`Exp sub) missing_pi
-    |> Prop.pi_free_vars |> Sequence.filter ~f:filter
+    Prop.pi_sub sub missing_pi |> Prop.pi_free_vars |> Sequence.filter ~f:filter
     |> Ident.hashqueue_of_sequence ~init:fav
     |> Ident.HashQueue.keys
   in
   let fav_missing_fld =
-    Prop.sigma_sub (`Exp sub) missing_fld |> Prop.sigma_free_vars |> Ident.hashqueue_of_sequence
+    Prop.sigma_sub sub missing_fld |> Prop.sigma_free_vars |> Ident.hashqueue_of_sequence
   in
   let map_var_to_pre_var_or_fresh id =
-    match Sil.exp_sub (`Exp sub1_inverse) (Exp.Var id) with
+    match Sil.exp_sub sub1_inverse (Exp.Var id) with
     | Exp.Var id' ->
         if
           Ident.HashQueue.mem fav_actual_pre id' || Ident.is_path id'
@@ -1227,10 +1226,9 @@ let exe_spec exe_env tenv ret_id (n, nspecs) caller_pdesc callee_pname loc prop
               ; vr_incons_res= inconsistent_results }
       in
       List.iter ~f:log_check_exn checks ;
-      let subbed_pre = Prop.prop_sub (`Exp sub1) actual_pre in
+      let subbed_pre = Prop.prop_sub sub1 actual_pre in
       match
-        check_dereferences caller_pname tenv callee_pname subbed_pre (`Exp sub2) spec_pre
-          formal_params
+        check_dereferences caller_pname tenv callee_pname subbed_pre sub2 spec_pre formal_params
       with
       | Some (Deref_undef _, _) ->
           let split = do_split () in
diff --git a/infer/src/biabduction/interproc.ml b/infer/src/biabduction/interproc.ml
index 9e2e6527e..d97b462e4 100644
--- a/infer/src/biabduction/interproc.ml
+++ b/infer/src/biabduction/interproc.ml
@@ -294,7 +294,7 @@ let propagate_nodes_divergence tenv (proc_cfg : ProcCfg.Exceptional.t) (pset : P
     let prop_incons =
       let mk_incons prop =
         let p_abs = Abs.abstract pname tenv prop in
-        let p_zero = Prop.set p_abs ~sub:Sil.exp_sub_empty ~sigma:[] in
+        let p_zero = Prop.set p_abs ~sub:Sil.sub_empty ~sigma:[] in
         Prop.normalize tenv (Prop.set p_zero ~pi:[Sil.Aneq (Exp.zero, Exp.zero)])
       in
       Paths.PathSet.map mk_incons diverging_states
@@ -586,7 +586,7 @@ let extract_specs tenv pdesc pathset : Prop.normal BiabductionSummary.spec list
       |> Ident.HashQueue.keys
     in
     let sub_list = List.map ~f:(fun id -> (id, Exp.Var (Ident.create_fresh Ident.knormal))) fav in
-    Sil.exp_subst_of_list sub_list
+    Sil.subst_of_list sub_list
   in
   let pre_post_visited_list =
     let pplist = Paths.PathSet.elements pathset in
@@ -594,10 +594,10 @@ let extract_specs tenv pdesc pathset : Prop.normal BiabductionSummary.spec list
       let _, prop' = PropUtil.remove_locals_formals tenv pdesc prop in
       let prop'' = Abs.abstract pname tenv prop' in
       let pre, post = Prop.extract_spec prop'' in
-      let pre' = Prop.normalize tenv (Prop.prop_sub (`Exp sub) pre) in
+      let pre' = Prop.normalize tenv (Prop.prop_sub sub pre) in
       let post' =
         if Prover.check_inconsistency_base tenv prop then None
-        else Some (Prop.normalize tenv (Prop.prop_sub (`Exp sub) post), path)
+        else Some (Prop.normalize tenv (Prop.prop_sub sub post), path)
       in
       let visited =
         let vset = vset_add_path Procdesc.NodeSet.empty path in