strengthen cmra_op_discrete

See merge request iris/iris!618

add Cinl_valid, Cinr_valid

See merge request iris/iris!621

reuse PreG class in G class where possible

See merge request iris/iris!617

gen_heap: expose that inG identities are preserved

See merge request iris/iris!585

Done with a script by Tej; see
iris/iris!609 for details.

Better errors when opening an invariant/mask changing update around a non-atomic WP

See merge request iris/iris!614

This makes sure that when trying to open an invariant or to eliminate a mask-changing
update around a non-atomic WP that it doesn't fail with "cannot eliminate modality",
but instead gives an side-condition `Atomic ...` informing the user what's going on.

Unlike the class `ElimModal` and `ElimInv`, the class `ElimAcc` was not yet equipped
with a Coq side-condition. This commit adds such a side-condition.

Move HeapLang class instances and tactics to separate file

See merge request iris/iris!612

Prove internal_eq_timeless

See merge request iris/iris!607

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

https://gitlab.mpi-sws.org/iris/iris/-/wikis/style-guide

Remove old `Hint Extern` hack for `impl_persistent` that seems no longer needed.

See merge request iris/iris!610