Commit b6859ed1 authored by Robbert Krebbers's avatar Robbert Krebbers

Disable test, since it's not compatible with Coq 8.8 and 8.9.

parent eef6260f
Pipeline #23921 passed with stage
in 17 minutes and 43 seconds
......@@ -239,6 +239,8 @@ Proof.
iFrame.
Qed.
(* Test for issue #288 *)
(* FIXME: Restore once we drop support for Coq 8.8 and Coq 8.9.
Lemma test_iExists_unused : (∃ P : PROP, ∃ x : nat, P)%I.
Proof.
iExists _.
......@@ -246,6 +248,7 @@ Proof.
iAssert emp%I as "H"; first done.
iExact "H".
Qed.
*)
(* Check coercions *)
Lemma test_iExist_coercion (P : Z PROP) : ( x, P x) - x, P x.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment