diff --git a/ProofMode.md b/ProofMode.md
index 9c14046768d3a805031cf133b9ffa8e077a9ef1d..82c0a5aedcd98aaa363182367bccf82a8425ad4c 100644
--- a/ProofMode.md
+++ b/ProofMode.md
@@ -92,6 +92,9 @@ Separating logic specific tactics
 
   Notice that framing spatial hypotheses makes them disappear, but framing Coq
   or persistent hypotheses does not make them disappear.
+
+  This tactic finishes the goal in case everything in the conclusion has been
+  framed.
 - `iCombine "H1" "H2" as "H"` : turns `H1 : P1` and `H2 : P2` into
   `H : P1 ★ P2`.
 
diff --git a/proofmode/tactics.v b/proofmode/tactics.v
index ca368e1aca2fd37fb7ff562acb2f40c7adeffb89..debb486052712763cc2570ae5b10cdd8f7abce53 100644
--- a/proofmode/tactics.v
+++ b/proofmode/tactics.v
@@ -432,17 +432,24 @@ Tactic Notation "iCombine" constr(H1) constr(H2) "as" constr(H) :=
     |env_cbv; reflexivity || fail "iCombine:" H "not fresh"|].
 
 (** Framing *)
+Local Ltac iFrameFinish :=
+  lazy iota beta;
+  try match goal with
+  | |- _ ⊢ True => exact (uPred.pure_intro _ _ I)
+  end.
+
 Local Ltac iFramePure t :=
   let φ := type of t in
   eapply (tac_frame_pure _ _ _ _ t);
-    [apply _ || fail "iFrame: cannot frame" φ|].
+    [apply _ || fail "iFrame: cannot frame" φ
+    |iFrameFinish].
 
 Local Ltac iFrameHyp H :=
   eapply tac_frame with _ H _ _ _;
     [env_cbv; reflexivity || fail "iFrame:" H "not found"
     |let R := match goal with |- Frame ?R _ _ => R end in
      apply _ || fail "iFrame: cannot frame" R
-    |lazy iota beta].
+    |iFrameFinish].
 
 Local Ltac iFrameAnyPure :=
   repeat match goal with H : _ |- _ => iFramePure H end.