diff --git a/CHANGELOG.md b/CHANGELOG.md
index 4619351d5e8ace979b1a82eea10d4f96c1945f9b..6cdea08d79f189fdcb5962578a19da5586ac4c04 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -3,6 +3,12 @@ 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:
+
+* Rename `timelessP` -> `timeless` (projection of the `Timeless` class)
+
 ## Iris 3.1.0 (released 2017-12-19)
 
 Changes in and extensions of the theory:
diff --git a/opam b/opam
index 57b4cf5da8384af3bd3db8e39b58f4fd1bfbb480..6dc8cdd4259828f14266e6ce70d224cac0d53842 100644
--- a/opam
+++ b/opam
@@ -11,5 +11,5 @@ install: [make "install"]
 remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/iris"]
 depends: [
   "coq" { >= "8.7.1" & < "8.8~" | (= "dev") }
-  "coq-stdpp" { (= "1.1.0") | (= "dev") }
+  "coq-stdpp" { (= "dev.2018-01-13.0") | (= "dev") }
 ]
diff --git a/theories/algebra/deprecated.v b/theories/algebra/deprecated.v
index ccb061003a11268da2e5b9a0a00005785188da77..2c8165cf10bff603132c3f7e054bee0c1129537d 100644
--- a/theories/algebra/deprecated.v
+++ b/theories/algebra/deprecated.v
@@ -14,7 +14,7 @@ Local Arguments op _ _ _ !_ /.
 Local Arguments pcore _ _ !_ /.
 
 (* This is isomorphic to option, but has a very different RA structure. *)
-Inductive dec_agree (A : Type) : Type := 
+Inductive dec_agree (A : Type) : Type :=
   | DecAgree : A → dec_agree A
   | DecAgreeBot : dec_agree A.
 Arguments DecAgree {_} _.
diff --git a/theories/algebra/dra.v b/theories/algebra/dra.v
index dc459baf45b763368a8be51d8773630aef0541e4..e2f3faf7d5ffed1391a1d267f1679d36dfd4b807 100644
--- a/theories/algebra/dra.v
+++ b/theories/algebra/dra.v
@@ -22,7 +22,7 @@ Record DraMixin A `{Equiv A, Core A, Disjoint A, Op A, Valid A} := {
   mixin_dra_core_disjoint_l x : ✓ x → core x ## x;
   mixin_dra_core_l x : ✓ x → core x ⋅ x ≡ x;
   mixin_dra_core_idemp x : ✓ x → core (core x) ≡ core x;
-  mixin_dra_core_mono x y : 
+  mixin_dra_core_mono x y :
     ∃ z, ✓ x → ✓ y → x ## y → core (x ⋅ y) ≡ core x ⋅ z ∧ ✓ z ∧ core x ## z
 }.
 Structure draT := DraT {
@@ -81,7 +81,7 @@ Section dra_mixin.
   Proof. apply (mixin_dra_core_l _ (dra_mixin A)). Qed.
   Lemma dra_core_idemp x : ✓ x → core (core x) ≡ core x.
   Proof. apply (mixin_dra_core_idemp _ (dra_mixin A)). Qed.
-  Lemma dra_core_mono x y : 
+  Lemma dra_core_mono x y :
     ∃ z, ✓ x → ✓ y → x ## y → core (x ⋅ y) ≡ core x ⋅ z ∧ ✓ z ∧ core x ## z.
   Proof. apply (mixin_dra_core_mono _ (dra_mixin A)). Qed.
 End dra_mixin.
@@ -209,7 +209,7 @@ Proof.
     assert (✓ y) by (rewrite EQ; by apply dra_op_valid).
     split; first done. exists (to_validity z). split; first split.
     + intros _. simpl. by split_and!.
-    + intros _. setoid_subst. by apply dra_op_valid. 
+    + intros _. setoid_subst. by apply dra_op_valid.
     + intros _. rewrite /= EQ //.
 Qed.
 *)
diff --git a/theories/algebra/functions.v b/theories/algebra/functions.v
index a0fd519b00d28b13f1a2587cd4b7c4acd91a7cdd..62c200d3a29649b1308a1423ad35d271e19057ca 100644
--- a/theories/algebra/functions.v
+++ b/theories/algebra/functions.v
@@ -8,7 +8,7 @@ Definition ofe_fun_insert `{EqDecision A} {B : A → ofeT}
   match decide (x = x') with left H => eq_rect _ B y _ H | right _ => f x' end.
 Instance: Params (@ofe_fun_insert) 5.
 
-Definition ofe_fun_singleton `{Finite A} {B : A → ucmraT} 
+Definition ofe_fun_singleton `{Finite A} {B : A → ucmraT}
   (x : A) (y : B x) : ofe_fun B := ofe_fun_insert x y ε.
 Instance: Params (@ofe_fun_singleton) 5.
 
diff --git a/theories/algebra/ofe.v b/theories/algebra/ofe.v
index 12ceaeb1d384a9a99976a025713675d318827631..48ec3e6a50fecf3653035b2c06df878561afe31a 100644
--- a/theories/algebra/ofe.v
+++ b/theories/algebra/ofe.v
@@ -7,7 +7,7 @@ Set Primitive Projections.
     category, and mathematically speaking, the entire development lives
     in this category. However, we will generally prefer to work with raw
     Coq functions plus some registered Proper instances for non-expansiveness.
-    This makes writing such functions much easier. It turns out that it many 
+    This makes writing such functions much easier. It turns out that it many
     cases, we do not even need non-expansiveness.
 *)
 
diff --git a/theories/algebra/sts.v b/theories/algebra/sts.v
index 66e4726e9c67e57f4b690e5930614bac087009c9..ceff0397934627149df817093562036da6ddebe0 100644
--- a/theories/algebra/sts.v
+++ b/theories/algebra/sts.v
@@ -311,7 +311,7 @@ Proof. done. Qed.
 Lemma sts_frag_up_valid s T : ✓ sts_frag_up s T ↔ tok s ## T.
 Proof.
   split.
-  - move=>/sts_frag_valid [H _]. apply H, elem_of_up. 
+  - move=>/sts_frag_valid [H _]. apply H, elem_of_up.
   - intros. apply sts_frag_valid; split. by apply closed_up. set_solver.
 Qed.
 
diff --git a/theories/base_logic/base_logic.v b/theories/base_logic/base_logic.v
index 61c01fb829b08f0b917c77fffc259eadc0faf008..61a43216a2d60abcb382fd26ebf4017bf41730f4 100644
--- a/theories/base_logic/base_logic.v
+++ b/theories/base_logic/base_logic.v
@@ -140,6 +140,9 @@ Proof. intros. by rewrite /ElimModal bupd_frame_r wand_elim_r bupd_plain. Qed.
 Global Instance elim_modal_bupd_plain P Q : Plain P → ElimModal (|==> P) P Q Q.
 Proof. intros. by rewrite /ElimModal bupd_plain wand_elim_r. Qed.
 
+Global Instance add_modal_bupd P Q : AddModal (|==> P) P (|==> Q).
+Proof. by rewrite /AddModal bupd_frame_r wand_elim_r bupd_trans. Qed.
+
 Global Instance is_except_0_bupd P : IsExcept0 P → IsExcept0 (|==> P).
 Proof.
   rewrite /IsExcept0=> HP.
diff --git a/theories/base_logic/double_negation.v b/theories/base_logic/double_negation.v
index 4799e0cc6a795f766f88931f63a3d9ff831ddbfd..b8981923b92d031b014c9d67e929315960edfdf4 100644
--- a/theories/base_logic/double_negation.v
+++ b/theories/base_logic/double_negation.v
@@ -229,7 +229,7 @@ Proof.
   revert P.
   induction k; intros P.
   - rewrite //= ?right_id. apply wand_intro_l.
-    rewrite {1}(nnupd_k_intro 0 (P -∗ False)%I) //= ?right_id. apply wand_elim_r. 
+    rewrite {1}(nnupd_k_intro 0 (P -∗ False)%I) //= ?right_id. apply wand_elim_r.
   - rewrite {2}(nnupd_k_unfold k P).
     apply and_intro.
     * rewrite (nnupd_k_unfold k P). rewrite and_elim_l.
@@ -292,9 +292,9 @@ Qed.
 End classical.
 
 (* We might wonder whether we can prove an adequacy lemma for nnupd. We could combine
-   the adequacy lemma for bupd with the previous result to get adquacy for nnupd, but 
+   the adequacy lemma for bupd with the previous result to get adquacy for nnupd, but
    this would rely on the classical axiom we needed to prove the equivalence! Can
-   we establish adequacy without axioms? Unfortunately not, because adequacy for 
+   we establish adequacy without axioms? Unfortunately not, because adequacy for
    nnupd would imply double negation elimination, which is classical: *)
 
 Lemma nnupd_dne φ: (|=n=> ⌜¬¬ φ → φ⌝: uPred M)%I.
@@ -327,7 +327,7 @@ Proof.
     intros Hf3. eapply Hf3; eauto.
     intros ??? Hx'. rewrite left_id in Hx' *=> Hx'.
     assert (n' < S k ∨ n' = S k) as [|] by omega.
-    * intros. move:(laterN_small n' (S k) x' False). rewrite //=. unseal. intros Hsmall. 
+    * intros. move:(laterN_small n' (S k) x' False). rewrite //=. unseal. intros Hsmall.
       eapply Hsmall; eauto.
     * subst. intros. exfalso. eapply Hf2. exists x'. split; eauto using cmra_validN_S.
   - intros k P x Hx. rewrite ?Nat_iter_S_r.
diff --git a/theories/base_logic/lib/fancy_updates.v b/theories/base_logic/lib/fancy_updates.v
index aacf160c5cfb2eb222f72709bae11e84718db7d6..7e9b763a987308a8578ed1a41fc475ae7e9e3e0e 100644
--- a/theories/base_logic/lib/fancy_updates.v
+++ b/theories/base_logic/lib/fancy_updates.v
@@ -204,17 +204,18 @@ Section proofmode_classes.
   Global Instance from_modal_fupd E P : FromModal (|={E}=> P) P.
   Proof. rewrite /FromModal. apply fupd_intro. Qed.
 
-  (* Put a lower priority compared to [elim_modal_fupd_fupd], so that
-     it is not taken when the first parameter is not specified (in
-     spec. patterns). *)
   Global Instance elim_modal_bupd_fupd E1 E2 P Q :
-    ElimModal (|==> P) P (|={E1,E2}=> Q) (|={E1,E2}=> Q) | 10.
+    ElimModal (|==> P) P (|={E1,E2}=> Q) (|={E1,E2}=> Q).
   Proof.
     by rewrite /ElimModal (bupd_fupd E1) fupd_frame_r wand_elim_r fupd_trans.
   Qed.
   Global Instance elim_modal_fupd_fupd E1 E2 E3 P Q :
     ElimModal (|={E1,E2}=> P) P (|={E1,E3}=> Q) (|={E2,E3}=> Q).
   Proof. by rewrite /ElimModal fupd_frame_r wand_elim_r fupd_trans. Qed.
+
+  Global Instance add_modal_fupd E1 E2 P Q :
+    AddModal (|={E1}=> P) P (|={E1,E2}=> Q).
+  Proof. by rewrite /AddModal fupd_frame_r wand_elim_r fupd_trans. Qed.
 End proofmode_classes.
 
 Hint Extern 2 (coq_tactics.envs_entails _ (|={_}=> _)) => iModIntro.
diff --git a/theories/base_logic/lib/namespaces.v b/theories/base_logic/lib/namespaces.v
index dc226f276d5a29ec5eaf26085ca33c4bda87d040..dfee3989ab332b4ead7a05ac10f912363991ba5a 100644
--- a/theories/base_logic/lib/namespaces.v
+++ b/theories/base_logic/lib/namespaces.v
@@ -84,7 +84,7 @@ End namespace.
 
 (* The hope is that registering these will suffice to solve most goals
 of the forms:
-- [N1 ## N2] 
+- [N1 ## N2]
 - [↑N1 ⊆ E ∖ ↑N2 ∖ .. ∖ ↑Nn]
 - [E1 ∖ ↑N1 ⊆ E2 ∖ ↑N2 ∖ .. ∖ ↑Nn] *)
 Create HintDb ndisj.
diff --git a/theories/base_logic/lib/sts.v b/theories/base_logic/lib/sts.v
index 00ddee6e6cea01022541fe0628533cbc0c0b3c0c..0d8e8ced6b615324537aded18038145a6d64606b 100644
--- a/theories/base_logic/lib/sts.v
+++ b/theories/base_logic/lib/sts.v
@@ -82,7 +82,7 @@ Section sts.
     sts_own γ s1 T ==∗ sts_own γ s2 T.
   Proof.
     intros ??. apply own_update, sts_update_frag_up; [|done..].
-    intros Hdisj. apply sts.closed_up. done. 
+    intros Hdisj. apply sts.closed_up. done.
   Qed.
 
   Lemma sts_own_weaken_tok γ s T1 T2 :
diff --git a/theories/bi/tactics.v b/theories/bi/tactics.v
index b755cce52f287c442bbb7f5f0914be9acf738b87..6c67948685f0fc614095f84ce2f3910b9e76df52 100644
--- a/theories/bi/tactics.v
+++ b/theories/bi/tactics.v
@@ -62,7 +62,7 @@ Module bi_reflection. Section bi_reflection.
     match e with
     | EEmp => None
     | EVar n' => if decide (n = n') then Some EEmp else None
-    | ESep e1 e2 => 
+    | ESep e1 e2 =>
        match cancel_go n e1 with
        | Some e1' => Some (ESep e1' e2)
        | None => ESep e1 <$> cancel_go n e2
diff --git a/theories/heap_lang/lang.v b/theories/heap_lang/lang.v
index 45f540eceb521c8268ac27054fa2720bbb402d86..39c6625fdc323eade1a7311b09c19a45056f1d16 100644
--- a/theories/heap_lang/lang.v
+++ b/theories/heap_lang/lang.v
@@ -276,7 +276,7 @@ Definition fill_item (Ki : ectx_item) (e : expr) : expr :=
   | CaseCtx e1 e2 => Case e e1 e2
   | AllocCtx => Alloc e
   | LoadCtx => Load e
-  | StoreLCtx e2 => Store e e2 
+  | StoreLCtx e2 => Store e e2
   | StoreRCtx v1 => Store (of_val v1) e
   | CasLCtx e1 e2 => CAS e e1 e2
   | CasMCtx v0 e2 => CAS (of_val v0) e e2
@@ -365,11 +365,11 @@ Inductive head_step : expr → state → expr → state → list (expr) → Prop
      head_step (App (Rec f x e1) e2) σ e' σ []
   | UnOpS op e v v' σ :
      to_val e = Some v →
-     un_op_eval op v = Some v' → 
+     un_op_eval op v = Some v' →
      head_step (UnOp op e) σ (of_val v') σ []
   | BinOpS op e1 e2 v1 v2 v' σ :
      to_val e1 = Some v1 → to_val e2 = Some v2 →
-     bin_op_eval op v1 v2 = Some v' → 
+     bin_op_eval op v1 v2 = Some v' →
      head_step (BinOp op e1 e2) σ (of_val v') σ []
   | IfTrueS e1 e2 σ :
      head_step (If (Lit $ LitBool true) e1 e2) σ e1 σ []
diff --git a/theories/heap_lang/lib/counter.v b/theories/heap_lang/lib/counter.v
index b9632c00c56c77d877d82dc6294721e44be25a74..8aee1924bb7256c1691f78a3bdf35e523f97017c 100644
--- a/theories/heap_lang/lib/counter.v
+++ b/theories/heap_lang/lib/counter.v
@@ -55,7 +55,7 @@ Section mono_proof.
     - iDestruct (own_valid_2 with "Hγ Hγf")
         as %[?%mnat_included _]%auth_valid_discrete_2.
       iMod (own_update_2 with "Hγ Hγf") as "[Hγ Hγf]".
-      { apply auth_update, (mnat_local_update _ _ (S c)); auto. } 
+      { apply auth_update, (mnat_local_update _ _ (S c)); auto. }
       wp_cas_suc. iMod ("Hclose" with "[Hl Hγ]") as "_".
       { iNext. iExists (S c). rewrite Nat2Z.inj_succ Z.add_1_l. by iFrame. }
       iModIntro. wp_if. iApply "HΦ"; iExists γ; repeat iSplit; eauto.
diff --git a/theories/heap_lang/lib/ticket_lock.v b/theories/heap_lang/lib/ticket_lock.v
index 7437f74833d1af6324e16db7e7080036bf757e16..b75704bb0439af170769225ce8d32eb03941a948 100644
--- a/theories/heap_lang/lib/ticket_lock.v
+++ b/theories/heap_lang/lib/ticket_lock.v
@@ -94,7 +94,7 @@ Section proof.
       + iMod ("Hclose" with "[Hlo Hln Hainv Ht]") as "_".
         { iNext. iExists o, n. iFrame. eauto. }
         iModIntro. wp_let. wp_op. case_bool_decide; [|done].
-        wp_if. 
+        wp_if.
         iApply ("HΦ" with "[-]"). rewrite /locked. iFrame. eauto.
       + iDestruct (own_valid_2 with "Ht Haown") as % [_ ?%gset_disj_valid_op].
         set_solver.
@@ -129,7 +129,7 @@ Section proof.
       iModIntro. wp_if.
       iApply (wait_loop_spec γ (#lo, #ln) with "[-HΦ]").
       + iFrame. rewrite /is_lock; eauto 10.
-      + by iNext. 
+      + by iNext.
     - wp_cas_fail.
       iMod ("Hclose" with "[Hlo' Hln' Hauth Haown]") as "_".
       { iNext. iExists o', n'. by iFrame. }
diff --git a/theories/heap_lang/proofmode.v b/theories/heap_lang/proofmode.v
index 643cfa12b6a4da9270afffdc1d231112a27c3013..980af2987690415d0dc0b5080e3b326d06475333 100644
--- a/theories/heap_lang/proofmode.v
+++ b/theories/heap_lang/proofmode.v
@@ -10,7 +10,7 @@ Lemma tac_wp_expr_eval `{heapG Σ} Δ s E Φ e e' :
   envs_entails Δ (WP e' @ s; E {{ Φ }}) → envs_entails Δ (WP e @ s; E {{ Φ }}).
 Proof. by intros ->. Qed.
 
-Ltac wp_expr_eval t :=
+Tactic Notation "wp_expr_eval" tactic(t) :=
   try iStartProof;
   try (eapply tac_wp_expr_eval; [t; reflexivity|]).
 
@@ -33,7 +33,10 @@ Lemma tac_wp_value `{heapG Σ} Δ s E Φ e v :
   envs_entails Δ (Φ v) → envs_entails Δ (WP e @ s; E {{ Φ }}).
 Proof. rewrite /envs_entails=> ? ->. by apply wp_value. Qed.
 
-Ltac wp_value_head := eapply tac_wp_value; [apply _|lazy beta].
+Ltac wp_value_head :=
+  eapply tac_wp_value;
+    [apply _
+    |iEval (lazy beta; simpl of_val)].
 
 Tactic Notation "wp_pure" open_constr(efoc) :=
   iStartProof;
diff --git a/theories/program_logic/weakestpre.v b/theories/program_logic/weakestpre.v
index bfeb71f1cd2b764547579c25558137cd0407e7a5..1243a60bc5d5a956adee8599e723c524412fa80f 100644
--- a/theories/program_logic/weakestpre.v
+++ b/theories/program_logic/weakestpre.v
@@ -236,7 +236,7 @@ Proof.
   iSplitL "He2"; first by iApply ("IH" with "He2"). iClear "Hred Hstep".
   induction efs as [|ef efs IH]; first by iApply big_sepL_nil.
   rewrite !big_sepL_cons. iDestruct "Hefs" as "(Hef & Hefs)".
-  iSplitL "Hef". by iApply ("IH" with "Hef"). exact: IH. 
+  iSplitL "Hef". by iApply ("IH" with "Hef"). exact: IH.
 Qed.
 
 Lemma fupd_wp s E e Φ : (|={E}=> WP e @ s; E {{ Φ }}) ⊢ WP e @ s; E {{ Φ }}.
@@ -392,10 +392,13 @@ Section proofmode_classes.
     ElimModal (|={E}=> P) P (WP e @ s; E {{ Φ }}) (WP e @ s; E {{ Φ }}).
   Proof. by rewrite /ElimModal fupd_frame_r wand_elim_r fupd_wp. Qed.
 
-  (* lower precedence, if possible, it should persistently pick elim_upd_fupd_wp *)
   Global Instance elim_modal_fupd_wp_atomic s E1 E2 e P Φ :
     Atomic (stuckness_to_atomicity s) e →
     ElimModal (|={E1,E2}=> P) P
-            (WP e @ s; E1 {{ Φ }}) (WP e @ s; E2 {{ v, |={E2,E1}=> Φ v }})%I | 100.
+            (WP e @ s; E1 {{ Φ }}) (WP e @ s; E2 {{ v, |={E2,E1}=> Φ v }})%I.
   Proof. intros. by rewrite /ElimModal fupd_frame_r wand_elim_r wp_atomic. Qed.
+
+  Global Instance add_modal_fupd_wp s E e P Φ :
+    AddModal (|={E}=> P) P (WP e @ s; E {{ Φ }}).
+  Proof. by rewrite /AddModal fupd_frame_r wand_elim_r fupd_wp. Qed.
 End proofmode_classes.
diff --git a/theories/proofmode/base.v b/theories/proofmode/base.v
index 9497be34506b4e7f20a132cc2a9f892aeefffdbb..159a09b5ae02e28cbbfdc268f2704109535a512a 100644
--- a/theories/proofmode/base.v
+++ b/theories/proofmode/base.v
@@ -27,7 +27,7 @@ Definition ascii_beq (x y : ascii) : bool :=
     beq x5 y5 && beq x6 y6 && beq x7 y7 && beq x8 y8.
 
 Fixpoint string_beq (s1 s2 : string) : bool :=
-  match s1, s2 with 
+  match s1, s2 with
   | "", "" => true
   | String a1 s1, String a2 s2 => ascii_beq a1 a2 && string_beq s1 s2
   | _, _ => false
diff --git a/theories/proofmode/class_instances.v b/theories/proofmode/class_instances.v
index d9e42bee2135f0eda69d694df9f6ed97db37fee6..f818a7b9cac012af05d4c4d021c890126853184c 100644
--- a/theories/proofmode/class_instances.v
+++ b/theories/proofmode/class_instances.v
@@ -706,7 +706,7 @@ Proof.
   rewrite /ElimModal=> H. apply wand_intro_r.
   by rewrite wand_curry -assoc (comm _ P') -wand_curry wand_elim_l.
 Qed.
-Global Instance forall_modal_wand {A} P P' (Φ Ψ : A → PROP) :
+Global Instance elim_modal_forall {A} P P' (Φ Ψ : A → PROP) :
   (∀ x, ElimModal P P' (Φ x) (Ψ x)) → ElimModal P P' (∀ x, Φ x) (∀ x, Ψ x).
 Proof.
   rewrite /ElimModal=> H. apply forall_intro=> a. by rewrite (forall_elim a).
@@ -716,6 +716,19 @@ Proof.
   rewrite /ElimModal=> H. by rewrite absorbingly_sep_l wand_elim_r absorbing_absorbingly.
 Qed.
 
+(* AddModal *)
+Global Instance add_modal_wand P P' Q R :
+  AddModal P P' Q → AddModal P P' (R -∗ Q).
+Proof.
+  rewrite /AddModal=> H. apply wand_intro_r.
+  by rewrite wand_curry -assoc (comm _ P') -wand_curry wand_elim_l.
+Qed.
+Global Instance add_modal_forall {A} P P' (Φ : A → PROP) :
+  (∀ x, AddModal P P' (Φ x)) → AddModal P P' (∀ x, Φ x).
+Proof.
+  rewrite /AddModal=> H. apply forall_intro=> a. by rewrite (forall_elim a).
+Qed.
+
 (* Frame *)
 Global Instance frame_here_absorbing p R : Absorbing R → Frame p R R True | 0.
 Proof. intros. by rewrite /Frame affinely_persistently_if_elim sep_elim_l. Qed.
diff --git a/theories/proofmode/classes.v b/theories/proofmode/classes.v
index f17d674d190749f904327ce0f03f322304555b3c..4692d73397779325ecad1d2a4a40bba89f081063 100644
--- a/theories/proofmode/classes.v
+++ b/theories/proofmode/classes.v
@@ -189,10 +189,17 @@ Class ElimModal {PROP : bi} (P P' : PROP) (Q Q' : PROP) :=
 Arguments ElimModal {_} _%I _%I _%I _%I : simpl never.
 Arguments elim_modal {_} _%I _%I _%I _%I {_}.
 Hint Mode ElimModal + ! - ! - : typeclass_instances.
-Hint Mode ElimModal + - ! - ! : typeclass_instances.
 
-Lemma elim_modal_dummy {PROP : bi} (P Q : PROP) : ElimModal P P Q Q.
-Proof. by rewrite /ElimModal wand_elim_r. Qed.
+(* Used by the specialization pattern [ > ] in [iSpecialize] and [iAssert] to
+add a modality to the goal corresponding to a premise/asserted proposition. *)
+Class AddModal {PROP : bi} (P P' : PROP) (Q : PROP) :=
+  add_modal : P ∗ (P' -∗ Q) ⊢ Q.
+Arguments AddModal {_} _%I _%I _%I : simpl never.
+Arguments add_modal {_} _%I _%I _%I {_}.
+Hint Mode AddModal + - ! ! : typeclass_instances.
+
+Lemma add_modal_id {PROP : bi} (P Q : PROP) : AddModal P P Q.
+Proof. by rewrite /AddModal wand_elim_r. Qed.
 
 Class IsCons {A} (l : list A) (x : A) (k : list A) := is_cons : l = x :: k.
 Class IsApp {A} (l k1 k2 : list A) := is_app : l = k1 ++ k2.
diff --git a/theories/proofmode/coq_tactics.v b/theories/proofmode/coq_tactics.v
index 0648e90709ddd3a1602496861f9c6e51637c4232..4d14e2e3a6fabd2f2554a15aefb6c9d86041e8c5 100644
--- a/theories/proofmode/coq_tactics.v
+++ b/theories/proofmode/coq_tactics.v
@@ -450,6 +450,11 @@ Proof.
 Qed.
 
 (** * Basic rules *)
+Lemma tac_eval Δ Q Q' :
+  Q = Q' →
+  envs_entails Δ Q' → envs_entails Δ Q.
+Proof. by intros ->. Qed.
+
 Class AffineEnv (Γ : env PROP) := affine_env : Forall Affine Γ.
 Global Instance affine_env_nil : AffineEnv Enil.
 Proof. constructor. Qed.
@@ -731,8 +736,7 @@ Qed.
 
 Lemma tac_specialize_assert Δ Δ' Δ1 Δ2' j q neg js R P1 P2 P1' Q :
   envs_lookup_delete j Δ = Some (q, R, Δ') →
-  IntoWand q false R P1 P2 →
-  ElimModal P1' P1 Q Q →
+  IntoWand q false R P1 P2 → AddModal P1' P1 Q →
   (''(Δ1,Δ2) ← envs_split (if neg is true then Right else Left) js Δ';
     Δ2' ← envs_app false (Esnoc Enil j P2) Δ2;
     Some (Δ1,Δ2')) = Some (Δ1,Δ2') → (* does not preserve position of [j] *)
@@ -743,7 +747,7 @@ Proof.
     destruct (envs_app _ _ _) eqn:?; simplify_eq/=.
   rewrite envs_lookup_sound // envs_split_sound //.
   rewrite (envs_app_singleton_sound Δ2) //; simpl.
-  rewrite HP1 into_wand /= -(elim_modal P1' P1 Q Q). cancel [P1'].
+  rewrite HP1 into_wand /= -(add_modal P1' P1 Q). cancel [P1'].
   apply wand_intro_l. by rewrite assoc !wand_elim_r.
 Qed.
 
@@ -753,14 +757,14 @@ Proof. by unlock. Qed.
 Lemma tac_specialize_frame Δ Δ' j q R P1 P2 P1' Q Q' :
   envs_lookup_delete j Δ = Some (q, R, Δ') →
   IntoWand q false R P1 P2 →
-  ElimModal P1' P1 Q Q →
+  AddModal P1' P1 Q →
   envs_entails Δ' (P1' ∗ locked Q') →
   Q' = (P2 -∗ Q)%I →
   envs_entails Δ Q.
 Proof.
   rewrite /envs_entails. intros [? ->]%envs_lookup_delete_Some ?? HPQ ->.
   rewrite envs_lookup_sound //. rewrite HPQ -lock.
-  rewrite into_wand -{2}(elim_modal P1' P1 Q Q). cancel [P1'].
+  rewrite into_wand -{2}(add_modal P1' P1 Q). cancel [P1'].
   apply wand_intro_l. by rewrite assoc !wand_elim_r.
 Qed.
 
@@ -847,7 +851,7 @@ Proof.
 Qed.
 
 Lemma tac_assert Δ Δ1 Δ2 Δ2' neg js j P P' Q :
-  ElimModal P' P Q Q →
+  AddModal P' P Q →
   envs_split (if neg is true then Right else Left) js Δ = Some (Δ1,Δ2) →
   envs_app false (Esnoc Enil j P) Δ2 = Some Δ2' →
   envs_entails Δ1 P' → envs_entails Δ2' Q → envs_entails Δ Q.
diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index e283e18deed5bf3226c14dafebfd3c5e97dfdc31..a5f23b9255fbe83244aecef1be08650e38f1c0a0 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -98,6 +98,13 @@ Tactic Notation "iStartProof" uconstr(PROP) :=
 
 Tactic Notation "iStartProof" := iStartProof _.
 
+(** * Simplification *)
+Tactic Notation "iEval" tactic(t) :=
+  try iStartProof;
+  try (eapply tac_eval; [t; reflexivity|]).
+
+Tactic Notation "iSimpl" := iEval simpl.
+
 (** * Context manipulation *)
 Tactic Notation "iRename" constr(H1) "into" constr(H2) :=
   eapply tac_rename with _ H1 H2 _ _; (* (i:=H1) (j:=H2) *)
@@ -430,15 +437,11 @@ Notation "( H $! x1 .. xn 'with' pat )" :=
 Notation "( H 'with' pat )" := (ITrm H hnil pat) (at level 0).
 
 (*
-There is some hacky stuff going on here (most probably there is a Coq bug).
-Holes -- like unresolved type class instances -- in the argument `xs` are
-resolved at arbitrary moments. It seems that tactics like `apply`, `split` and
-`eexists` trigger type class search to resolve these holes. To avoid TC being
-triggered too eagerly, this tactic uses `refine` at various places instead of
-`apply`.
-
-TODO: Investigate what really is going on. Is there a related to Cog bug #5752?
-When should holes in an `open_constr` be resolved?
+There is some hacky stuff going on here: because of Coq bug #6583, unresolved
+type classes in the arguments `xs` are resolved at arbitrary moments. Tactics
+like `apply`, `split` and `eexists` wrongly trigger type class search to resolve
+these holes. To avoid TC being triggered too eagerly, this tactic uses `refine`
+at most places instead of `apply`.
 *)
 Local Tactic Notation "iSpecializeArgs" constr(H) open_constr(xs) :=
   let rec go xs :=
@@ -508,7 +511,7 @@ Local Tactic Notation "iSpecializePat" open_constr(H) constr(pat) :=
          [env_reflexivity || fail "iSpecialize:" H1 "not found"
          |solve_to_wand H1
          |lazymatch m with
-          | GSpatial => apply elim_modal_dummy
+          | GSpatial => apply add_modal_id
           | GModal => apply _ || fail "iSpecialize: goal not a modality"
           end
          |env_reflexivity ||
@@ -531,7 +534,7 @@ Local Tactic Notation "iSpecializePat" open_constr(H) constr(pat) :=
          [env_reflexivity || fail "iSpecialize:" H1 "not found"
          |solve_to_wand H1
          |lazymatch m with
-          | GSpatial => apply elim_modal_dummy
+          | GSpatial => apply add_modal_id
           | GModal => apply _ || fail "iSpecialize: goal not a modality"
           end
          |iFrame "∗ #"; apply tac_unlock ||
@@ -625,7 +628,12 @@ Tactic Notation "iIntoValid" open_constr(t) :=
 
 (* The tactic [tac] is called with a temporary fresh name [H]. The argument
 [lazy_tc] denotes whether type class inference on the premises of [lem] should
-be performed before (if false) or after (if true) [tac H] is called. *)
+be performed before (if false) or after (if true) [tac H] is called.
+
+The tactic [iApply] uses laxy type class inference, so that evars can first be
+instantiated by matching with the goal, whereas [iDestruct] does not, because
+eliminations may not be performed when type classes have not been resolved.
+*)
 Tactic Notation "iPoseProofCore" open_constr(lem)
     "as" constr(p) constr(lazy_tc) tactic(tac) :=
   try iStartProof;
@@ -1659,7 +1667,7 @@ Tactic Notation "iAssertCore" open_constr(Q)
      | false =>
        eapply tac_assert with _ _ _ lr Hs' H Q _;
          [lazymatch m with
-          | GSpatial => apply elim_modal_dummy
+          | GSpatial => apply add_modal_id
           | GModal => apply _ || fail "iAssert: goal not a modality"
           end
          |env_reflexivity ||