diff --git a/infer/src/backend/prop.ml b/infer/src/backend/prop.ml index 8537dd37d..424269bb9 100644 --- a/infer/src/backend/prop.ml +++ b/infer/src/backend/prop.ml @@ -2528,17 +2528,6 @@ let prop_normal_vars_to_primed_vars p = Sil.fav_filter_ident fav Ident.is_normal; exist_quantify fav p -(** Rename all primed variables fresh *) -let prop_rename_primed_fresh (p : normal t) : normal t = - let ids_primed = - let fav = prop_fav p in - let ids = Sil.fav_to_list fav in - IList.filter Ident.is_primed ids in - let ren_sub = - let f i = (i, Sil.Var (Ident.create_fresh Ident.kprimed)) in - Sil.sub_of_list (IList.map f ids_primed) in - prop_ren_sub ren_sub p - (** convert the primed vars to normal vars. *) let prop_primed_vars_to_normal_vars (p : normal t) : normal t = let fav = prop_fav p in diff --git a/infer/src/backend/prop.mli b/infer/src/backend/prop.mli index e910f8872..575deb2fb 100644 --- a/infer/src/backend/prop.mli +++ b/infer/src/backend/prop.mli @@ -398,9 +398,6 @@ val prop_normal_vars_to_primed_vars : normal t -> normal t (** convert the primed vars to normal vars. *) val prop_primed_vars_to_normal_vars : normal t -> normal t -(** Rename all primed variables. *) -val prop_rename_primed_fresh : normal t -> normal t - (** Build an exposed prop from pi *) val from_pi : pi -> exposed t