diff --git a/theories/tests/proofmode.v b/theories/tests/proofmode.v
index 3fb0578643d560fd45d808d10ec8dfb767fc635c..d70e016aa0bc7f1bf37a4eb096af7bba98018f08 100644
--- a/theories/tests/proofmode.v
+++ b/theories/tests/proofmode.v
@@ -328,12 +328,8 @@ Proof.
   done.
 Qed.
 
-(* TODO: This test is broken in Coq 8.6. Should be restored once we drop Coq
-8.6 support. See also issue #108. *)
-(*
-Lemma test_iIntros_pure : (⌜ ¬False ⌝ : uPred M)%I.
+Lemma test_iIntros_pure_neg : (⌜ ¬False ⌝ : uPred M)%I.
 Proof. by iIntros (?). Qed.
-*)
 End tests.
 
 Section more_tests.