Commit 87779ac4 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Add test case.

parent 13da2867
Pipeline #65902 passed with stage
in 4 minutes and 22 seconds
...@@ -82,3 +82,10 @@ Proof. ...@@ -82,3 +82,10 @@ Proof.
Fail progress simplify_eq. Fail progress simplify_eq.
done. done.
Qed. Qed.
(** Test case for issue #139 *)
Lemma test_issue_139 (m : gmap nat nat) : x, x dom m.
Proof.
destruct (exist_fresh (dom m)); eauto.
Qed.
Supports Markdown
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