Simplify definition of `mapset_dom_with`.

This fixes issue #183 (closed)

It is not clear that it fixes similar issues. But regardless, I would say that the simplification of the definition of dom is a sensible change.

I think the real fix for #183 (closed) is to convince that Coq devs that we need Arguments ... : simpl really never ever or a better variant of ! that does not head reduce.

The Opaque declarations (such as the one for gmap_empty) don't just tell simpl to really not unfold a constant, but they also cause the conversion and unification algorithm to delay unfolding the constant. For something as gmap_empty it seems that delaying its unfolding is always a bad idea; it should be unfolded as eagerly as possible.

Another thing to add to your discussion list when you meet the Coq team. ;)

mentioned in issue #183 (closed)

added 1 commit

• 84e0ebf3 - Simplify `dom` even further.

Compare with previous version

I made the dom implementation even simpler, to use fmap instead of mapset_dom_with (which in turn uses omap). I kept the simplification to mapset_dom_with too.

Going to merge.

enabled an automatic merge when the pipeline for 84e0ebf3 succeeds

aborted the automatic merge because source branch was updated

added 1 commit

• 85d5c299 - Simplify `dom` even further.

Compare with previous version

merged

mentioned in commit 40e5274f