Gregory Malecha authored 5 years ago and Robbert Krebbers committed 5 years ago

- remove "odd" comment
- move atomic triples to bi_scope

Use `_inv` for the reverse direction.

This feature is now deprecated in Coq master (see
https://github.com/coq/coq/pull/7791).

Instead of passing a partially-applied lemma directly to Hint Resolve,
first create a definition and then make that reference a hint.

Tej Chajed authored 5 years ago and Ralf Jung committed 5 years ago

Add array_copy_to (copy in-place to destination array) and array_clone
(copy to a freshly allocated array). The heap_lang spec and proof for
array_copy_to are inspired by
https://gitlab.mpi-sws.org/iris/lambda-rust/blob/3b4ae69fa3be1344245245bf05e5e80e790e064d/theories/lang/lib/memcpy.v.

Fixes #293.

- Export `total_weakestpre` in `lifting` already, like we do for `weakestpre`.
- Do not export modules that are already exported by exported modules.

Thanks to @Blaisorblade, based on
https://gitlab.mpi-sws.org/Blaisorblade/iris-coq/commit/0739608d32272ca5679bf504a569b3ddd50c7b29,
but applied to similar notations too.

It was already marked as deprecated in `doc/proof_mode.md`.

- Rename `IPureElim` -> `iPure`, `IAlwaysElim` -> `IIntuitionistic`
- Drop `IAlwaysIntro` (it's just `IModalIntro`).

Tej Chajed authored 5 years ago and Ralf Jung committed 5 years ago

Fixes a new warning on Coq 8.12+alpha when implicit annotations are used
in positions where they are ignored.