 19 Apr, 2016 7 commits


Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored
That way, we do not have useless type annotations of the form "v : language.val heap_lang" cluttering about any goal. Note, that we could decide to eta expand everywhere (as we do for ∀ and ∃), and use the notation "WP e {{ Q }}" for "wp e ⊤ (λ _, Q)".

Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored
newline before the first context" and "shuffle 0width spaces around so they are distributed more evenly" This reverts commits e3c56f9e and 7fc1124c, which are workarounds for Coq bug https://coq.inria.fr/bugs/show_bug.cgi?id=4675 Also, this commit fixes the levels to avoid parantheses.

 18 Apr, 2016 2 commits


Ralf Jung authored

Robbert Krebbers authored

 15 Apr, 2016 3 commits


Ralf Jung authored
Pros: * It does not matter how editors render the 0width space, everything is always aligned * In ProofGeneral, there is no more incorrectn indentation of the first line Cons: * There is an empty line between the bar ending the Coq context, and the first Iris hypothesis

Ralf Jung authored

Ralf Jung authored

 14 Apr, 2016 1 commit


Robbert Krebbers authored

 13 Apr, 2016 5 commits


Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored

Ralf Jung authored

Ralf Jung authored

 12 Apr, 2016 6 commits


Robbert Krebbers authored

Robbert Krebbers authored
It is not a library; it does not contain code, but instead is a core part of heap_lang.

Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored
This reverts commit 3cc38ff6. The reverted pure hypotheses and variables appear in the wrong order.

Robbert Krebbers authored

 11 Apr, 2016 5 commits


Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored

 10 Apr, 2016 1 commit


Robbert Krebbers authored

 09 Apr, 2016 1 commit


Robbert Krebbers authored

 08 Apr, 2016 3 commits


Robbert Krebbers authored
Since strip_later is doing a good job stripping laters in the conclusion, these tactics are thus no longer needed. Also, wp_finish now properly converts the result in a primitive viewshift in case it is not a weakestpre.

Robbert Krebbers authored
And introduce more useful variants with a wand.

Robbert Krebbers authored

 07 Apr, 2016 4 commits


Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored

 30 Mar, 2016 2 commits