Robbert Krebbers authored 4 years ago and Ralf Jung committed 4 years ago

* Add lemma `map_omap_union`.
* Add lemmas `map_disjoint_fmap` and `map_disjoint_omap`.
* Add lemmas `fmap_merge` and `omap_merge`.
* Add lemma `omap_delete`.
* Generalize `omap_insert` and `omap_singleton` to cover both the `Some` and `None` case. Add `_Some` and `_None` versions of the lemmas for the specific cases.
* Generalize `map_size_insert` and `map_size_delete` in the same way.
* Add lemmas `lookup_fmap_Some`, `lookup_omap_Some`, and `lookup_omap_id_Some`.

Remove duplicate `map_fmap_empty` of `fmap_empty`, and rename `map_fmap_empty_inv` into `fmap_empty_inv` for consistency's sake.

Fixes new Coq master warning deprecated-hint-without-locality.

Fix in preparation for https://github.com/coq/coq/pull/13188

Tej Chajed authored 4 years ago and Robbert Krebbers committed 4 years ago

Set Default Goal Selector "!" makes it illegal to ever apply a tactic
with more than one goal (instead, must focus with bullets or braces).

Ralf Jung authored 4 years ago and Robbert Krebbers committed 4 years ago

by Tej

According to the documentation
https://coq.inria.fr/distrib/current/refman/proof-engine/tactics.html#coq:cmd.create-hintdb,
when creating a hint database without discrimination, Coq uses the
legacy implementation, which only uses Discrimination Trees for goals
without evars and does not use opaqueness information. This commit
switches the hint databases of stdpp to the new implementation.

This was done using `sed --in-place 's/[[:space:]]\+$//' theories/*.v`.

For other operations, like `<$>`,  such lemmas appear to make little sense, since
they require premises involving `!!`.

This follows iris!387
This closes issue #54.