GitLab

We define basic updates as:

    |==> P  :=  (∀ Q, (P -∗ ■ Q) -∗ ■ Q)

From this definitions, we can prove all laws of basic updates, apart from
those related to frame preserving updates. For that, we need the following
primitive rule:

    x ~~>: Φ →
    uPred_ownM x ∗ (∀ y, ⌜Φ y⌝ -∗ uPred_ownM y -∗ ■ R) ⊢ ■ R.

So, in total, this gets rid of 1 primitive connective (|==>) and 5 primitive
rules (those of `|==>`), which is replaced by one new primitive rule.

opam is broken beyond repair for system ocaml, it seems... see
<https://github.com/ocaml/opam/issues/3586>.

Modify adequacy proof to not break the 'fancy update' abstraction.

See merge request FP/iris-coq!171

Use explicit names in some scripts, re-organize fupd plainly derived laws, adjust wsat import/export.

Modify adequacy proof to not break the 'fancy update' abstraction. Modify fupd plainly interface and add new derived results.

Prophecy variables

See merge request FP/iris-coq!173

Support multiple steps in `PureExec`.

See merge request FP/iris-coq!179