 05 Nov, 2017 1 commit


Robbert Krebbers authored

 04 Nov, 2017 3 commits


Robbert Krebbers authored

Robbert authored
Make atomic a type class. See merge request FP/iriscoq!78

Robbert Krebbers authored

 03 Nov, 2017 2 commits


Ralf Jung authored

Robbert Krebbers authored

 02 Nov, 2017 3 commits


Robbert Krebbers authored

Robbert Krebbers authored
Thanks to Amin Timany for an initial version of the proof.

Robbert authored
Make proofnode notation more robust in the context of import order See merge request FP/iriscoq!75

 01 Nov, 2017 5 commits


Robbert Krebbers authored
This solves issue #100: the proof mode notation is sometimes not printed. As Ralf discovered, the problem is that there are two overlapping notations: ```coq Notation "P ⊢ Q" := (uPred_entails P Q). ``` And the "proof mode" notation: ``` Notation "Γ '' □ Δ '' ∗ Q" := (of_envs (Envs Γ Δ) ⊢ Q%I). ``` These two notations overlap, so, when having a "proof mode" goal of the shape `of_envs (Envs Γ Δ) ⊢ Q%I`, how do we know which notation is Coq going to pick for pretty printing this goal? As we have seen, this choice depends on the import order (since both notations appear in different files), and as such, Coq sometimes (unintendedly) uses the first notation instead of the latter. The idea of this commit is to wrap `of_envs (Envs Γ Δ) ⊢ Q%I` into a definition so that there is no ambiguity for the pretty printer anymore.

Robbert Krebbers authored

Robbert Krebbers authored
This class, in combination with `TCForall`, turns out the useful in LambdaRust to express that lists of expressions are values.

Robbert Krebbers authored

Robbert Krebbers authored

 30 Oct, 2017 1 commit


Robbert Krebbers authored

 29 Oct, 2017 7 commits


Robbert authored
Rules for fancy updates and plain propositions. Closes #105 See merge request FP/iriscoq!74

Robbert Krebbers authored
This commit is based on code by Amin Timany.

Ralf Jung authored

Ralf Jung authored
add a strong form of atomicity, for weak forms of weakestpre Closes #107 See merge request FP/iriscoq!77

Ralf Jung authored

Ralf Jung authored

Ralf Jung authored

 28 Oct, 2017 18 commits


Robbert Krebbers authored

Robbert Krebbers authored
This way, it can be used with `iApply`.

JacquesHenri Jourdan authored
Notation for disjointness: replace ⊥ with ##, so that ⊥ can be used for bottom. See merge request FP/iriscoq!73

JacquesHenri Jourdan authored
This is to be used on top of stdpp's 4b5d254e.

Ralf Jung authored

Ralf Jung authored

Ralf Jung authored

Ralf Jung authored

Ralf Jung authored

Ralf Jung authored

Ralf Jung authored

Robbert Krebbers authored
Instead, as Ralf suggested, just comment the test out.

Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored

Ralf Jung authored

Ralf Jung authored

Robbert Krebbers authored
