diff --git a/CHANGELOG.md b/CHANGELOG.md
index fd3422e9f49e13467fe25369e31abbb126d99c49..bb434f4b9353559789c80ccc24a69e0823dede18 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -3,6 +3,13 @@ way the logic is used on paper.  We also mention some significant changes in the
 Coq development, but not every API-breaking change is listed.  Changes marked
 `[#]` still need to be ported to the Iris Documentation LaTeX file(s).
 
+## Iris master
+
+**Changes in Coq:**
+
+* A new tactic `iStopProof` to turn the proof mode entailment into an ordinary
+  Coq goal `big star of context ⊢ proof mode goal`.
+
 ## Iris 3.2.0 (released 2019-08-29)
 
 The highlight of this release is the completely re-engineered interactive proof
diff --git a/ProofMode.md b/ProofMode.md
index 7c6be416c8cd9836cff6a40328788aec897c7148..990a7a44eaed48b72d2252c0cfcbe56134a1a67b 100644
--- a/ProofMode.md
+++ b/ProofMode.md
@@ -8,6 +8,18 @@ of the tactics can be applied when the connective to be introduced or to be elim
 appears under a later, an update modality, or in the conclusion of a
 weakest precondition.
 
+Starting and stopping the proof mode
+------------------------------------
+
+- `iStartProof PROP` : start the proof mode by turning a Coq goal into a proof
+  mode entailment. This tactic is performed implicitly by all proof mode tactics
+  described in this file, and thus should generally not be used by hand. The
+  optional argument `PROP` can be used to explicitly specify which BI logic
+  `PROP : bi` should be used. This is useful to drop down in a layered logic,
+  e.g. to drop down from `monPred PROP` to `PROP`.
+- `iStopProof` to turn the proof mode entailment into an ordinary Coq goal
+  `big star of context ⊢ proof mode goal`.
+
 Applying hypotheses and lemmas
 ------------------------------
 
diff --git a/theories/proofmode/coq_tactics.v b/theories/proofmode/coq_tactics.v
index fbfb2a7ce89453d12370a4e1a5366226ceaefe0a..72164546d98a8543aff55a8d13f9c82daa233844 100644
--- a/theories/proofmode/coq_tactics.v
+++ b/theories/proofmode/coq_tactics.v
@@ -12,14 +12,28 @@ Implicit Types Γ : env PROP.
 Implicit Types Δ : envs PROP.
 Implicit Types P Q : PROP.
 
-(** * Adequacy *)
-Lemma tac_adequate P : envs_entails (Envs Enil Enil 1) P → P.
+(** * Starting and stopping the proof mode *)
+Lemma tac_start P : envs_entails (Envs Enil Enil 1) P → bi_emp_valid P.
 Proof.
   rewrite envs_entails_eq !of_envs_eq /=.
   rewrite intuitionistically_True_emp left_id=><-.
   apply and_intro=> //. apply pure_intro; repeat constructor.
 Qed.
 
+Lemma tac_stop Δ P :
+  (match env_intuitionistic Δ, env_spatial Δ with
+   | Enil, Γs => env_to_prop Γs
+   | Γp, Enil => □ env_to_prop_and Γp
+   | Γp, Γs => □ env_to_prop_and Γp ∗ env_to_prop Γs
+   end%I ⊢ P) →
+  envs_entails Δ P.
+Proof.
+  rewrite envs_entails_eq !of_envs_eq. intros <-.
+  rewrite and_elim_r -env_to_prop_and_sound -env_to_prop_sound.
+  destruct (env_intuitionistic Δ), (env_spatial Δ);
+    by rewrite /= ?intuitionistically_True_emp ?left_id ?right_id.
+Qed.
+
 (** * Basic rules *)
 Lemma tac_eval Δ Q Q' :
   (∀ (Q'':=Q'), Q'' ⊢ Q) → (* We introduce [Q''] as a let binding so that
diff --git a/theories/proofmode/environments.v b/theories/proofmode/environments.v
index a0e04eb0e7bbbc9affe13f6f0b2f8e2600347d9c..f3e8e93f7fca2a6b4992f520f110a5f2ccfa78ed 100644
--- a/theories/proofmode/environments.v
+++ b/theories/proofmode/environments.v
@@ -364,11 +364,15 @@ Definition envs_split {PROP} (d : direction)
   ''(Δ1,Δ2) ← envs_split_go js Δ (envs_clear_spatial Δ);
   if d is Right then Some (Δ1,Δ2) else Some (Δ2,Δ1).
 
+Fixpoint env_to_prop_go {PROP : bi} (acc : PROP) (Γ : env PROP) : PROP :=
+  match Γ with Enil => acc | Esnoc Γ _ P => env_to_prop_go (P ∗ acc)%I Γ end.
 Definition env_to_prop {PROP : bi} (Γ : env PROP) : PROP :=
-  let fix aux Γ acc :=
-    match Γ with Enil => acc | Esnoc Γ _ P => aux Γ (P ∗ acc)%I end
-  in
-  match Γ with Enil => emp%I | Esnoc Γ _ P => aux Γ P end.
+  match Γ with Enil => emp%I | Esnoc Γ _ P => env_to_prop_go P Γ end.
+
+Fixpoint env_to_prop_and_go {PROP : bi} (acc : PROP) (Γ : env PROP) : PROP :=
+  match Γ with Enil => acc | Esnoc Γ _ P => env_to_prop_and_go (P ∧ acc)%I Γ end.
+Definition env_to_prop_and {PROP : bi} (Γ : env PROP) : PROP :=
+  match Γ with Enil => True%I | Esnoc Γ _ P => env_to_prop_and_go P Γ end.
 
 Section envs.
 Context {PROP : bi}.
@@ -767,7 +771,15 @@ Qed.
 
 Lemma env_to_prop_sound Γ : env_to_prop Γ ⊣⊢ [∗] Γ.
 Proof.
-  destruct Γ as [|Γ ? P]; simpl; first done.
+  destruct Γ as [|Γ i P]; simpl; first done.
+  revert P. induction Γ as [|Γ IH ? Q]=>P; simpl.
+  - by rewrite right_id.
+  - rewrite /= IH (comm _ Q _) assoc. done.
+Qed.
+
+Lemma env_to_prop_and_sound Γ : env_to_prop_and Γ ⊣⊢ [∧] Γ.
+Proof.
+  destruct Γ as [|Γ i P]; simpl; first done.
   revert P. induction Γ as [|Γ IH ? Q]=>P; simpl.
   - by rewrite right_id.
   - rewrite /= IH (comm _ Q _) assoc. done.
diff --git a/theories/proofmode/ltac_tactics.v b/theories/proofmode/ltac_tactics.v
index 72ceda801a7c6c34ddfe6998dea73fc04e38c6d9..b63077368563de53cf2796056b845bc73edaabe1 100644
--- a/theories/proofmode/ltac_tactics.v
+++ b/theories/proofmode/ltac_tactics.v
@@ -71,7 +71,7 @@ Tactic Notation "iStartProof" :=
   | |- envs_entails _ _ => idtac
   | |- ?φ => notypeclasses refine (as_emp_valid_2 φ _ _);
                [iSolveTC || fail "iStartProof: not a BI assertion"
-               |apply tac_adequate]
+               |apply tac_start]
   end.
 
 (* Same as above, with 2 differences :
@@ -92,7 +92,13 @@ Tactic Notation "iStartProof" uconstr(PROP) :=
      to find the corresponding bi. *)
   | |- ?φ => notypeclasses refine ((λ P : PROP, @as_emp_valid_2 φ _ P) _ _ _);
                [iSolveTC || fail "iStartProof: not a BI assertion"
-               |apply tac_adequate]
+               |apply tac_start]
+  end.
+
+Tactic Notation "iStopProof" :=
+  lazymatch goal with
+  | |- envs_entails _ _ => apply tac_stop; pm_reduce
+  | |- _ => fail "iStopProof: proofmode not started"
   end.
 
 (** * Generate a fresh identifier *)
diff --git a/theories/proofmode/reduction.v b/theories/proofmode/reduction.v
index c126c9bab334a46599d8f2aa03e29513990f0e84..ba3090367327c75f7473f4cf1c7c2a96522ea36c 100644
--- a/theories/proofmode/reduction.v
+++ b/theories/proofmode/reduction.v
@@ -13,7 +13,8 @@ Declare Reduction pm_eval := cbv [
   envs_lookup envs_lookup_delete envs_delete envs_snoc envs_app
   envs_simple_replace envs_replace envs_split
   envs_clear_spatial envs_clear_intuitionistic envs_incr_counter
-  envs_split_go envs_split env_to_prop
+  envs_split_go envs_split
+  env_to_prop_go env_to_prop env_to_prop_and_go env_to_prop_and
   (* PM option combinators *)
   pm_option_bind pm_from_option pm_option_fun
 ].