diff --git a/infer/src/backend/abs.ml b/infer/src/backend/abs.ml
index 547e8efe5..a80d22194 100644
--- a/infer/src/backend/abs.ml
+++ b/infer/src/backend/abs.ml
@@ -1194,8 +1194,8 @@ let check_junk ?original_prop pname tenv prop =
   let sigma_new = remove_junk false fav_sub_sigmafp prop.Prop.sigma in
   let sigma_fp_new = remove_junk true (Sil.fav_new ()) prop.Prop.sigma_fp in
   if
-    Prop.sigma_equal prop.Prop.sigma sigma_new
-    && Prop.sigma_equal prop.Prop.sigma_fp sigma_fp_new
+    Prop.equal_sigma prop.Prop.sigma sigma_new
+    && Prop.equal_sigma prop.Prop.sigma_fp sigma_fp_new
   then prop
   else Prop.normalize tenv (Prop.set prop ~sigma:sigma_new ~sigma_fp:sigma_fp_new)
 
diff --git a/infer/src/backend/dom.ml b/infer/src/backend/dom.ml
index 7d7c39b18..a99f8d3ee 100644
--- a/infer/src/backend/dom.ml
+++ b/infer/src/backend/dom.ml
@@ -25,7 +25,7 @@ let can_rename id =
 
 (** {2 Utility functions for sigma} *)
 
-let sigma_equal sigma1 sigma2 =
+let equal_sigma sigma1 sigma2 =
   let rec f sigma1_rest sigma2_rest =
     match (sigma1_rest, sigma2_rest) with
     | [], [] -> ()
@@ -1314,7 +1314,7 @@ let sigma_renaming_check (lhs: side) (sigma: Prop.sigma) (sigma_new: Prop.sigma)
   let fav_sigma = Prop.sigma_fav sigma_new in
   let sub = Rename.to_subst_proj lhs fav_sigma in
   let sigma' = Prop.sigma_sub sub sigma_new in
-  sigma_equal sigma sigma'
+  equal_sigma sigma sigma'
 
 let sigma_renaming_check_lhs = sigma_renaming_check Lhs
 let sigma_renaming_check_rhs = sigma_renaming_check Rhs
diff --git a/infer/src/backend/interproc.ml b/infer/src/backend/interproc.ml
index e168e696f..d6398cabe 100644
--- a/infer/src/backend/interproc.ml
+++ b/infer/src/backend/interproc.ml
@@ -711,7 +711,7 @@ let collect_analysis_result tenv wl pdesc : Paths.PathSet.t =
 module Pmap = Map.Make
     (struct
       type t = Prop.normal Prop.t
-      let compare = Prop.prop_compare
+      let compare = Prop.compare_prop
     end)
 
 let vset_ref_add_path vset_ref path =
diff --git a/infer/src/backend/paths.ml b/infer/src/backend/paths.ml
index 0b902d341..e3c8819c0 100644
--- a/infer/src/backend/paths.ml
+++ b/infer/src/backend/paths.ml
@@ -524,7 +524,7 @@ end
 
 module PropMap = Map.Make (struct
     type t = Prop.normal Prop.t
-    let compare = Prop.prop_compare
+    let compare = Prop.compare_prop
   end)
 
 (* =============== START of the PathSet module ===============*)
diff --git a/infer/src/backend/prop.ml b/infer/src/backend/prop.ml
index 660ee8cc2..30f31e05f 100644
--- a/infer/src/backend/prop.ml
+++ b/infer/src/backend/prop.ml
@@ -30,8 +30,14 @@ type normal (** kind for normal props, i.e. normalized *)
 
 type exposed (** kind for exposed props *)
 
-type pi = Sil.atom list
-type sigma = Sil.hpred list
+type pi = Sil.atom list [@@deriving compare]
+type sigma = Sil.hpred list [@@deriving compare]
+
+let equal_pi pi1 pi2 =
+  compare_pi pi1 pi2 = 0
+
+let equal_sigma sigma1 sigma2 =
+  compare_sigma sigma1 sigma2 = 0
 
 
 module Core : sig
@@ -44,7 +50,7 @@ module Core : sig
       pi: pi;  (** pure part *)
       sigma_fp : sigma;  (** abduced spatial part *)
       pi_fp: pi;  (** abduced pure part *)
-    }
+    } [@@deriving compare]
 
   (** Proposition [true /\ emp]. *)
   val prop_emp : normal t
@@ -72,7 +78,7 @@ end = struct
       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 =
@@ -104,47 +110,13 @@ include Core
 
 (** {1 Functions for Comparison} *)
 
-(** Comparison between lists of equalities and disequalities. Lexicographical order. *)
-let rec pi_compare pi1 pi2 =
-  if pi1 == pi2 then 0
-  else match (pi1, pi2) with
-    | ([],[]) -> 0
-    | ([], _:: _) -> - 1
-    | (_:: _,[]) -> 1
-    | (a1:: pi1', a2:: pi2') ->
-        let n = Sil.compare_atom a1 a2 in
-        if n <> 0 then n
-        else pi_compare pi1' pi2'
-
-let pi_equal pi1 pi2 =
-  pi_compare pi1 pi2 = 0
-
-(** Comparsion between lists of heap predicates. Lexicographical order. *)
-let rec sigma_compare sigma1 sigma2 =
-  if sigma1 == sigma2 then 0
-  else match (sigma1, sigma2) with
-    | ([],[]) -> 0
-    | ([], _:: _) -> - 1
-    | (_:: _,[]) -> 1
-    | (h1:: sigma1', h2:: sigma2') ->
-        let n = Sil.compare_hpred h1 h2 in
-        if n <> 0 then n
-        else sigma_compare sigma1' sigma2'
-
-let sigma_equal sigma1 sigma2 =
-  sigma_compare sigma1 sigma2 = 0
-
 (** Comparison between propositions. Lexicographical order. *)
-let prop_compare p1 p2 =
-  sigma_compare p1.sigma p2.sigma
-  |> next Sil.compare_subst p1.sub p2.sub
-  |> next pi_compare p1.pi p2.pi
-  |> next sigma_compare p1.sigma_fp p2.sigma_fp
-  |> next pi_compare p1.pi_fp p2.pi_fp
+let compare_prop p1 p2 =
+  compare (fun _ _ -> 0) p1 p2
 
 (** Check the equality of two propositions *)
-let prop_equal p1 p2 =
-  prop_compare p1 p2 = 0
+let equal_prop p1 p2 =
+  compare_prop p1 p2 = 0
 
 (** {1 Functions for Pretty Printing} *)
 
@@ -1445,7 +1417,7 @@ module Normalize = struct
   let sigma_normalize tenv sub sigma =
     let sigma' =
       IList.stable_sort Sil.compare_hpred (IList.map (hpred_normalize tenv sub) sigma) in
-    if sigma_equal sigma sigma' then sigma else sigma'
+    if equal_sigma sigma sigma' then sigma else sigma'
 
   let pi_tighten_ineq tenv pi =
     let ineq_list, nonineq_list = IList.partition atom_is_inequality pi in
@@ -1543,7 +1515,7 @@ module Normalize = struct
         Sil.compare_atom
         ((IList.filter filter_useful_atom nonineq_list) @ ineq_list) in
     let pi'' = pi_sorted_remove_redundant pi' in
-    if pi_equal pi0 pi'' then pi0 else pi''
+    if equal_pi pi0 pi'' then pi0 else pi''
 
   (** normalize the footprint part, and rename any primed vars
       in the footprint with fresh footprint vars *)
diff --git a/infer/src/backend/prop.mli b/infer/src/backend/prop.mli
index f7a8970ee..33ada7b9f 100644
--- a/infer/src/backend/prop.mli
+++ b/infer/src/backend/prop.mli
@@ -44,13 +44,13 @@ type struct_init_mode =
 (** {2 Basic Functions for propositions} *)
 
 (** Compare propositions *)
-val prop_compare : 'a t -> 'a t -> int
+val compare_prop : 'a t -> 'a t -> int
 
 (** Check the equality of two sigma's *)
-val sigma_equal : sigma -> sigma -> bool
+val equal_sigma : sigma -> sigma -> bool
 
 (** Check the equality of two propositions *)
-val prop_equal : 'a t -> 'a t -> bool
+val equal_prop : 'a t -> 'a t -> bool
 
 (** Pretty print a substitution. *)
 val pp_sub : printenv -> Format.formatter -> subst -> unit
diff --git a/infer/src/backend/propset.ml b/infer/src/backend/propset.ml
index 6eaedb3d7..18c2845bc 100644
--- a/infer/src/backend/propset.ml
+++ b/infer/src/backend/propset.ml
@@ -20,7 +20,7 @@ module F = Format
 module PropSet =
   Set.Make(struct
     type t = Prop.normal Prop.t
-    let compare = Prop.prop_compare
+    let compare = Prop.compare_prop
   end)
 
 let compare = PropSet.compare
diff --git a/infer/src/backend/specs.ml b/infer/src/backend/specs.ml
index f5c4278a8..ddfb843c2 100644
--- a/infer/src/backend/specs.ml
+++ b/infer/src/backend/specs.ml
@@ -83,11 +83,11 @@ module Jprop = struct
   (** Comparison for joined_prop *)
   let rec compare jp1 jp2 = match jp1, jp2 with
     | Prop (_, p1), Prop (_, p2) ->
-        Prop.prop_compare p1 p2
+        Prop.compare_prop p1 p2
     | Prop _, _ -> - 1
     | _, Prop _ -> 1
     | Joined (_, p1, jp1, jq1), Joined (_, p2, jp2, jq2) ->
-        let n = Prop.prop_compare p1 p2 in
+        let n = Prop.compare_prop p1 p2 in
         if n <> 0 then n
         else
           let n = compare jp1 jp2 in
@@ -827,6 +827,6 @@ let rec post_equal pl1 pl2 = match pl1, pl2 with
   | [], _:: _ -> false
   | _:: _,[] -> false
   | p1:: pl1', p2:: pl2' ->
-      if Prop.prop_equal p1 p2 then post_equal pl1' pl2'
+      if Prop.equal_prop p1 p2 then post_equal pl1' pl2'
       else false
 *)