From 850e6c3cc19455579d505fbf9134de7db2f6ab21 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Wed, 14 Feb 2018 13:35:31 +0100
Subject: [PATCH] Remove Admitted.

---
 theories/tests/proofmode_monpred.v | 14 ++++++++++----
 1 file changed, 10 insertions(+), 4 deletions(-)

diff --git a/theories/tests/proofmode_monpred.v b/theories/tests/proofmode_monpred.v
index cf7d297f5..fb7b6b35f 100644
--- a/theories/tests/proofmode_monpred.v
+++ b/theories/tests/proofmode_monpred.v
@@ -75,10 +75,16 @@ Section tests.
     ∀ᵢ emp -∗ ∀ᵢ P -∗ ∀ᵢ Q -∗ R -∗ ∀ᵢ (P ∗ Q).
   Proof. iIntros "#? HP HQ HR". iAlways. by iSplitL "HP". Qed.
 
-  (* We do not use section variables to avoid coq bug #5735. *)
-  Instance BU : BUpd PROP. Admitted.
-  Instance FU : FUpd PROP. Admitted.
-  Instance FUF : FUpdFacts PROP. Admitted.
+  (* This is a hack to avoid avoid coq bug #5735: sections variables
+     ignore hint modes. So we assume the instances in a way that
+     cannot be used by type class resolution, and then declare the
+     instance. as such. *)
+  Context (BU0 : BUpd PROP * unit).
+  Instance BU : BUpd PROP := fst BU0.
+  Context (FU0 : FUpd PROP * unit).
+  Instance FU : FUpd PROP := fst FU0.
+  Context (FUF0 : FUpdFacts PROP * unit).
+  Instance FUF : FUpdFacts PROP := fst FUF0.
 
   Lemma test_apply_fupd_intro_mask E1 E2 P :
     E2 ⊆ E1 → P -∗ |={E1,E2}=> |={E2,E1}=> P.
-- 
GitLab