LookupTotal

See merge request iris/stdpp!97

Dan Frumin authored 5 years ago and Robbert Krebbers committed 5 years ago

In accordance with
<!93>

Added TCForall2_Forall2 lemma

See merge request !107

Namely, `fmap`, `omap`, `imap`, `mbind`, `mjoin`, `zip_with`.

As part of this, refactor slightly to put all `omap`, `imap`, and `seq`
results together.

The `Equiv` instance for the domain is not needed.

Opaquify proofs in gmap_partial_alter (fix #46)

Closes #46

See merge request !106

Paolo G. Giarrusso authored 5 years ago and Robbert Krebbers committed 5 years ago

- Ensure gmap well-formedness proofs are fully opaque.
- Use pattern-matching lambdas over lets.

Add lemmas regarding set_seq

See merge request !105

Remove `:>>` subclass instance declarations

See merge request !104

There are not documented in
https://coq.inria.fr/refman/addendum/type-classes.html?highlight=class#coq:cmd.class,
and they don't have any advantage, so it's better to stop using them.

Update gitignore for compatibility with Coq master

See merge request !103

See https://github.com/coq/coq/pull/10947 (.coqdeps.d now uses the name
of the Coq Makefile) and https://github.com/coq/coq/pull/8642 (Coq now
generates empty interface files *.vos when compiling).