diff --git a/README b/README
index 7986c94..6e53622 100644
--- a/README
+++ b/README
@@ -9,7 +9,7 @@ This version is known to compile with:
  - OCaml-Num 1.4.2
  - OCamlbuild 0.14.0
  - GNU C preprocessor 8.3.0
- - stdpp 1.6.0
+ - stdpp 1.7.0
 
 BUILDING INSTRUCTIONS
 ---------------------
diff --git a/memory/memory_map.v b/memory/memory_map.v
index b2d42dc..e35d422 100644
--- a/memory/memory_map.v
+++ b/memory/memory_map.v
@@ -266,7 +266,7 @@ Proof.
   destruct (m !!{Γ} (_, addr_ref _ _)) as [w'|] eqn:?; simplify_equality'.
   erewrite cmap_lookup_ref_le
     by eauto using cmap_lookup_ref_le, ref_freeze_le_r; simpl.
-  by rewrite (decide_iff _ _ _ _ (addr_is_obj_freeze _ _)).
+  by rewrite (decide_ext _ _ _ _ (addr_is_obj_freeze _ _)).
 Qed.
 Lemma cmap_lookup_ref_Some Γ Δ m o r w :
   ✓ Γ → ✓{Γ,Δ} m → m !!{Γ} (o,r) = Some w →
diff --git a/memory/pointer_bits.v b/memory/pointer_bits.v
index e6d7f0f..616643a 100644
--- a/memory/pointer_bits.v
+++ b/memory/pointer_bits.v
@@ -40,7 +40,7 @@ Proof.
   | inleft (τ↾Hτ) => cast_if_and (decide (frozen (frag_item pb)))
      (decide (frag_index pb < bit_size_of (ΓΔ.1) (τ.*)))
   | inright Hτ => right _
-  end; unfold frozen; auto with typeclass_instances;
+  end;
   destruct ΓΔ; first
   [ simplify_type_equality; econstructor; eauto
   | by destruct 1 as (?&?&?&?); simplify_type_equality ].
diff --git a/memory/references.v b/memory/references.v
index 6deae74..20976da 100644
--- a/memory/references.v
+++ b/memory/references.v
@@ -68,8 +68,11 @@ Inductive ref_typed' `{Env K} (Γ : env K) :
 
 Class Freeze A := freeze: bool → A → A.
 Arguments freeze {_ _} _ !_ /.
+
 Definition frozen `{Freeze A} (x : A) := freeze true x = x.
-Arguments freeze {_ _} _ !_ /.
+#[global] Typeclasses Opaque frozen.
+#[global] Instance frozen_dec `{EqDecision A, Freeze A} (x : A) :
+  Decision (frozen x) := decide (freeze true x = x).
 
 #[global] Instance ref_seg_freeze {K} : Freeze (ref_seg K) := λ β rs,
   match rs with
diff --git a/refinements/operations_refine.v b/refinements/operations_refine.v
index 3fa307a..7dccca8 100644
--- a/refinements/operations_refine.v
+++ b/refinements/operations_refine.v
@@ -39,7 +39,7 @@ Lemma addr_compare_refine Γ α f m1 m2 c a1 a2 a3 a4 σp :
   a1 ⊑{Γ,α,f@'{m1}↦'{m2}} a2 : σp → a3 ⊑{Γ,α,f@'{m1}↦'{m2}} a4 : σp →
   addr_compare Γ c a1 a3 = addr_compare Γ c a2 a4.
 Proof.
-  intros ? (_&_&Hstrict) Ha1 Ha2; unfold addr_compare; apply bool_decide_iff.
+  intros ? (_&_&Hstrict) Ha1 Ha2; unfold addr_compare; apply bool_decide_ext.
   assert ('{m1} ⊑{Γ,α,f} '{m2}) as HΔ by eauto using addr_refine_memenv_refine.
   destruct (addr_object_offset_refine Γ α f
     '{m1} '{m2} a1 a2 σp) as (r1&?&?&->); auto.