 01 Nov, 2017 1 commit


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.

 28 Oct, 2017 2 commits


Robbert Krebbers authored

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

 27 Oct, 2017 1 commit


Robbert Krebbers authored

 26 Oct, 2017 2 commits


Robbert Krebbers authored

Robbert Krebbers authored

 25 Oct, 2017 4 commits


Robbert Krebbers authored
Replace/remove some occurences of `persistently` into `persistent` where the property instead of the modality is used.

Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored
I have reimplemented the tactic for introduction of ∀s/pures using type classes, which directly made it much more modular.

 05 Oct, 2017 1 commit


Robbert Krebbers authored

 06 Sep, 2017 1 commit


Robbert Krebbers authored

 28 Aug, 2017 1 commit


Robbert Krebbers authored
persistent context. Given the source does not contain a box:  Before: noop if there is a Persistent instance.  Now: noop in all cases.

 24 Aug, 2017 1 commit


Robbert Krebbers authored

 13 Apr, 2017 1 commit


Robbert Krebbers authored
This enables things like `iSpecialize ("H2" with "H1") in the below: "H1" : P □ "H2" : □ P ∗ Q ∗ R

 24 Mar, 2017 2 commits


Robbert Krebbers authored

Robbert Krebbers authored

 21 Mar, 2017 1 commit


Robbert Krebbers authored

 16 Mar, 2017 1 commit


Robbert Krebbers authored
This fixes issue #81.

 15 Mar, 2017 1 commit


Robbert Krebbers authored
 Allow framing of persistent hypotheses below the always modality.  Allow framing of persistent hypotheses in just one branch of a disjunction.

 14 Mar, 2017 1 commit


Robbert Krebbers authored
 Support for a `//` modifier to close the goal using `done`.  Support for framing in the `[#]` specialization pattern for persistent premises, i.e. `[# $H1 $H2]`  Add new "auto framing patterns" `[$]`, `[# $]` and `>[$]` that will try to solve the premise by framing. Hypothesis that are not framed are carried over to the next goal.

 21 Feb, 2017 1 commit


Robbert Krebbers authored
This fixes issue #72.

 12 Feb, 2017 1 commit


Robbert Krebbers authored
For example, when having `"H" : ∀ x : Z, P x`, using `iSpecialize ("H" $! (0:nat))` now works. We do this by first resolving the `IntoForall` type class, and then instantiating the quantifier.

 11 Feb, 2017 2 commits


Robbert Krebbers authored
Instead of doing all the instantiations by invoking a single type class search, it now performs the instantiations by invoking individual type class searches. This a.) gives better error messages and b.) works when `xj` depends on `xi`.

Robbert Krebbers authored
In the following ways:  When having `P → Q` it will now also work when the spatial context is nonempty.  When having `∀ x : A, Q` it will now do an `iIntros (_)`.

 06 Feb, 2017 1 commit


Ralf Jung authored

 27 Jan, 2017 1 commit


Ralf Jung authored

 22 Jan, 2017 1 commit


Robbert Krebbers authored
This fixes issue #62.

 05 Jan, 2017 1 commit


Ralf Jung authored

 03 Jan, 2017 1 commit


Ralf Jung authored
This patch was created using find name *.v  xargs L 1 awk i inplace '{from = 0} /^From/{ from = 1; ever_from = 1} { if (from == 0 && seen == 0 && ever_from == 1) { print "Set Default Proof Using \"Type*\"."; seen = 1 } }1 ' and some minor manual editing

 28 Dec, 2016 1 commit


Robbert Krebbers authored

 09 Dec, 2016 1 commit


Ralf Jung authored

 27 Nov, 2016 1 commit


Robbert Krebbers authored

 24 Nov, 2016 1 commit


JacquesHenri Jourdan authored
The idea on magic wand is to use it for curried lemmas and use ⊢ for uncurried lemmas.

 22 Nov, 2016 2 commits
 21 Nov, 2016 1 commit


Robbert Krebbers authored
The old name didn't make much sense. Also now we can have pure_False too.

 20 Nov, 2016 1 commit


Robbert Krebbers authored

 10 Nov, 2016 1 commit


Robbert Krebbers authored
This way we avoid the env_cbv tactic unfolding string related stuff that appears in the goal and hypotheses of the proof mode.

 03 Nov, 2016 1 commit


Robbert Krebbers authored
The old choice for ★ was a arbitrary: the precedence of the ASCII asterisk * was fixed at a wrong level in Coq, so we had to pick another symbol. The ★ was a random choice from a unicode chart. The new symbol ∗ (as proposed by David Swasey) corresponds better to conventional practise and matches the symbol we use on paper.
