 21 Feb, 2018 8 commits


Ralf Jung authored


Ralf Jung authored

Ralf Jung authored

Ralf Jung authored
weaken BI axiom persistently_and_sep_elim and rederive the stronger form See merge request FP/iriscoq!119

Ralf Jung authored

Ralf Jung authored

Robbert Krebbers authored
For better support for eliminating affine/absorbing separating conjunctions in the persistent context/under a plainness/persistence modality.

 20 Feb, 2018 20 commits


Robbert Krebbers authored
This regression was caused by a bug in handling spec patterns.

Ralf Jung authored

JacquesHenri Jourdan authored

JacquesHenri Jourdan authored
Remove the domain finiteness hypothesis for the function CMRA, and put cmra_extend in Type. See merge request FP/iriscoq!118

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

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 Krebbers authored

Robbert Krebbers authored

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

Robbert Krebbers authored
In the same way that `iFrame` would succeed on said goals.

Robbert Krebbers authored

 19 Feb, 2018 12 commits


Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored
This made the definition much simpler, and provides support for all specialization patterns (although most are not very useful in combination with `iAssert`).

Robbert Krebbers authored

Robbert Krebbers authored

Ralf Jung authored


Ralf Jung authored

JacquesHenri Jourdan authored

JacquesHenri Jourdan authored
