diff --git a/CHANGELOG.md b/CHANGELOG.md
index dd01e92ce1ed70542c66b5c69612898888cf0333..231ee8fbd8fa52f5d2074d0ada18a79deb9c5956 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -27,6 +27,7 @@ API-breaking change is listed.
   Slight breaking change: `destruct_and` no longer handle `False`;
   `destruct_or` now handles `False` while `destruct_and` handles `True`,
   as the respective units of disjunction and conjunction.
+- Add tactic `set_unfold in H`.
 
 ## std++ 1.2.1 (released 2019-08-29)
 
diff --git a/theories/sets.v b/theories/sets.v
index c6bdf3e45cc645a2c1f00739d04e9cead9b7ea52..6841be618e326a5be7c5d50d2d4096770126ee42 100644
--- a/theories/sets.v
+++ b/theories/sets.v
@@ -304,7 +304,7 @@ Section set_unfold_list.
   Qed.
 End set_unfold_list.
 
-Ltac set_unfold :=
+Tactic Notation "set_unfold" :=
   let rec unfold_hyps :=
     try match goal with
     | H : ?P |- _ =>
@@ -317,6 +317,13 @@ Ltac set_unfold :=
     end in
   apply set_unfold_2; unfold_hyps; csimpl in *.
 
+Tactic Notation "set_unfold" "in" ident(H) :=
+  let P := type of H in
+  lazymatch type of P with
+  | Prop => apply set_unfold_1 in H
+  | _ => fail "hypothesis" H "is not a proposition"
+  end.
+
 (** Since [firstorder] already fails or loops on very small goals generated by
 [set_solver], we use the [naive_solver] tactic as a substitute. *)
 Tactic Notation "set_solver" "by" tactic3(tac) :=