Commit 81022281 authored by Robbert Krebbers's avatar Robbert Krebbers

Compatibility with Coq 8.5.

parent 22511f77
......@@ -261,7 +261,7 @@ Lemma map_subset_alt {A} (m1 m2 : M A) :
Proof.
rewrite strict_spec_alt. split.
- intros [? Heq]; split; [done|].
destruct (decide (Exists (λ '(i,_), m1 !! i = None) (map_to_list m2)))
destruct (decide (Exists (λ ix, m1 !! ix.1 = None) (map_to_list m2)))
as [[[i x] [?%elem_of_map_to_list ?]]%Exists_exists
|Hm%(not_Exists_Forall _)]; [eauto|].
destruct Heq; apply (anti_symm _), map_subseteq_spec; [done|intros i x Hi].
......
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