 22 Feb, 2018 1 commit


Robbert Krebbers authored
As reported by @jjourdan: framing now no longer back tracks on whether to strip laters or not. When framing below a later, we now only make it strip laters of the head of the frame.

 21 Feb, 2018 2 commits


Robbert Krebbers authored

Ralf Jung authored

 20 Feb, 2018 17 commits


Robbert Krebbers authored

Ralf Jung authored


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
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
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 authored
Use `NoBackTrack` type class for framing with ▷ Closes #153 See merge request FP/iriscoq!112

Robbert Krebbers authored

Robbert Krebbers authored

 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 1 commit


Robbert Krebbers authored
