Commit f69cdc8c authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Make gmap_empty Opaque to avoid simpl unfolding it.

This happened for example in <[i:=x]>∅, where simpl unfold insert (despite
it being declared simpl never) because ∅ reduces to a constructor.
parent e9e55145
...@@ -33,6 +33,7 @@ Defined. ...@@ -33,6 +33,7 @@ Defined.
Instance gmap_lookup `{Countable K} {A} : Lookup K A (gmap K A) := λ i m, Instance gmap_lookup `{Countable K} {A} : Lookup K A (gmap K A) := λ i m,
let (m,_) := m in m !! encode i. let (m,_) := m in m !! encode i.
Instance gmap_empty `{Countable K} {A} : Empty (gmap K A) := GMap I. Instance gmap_empty `{Countable K} {A} : Empty (gmap K A) := GMap I.
Global Opaque gmap_empty.
Lemma gmap_partial_alter_wf `{Countable K} {A} (f : option A option A) m i : Lemma gmap_partial_alter_wf `{Countable K} {A} (f : option A option A) m i :
gmap_wf m gmap_wf (partial_alter f (encode i) m). gmap_wf m gmap_wf (partial_alter f (encode i) m).
Proof. Proof.
......
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