 20 Feb, 2018 11 commits


JacquesHenri Jourdan authored
The finiteness was needed to have the axiom of choice over the domain. This axiom is not needed if cmra_extend is in Type.

JacquesHenri Jourdan authored
Revert "Remove the domain finiteness hypothesis for the function CMRA, and put cmra_extend in Type." This reverts commit fa897ff5.

JacquesHenri Jourdan authored
The finiteness was needed to have the axiom of choice over the domain. This axiom is not needed if cmra_extend is in Type.

Robbert authored
Stronger `iNext` that performs arithmetic cancelation Closes #148 See merge request FP/iriscoq!109

Robbert Krebbers authored
Fixed by stdpp 93b4ec70e13a573a9055a5bf1269f5885e18e843.

Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored
We now use the `Maybe` prefix as also used for `Frame`: it indicates whether progress has been made by stripping of a later or not.

Robbert Krebbers authored

 16 Feb, 2018 3 commits
 15 Feb, 2018 1 commit


Ralf Jung authored

 13 Feb, 2018 3 commits
 09 Feb, 2018 1 commit


Robbert Krebbers authored

 08 Feb, 2018 4 commits


Robbert Krebbers authored

Robbert Krebbers authored

Robbert authored
Various improvements to iFrame Closes #145 See merge request FP/iriscoq!110
 07 Feb, 2018 5 commits


Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored
We already supported framing under wands.

Robbert Krebbers authored

Robbert Krebbers authored
For example, framing `P` in `(P ∨ Q) ∗ R` now succeeds and turns the goal into `R`.

 06 Feb, 2018 1 commit


Ralf Jung authored

 03 Feb, 2018 1 commit


Ralf Jung authored

 02 Feb, 2018 2 commits


Robbert Krebbers authored

Robbert Krebbers authored

 31 Jan, 2018 1 commit


Robbert Krebbers authored

 29 Jan, 2018 2 commits


Robbert Krebbers authored

Ralf Jung authored

 24 Jan, 2018 5 commits


Ralf Jung authored

Ralf Jung authored
Make invariants closed under weakening. See merge request FP/iriscoq!85

Robbert Krebbers authored

Robbert Krebbers authored
This partially solves #112.

Robbert authored
Consistently name `wp_value_inv` See merge request FP/iriscoq!108
