Fixes for compilation with Coq 8.6.

algebra/cmra.v

@@ -321,7 +321,7 @@ Proof. by apply cmra_pcore_dup' with x. Qed.
 
 (** ** Exclusive elements *)
 Lemma exclusiveN_l n x `{!Exclusive x} y : ✓{n} (x ⋅ y) → False.
-Proof. intros ?%cmra_validN_le%exclusive0_l; auto with arith. Qed.
+Proof. intros. eapply (exclusive0_l x y), cmra_validN_le; eauto with lia. Qed.
 Lemma exclusiveN_r n x `{!Exclusive x} y : ✓{n} (y ⋅ x) → False.
 Proof. rewrite comm. by apply exclusiveN_l. Qed.
 Lemma exclusive_l x `{!Exclusive x} y : ✓ (x ⋅ y) → False.
@@ -329,7 +329,7 @@ Proof. by move /cmra_valid_validN /(_ 0) /exclusive0_l. Qed.
 Lemma exclusive_r x `{!Exclusive x} y : ✓ (y ⋅ x) → False.
 Proof. rewrite comm. by apply exclusive_l. Qed.
 Lemma exclusiveN_opM n x `{!Exclusive x} my : ✓{n} (x ⋅? my) → my = None.
-Proof. destruct my. move=> /(exclusiveN_l _ x) []. done. Qed.
+Proof. destruct my as [y|]. move=> /(exclusiveN_l _ x) []. done. Qed.
 
 (** ** Order *)
 Lemma cmra_included_includedN n x y : x ≼ y → x ≼{n} y.

algebra/dra.v

@@ -167,10 +167,10 @@ Proof.
   - intros [x px ?]; split; naive_solver eauto using dra_core_idemp.
   - intros [x px ?] [y py ?] [[z pz ?] [? Hy]]; simpl in *.
     destruct (dra_core_mono x z) as (z'&Hz').
-    unshelve eexists (Validity z' (px ∧ py ∧ pz) _); [|split; simpl].
+    unshelve eexists (Validity z' (px ∧ py ∧ pz) _).
     { intros (?&?&?); apply Hz'; tauto. }
-    + tauto.
-    + intros. rewrite Hy //. tauto.
+    split; simpl; first tauto.
+    intros. rewrite Hy //. tauto.
   - by intros [x px ?] [y py ?] (?&?&?).
 Qed.
 Canonical Structure validityR : cmraT :=

algebra/gmap.v

@@ -138,7 +138,8 @@ Proof.
   - intros n m1 m2 Hm i; apply cmra_validN_op_l with (m2 !! i).
     by rewrite -lookup_op.
   - intros n m. induction m as [|i x m Hi IH] using map_ind=> m1 m2 Hmv Hm.
-    { exists ∅, ∅; split_and!=> -i; symmetry; symmetry in Hm; move: Hm=> /(_ i);
+    { exists ∅. exists ∅. (* FIXME: exists ∅, ∅. results in a TC loop in Coq 8.6 *)
+      split_and!=> -i; symmetry; symmetry in Hm; move: Hm=> /(_ i);
         rewrite !lookup_op !lookup_empty ?dist_None op_None; intuition. }
     destruct (IH (delete i m1) (delete i m2)) as (m1'&m2'&Hm'&Hm1'&Hm2').
     { intros j; move: Hmv=> /(_ j). destruct (decide (i = j)) as [->|].
@@ -342,8 +343,8 @@ Section freshness.
     ✓ u → LeftId (≡) u (⋅) →
     u ~~>: P → ∅ ~~>: λ m, ∃ y, m = {[ i := y ]} ∧ P y.
   Proof. eauto using alloc_unit_singleton_updateP. Qed.
-  Lemma alloc_unit_singleton_update u i (y : A) :
-    ✓ u → LeftId (≡) u (⋅) → u ~~> y → ∅ ~~> {[ i := y ]}.
+  Lemma alloc_unit_singleton_update (u : A) i (y : A) :
+    ✓ u → LeftId (≡) u (⋅) → u ~~> y → (∅:gmap K A) ~~> {[ i := y ]}.
   Proof.
     rewrite !cmra_update_updateP;
       eauto using alloc_unit_singleton_updateP with subst.
@@ -379,7 +380,7 @@ Proof.
 Qed.
 
 Lemma alloc_unit_singleton_local_update i x mf :
-  mf ≫= (!! i) = None → ✓ x → ∅ ~l~> {[ i := x ]} @ mf.
+  mf ≫= (!! i) = None → ✓ x → (∅:gmap K A) ~l~> {[ i := x ]} @ mf.
 Proof.
   intros Hi; apply alloc_singleton_local_update. by rewrite lookup_opM Hi.
 Qed.

heap_lang/lifting.v

@@ -33,6 +33,7 @@ Context `{irisG heap_lang Σ}.
 Implicit Types P Q : iProp Σ.
 Implicit Types Φ : val → iProp Σ.
 Implicit Types efs : list expr.
+Implicit Types σ : state.
 
 (** Bind. This bundles some arguments that wp_ectx_bind leaves as indices. *)
 Lemma wp_bind {E e} K Φ :

proofmode/coq_tactics.v

@@ -135,7 +135,7 @@ Proof. intros. rewrite envs_lookup_sound //. by rewrite always_if_elim. Qed.
 Lemma envs_lookup_persistent_sound Δ i P :
   envs_lookup i Δ = Some (true,P) → Δ ⊢ □ P ★ Δ.
 Proof.
-  intros. apply: always_entails_l. by rewrite envs_lookup_sound // sep_elim_l.
+  intros. apply (always_entails_l _ _). by rewrite envs_lookup_sound // sep_elim_l.
 Qed.
 
 Lemma envs_lookup_split Δ i p P :
@@ -277,8 +277,8 @@ Proof.
 Qed.
 Global Instance of_envs_proper : Proper (envs_Forall2 (⊣⊢) ==> (⊣⊢)) (@of_envs M).
 Proof.
-  intros Δ1 Δ2 ?; apply (anti_symm (⊢)); apply of_envs_mono;
-    eapply envs_Forall2_impl; [| |symmetry|]; eauto using equiv_entails.
+  intros Δ1 Δ2 HΔ; apply (anti_symm (⊢)); apply of_envs_mono;
+    eapply (envs_Forall2_impl (⊣⊢)); [| |symmetry|]; eauto using equiv_entails.
 Qed.
 Global Instance Envs_mono (R : relation (uPred M)) :
   Proper (env_Forall2 R ==> env_Forall2 R ==> envs_Forall2 R) (@Envs M).
@@ -388,7 +388,7 @@ Qed.
 
 (** * Always *)
 Lemma tac_always_intro Δ Q : envs_persistent Δ = true → (Δ ⊢ Q) → Δ ⊢ □ Q.
-Proof. intros. by apply: always_intro. Qed.
+Proof. intros. by apply (always_intro _ _). Qed.
 
 Lemma tac_persistent Δ Δ' i p P P' Q :
   envs_lookup i Δ = Some (p, P) → IntoPersistentP P P' →

proofmode/tactics.v

@@ -26,7 +26,7 @@ Ltac iFresh :=
      first use [cbv] to compute the domain of [Δ] *)
      let Hs := eval cbv in (envs_dom Δ) in
      eval vm_compute in (fresh_string_of_set "~" (of_list Hs))
-  | _ => constr:"~"
+  | _ => constr:("~")
   end.
 
 Tactic Notation "iTypeOf" constr(H) tactic(tac):=