enable a test that failed with Coq 8.6

a82aa047 · Ralf Jung · c650b0ee · a82aa047
Commit a82aa047 authored Apr 23, 2018 by Ralf Jung
Hide whitespace changes
Inline Side-by-side

Showing with 1 addition and 5 deletions

theories/tests/proofmode.v theories/tests/proofmode.v +1 -5

No files found.
--- 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.