Merge branch 'master' of https://gitlab.mpi-sws.org/FP/iris-coq

theories/algebra/gmap.v

@@ -146,8 +146,7 @@ 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 ∅. exists ∅. (* FIXME: exists ∅, ∅. results in a TC loop in Coq 8.6 *)
-      split_and!=> -i; symmetry; symmetry in Hm; move: Hm=> /(_ i);
+    { exists ∅, ∅. 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 [->|].

theories/base_logic/lib/fancy_updates.v

@@ -195,8 +195,7 @@ Section proofmode_classes.
   Proof. by rewrite /ElimModal fupd_frame_r wand_elim_r fupd_trans. Qed.
 End proofmode_classes.
 
-Hint Extern 2 (coq_tactics.of_envs _ ⊢ _) =>
-  match goal with |- _ ⊢ |={_}=> _ => iModIntro end.
+Hint Extern 2 (coq_tactics.of_envs _ ⊢ |={_}=> _) => iModIntro.
 
 (** Fancy updates that take a step. *)
 

theories/base_logic/lib/na_invariants.v

@@ -9,7 +9,11 @@ Import uPred.
 Definition na_inv_pool_name := gname.
 
 Class na_invG Σ :=
-  na_inG :> inG Σ (prodR coPset_disjR (gset_disjR positive)).
+  na_inv_inG :> inG Σ (prodR coPset_disjR (gset_disjR positive)).
+Definition na_invΣ : gFunctors :=
+  #[ GFunctor (constRF (prodR coPset_disjR (gset_disjR positive))) ].
+Instance subG_na_invG {Σ} : subG na_invΣ Σ → na_invG Σ.
+Proof. solve_inG. Qed.
 
 Section defs.
   Context `{invG Σ, na_invG Σ}.

theories/proofmode/tactics.v

@@ -1270,19 +1270,12 @@ Hint Extern 0 (of_envs _ ⊢ _) => iAssumption.
 Hint Extern 0 (of_envs _ ⊢ _) => progress iIntros.
 Hint Resolve uPred.internal_eq_refl'. (* Maybe make an [iReflexivity] tactic *)
 
-(* We should be able to write [Hint Extern 1 (of_envs _ ⊢ (_ ∗ _)%I) => ...],
-but then [eauto] mysteriously fails. See bug 4762 *)
-Hint Extern 1 (of_envs _ ⊢ _) =>
-  match goal with
-  | |- _ ⊢ _ ∧ _ => iSplit
-  | |- _ ⊢ _ ∗ _ => iSplit
-  | |- _ ⊢ ▷ _ => iNext
-  | |- _ ⊢ □ _ => iClear "*"; iAlways
-  | |- _ ⊢ ∃ _, _ => iExists _
-  | |- _ ⊢ |==> _ => iModIntro
-  | |- _ ⊢ ◇ _ => iModIntro
-  end.
-Hint Extern 1 (of_envs _ ⊢ _) =>
-  match goal with |- _ ⊢ (_ ∨ _)%I => iLeft end.
-Hint Extern 1 (of_envs _ ⊢ _) =>
-  match goal with |- _ ⊢ (_ ∨ _)%I => iRight end.
+Hint Extern 1 (of_envs _ ⊢ _ ∧ _) => iSplit.
+Hint Extern 1 (of_envs _ ⊢ _ ∗ _) => iSplit.
+Hint Extern 1 (of_envs _ ⊢ ▷ _) => iNext.
+Hint Extern 1 (of_envs _ ⊢ □ _) => iClear "*"; iAlways.
+Hint Extern 1 (of_envs _ ⊢ ∃ _, _) => iExists _.
+Hint Extern 1 (of_envs _ ⊢ |==> _) => iModIntro.
+Hint Extern 1 (of_envs _ ⊢ ◇ _) => iModIntro.
+Hint Extern 1 (of_envs _ ⊢ _ ∨ _) => iLeft.
+Hint Extern 1 (of_envs _ ⊢ _ ∨ _) => iRight.