 05 Dec, 2017 4 commits


Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored

 04 Dec, 2017 2 commits


Robbert Krebbers authored

Robbert Krebbers authored

 30 Nov, 2017 6 commits


Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored

 24 Nov, 2017 3 commits


Robbert Krebbers authored

Robbert Krebbers authored

Ralf Jung authored

 23 Nov, 2017 1 commit


Robbert Krebbers authored

 21 Nov, 2017 1 commit


Ralf Jung authored

 14 Nov, 2017 1 commit


Robbert Krebbers authored
This is an old flag set by the ssr plugin, and recently unset in coqstdpp, see https://gitlab.mpisws.org/robbertkrebbers/coqstdpp/issues/5.

 13 Nov, 2017 1 commit


Robbert Krebbers authored

 09 Nov, 2017 3 commits


David Swasey authored
I saw no need for `stuckness_flip`: strong atomicity always works, while weak atomicity works only for expressions that are not stuck. Since this seemed unclear, I split lemma `wp_atomic'` up into `wp_strong_atomic` (parametric in the WP's `s`) and `wp_weak_atomic` (not). The proof mode instance is stated in terms of the derived rule `wp_atomic` (parametric in `s`).

David Swasey authored
 08 Nov, 2017 4 commits


David Swasey authored

David Swasey authored

David Swasey authored

David Swasey authored

 07 Nov, 2017 1 commit


Ralf Jung authored

 05 Nov, 2017 1 commit


Robbert Krebbers authored

 04 Nov, 2017 3 commits


Ralf Jung authored

Robbert Krebbers authored

Robbert Krebbers authored

 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

 26 Oct, 2017 1 commit


Robbert Krebbers authored
Coq also uses level 200 for these constructs. Besides, heap_lang's match and if were also already at this level.

 25 Oct, 2017 2 commits


Robbert Krebbers authored

Robbert Krebbers authored
The advantage is that we can directly use a Coq introduction pattern `cpat` to perform actions to the pure assertion. Before, this had to be done in several steps: iDestruct ... as "[Htmp ...]"; iDestruct "Htmp" as %cpat. That is, one had to introduce a temporary name. I expect this to be quite useful in various developments as many of e.g. our invariants are written as: ∃ x1 .. x2, ⌜ pure stuff ⌝ ∗ spacial stuff.

 19 Oct, 2017 1 commit


Ralf Jung authored
