From e2abd6c428acb5a6b85559d281564d522bd68a7a Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 11 Jan 2017 14:07:34 +0100
Subject: [PATCH] Remove some FIXMEs: Coq bug 4762 has been fixed in 8.6.

---
 theories/base_logic/lib/fancy_updates.v |  3 +--
 theories/proofmode/tactics.v            | 25 +++++++++----------------
 2 files changed, 10 insertions(+), 18 deletions(-)

diff --git a/theories/base_logic/lib/fancy_updates.v b/theories/base_logic/lib/fancy_updates.v
index d6817d633..91fe5efe5 100644
--- a/theories/base_logic/lib/fancy_updates.v
+++ b/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. *)
 
diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index a32345598..a113eb39f 100644
--- a/theories/proofmode/tactics.v
+++ b/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.
-- 
GitLab