 04 Aug, 2017 1 commit


Robbert Krebbers authored

 27 Apr, 2017 1 commit


Robbert Krebbers authored
Now they can also be used to clear/frame the whole pure/persistent/spatial context.

 28 Mar, 2017 1 commit


Robbert Krebbers authored

 16 Mar, 2017 3 commits


Robbert Krebbers authored
This fixes issue #81.

Dan Frumin authored

Dan Frumin authored

 14 Mar, 2017 3 commits


Robbert Krebbers authored

Robbert Krebbers authored

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.

 07 Mar, 2017 1 commit


Robbert Krebbers authored

 17 Feb, 2017 1 commit


Robbert Krebbers authored

 24 Jan, 2017 1 commit


Robbert Krebbers authored

 23 Jan, 2017 4 commits


Ralf Jung authored

Robbert Krebbers authored

Ralf Jung authored

Robbert Krebbers authored

 04 Jan, 2017 1 commit


Robbert Krebbers authored
Thanks to Janno for spotting this!

 28 Dec, 2016 1 commit


Robbert Krebbers authored

 30 Nov, 2016 1 commit


Robbert Krebbers authored

 27 Nov, 2016 1 commit


Robbert Krebbers authored

 27 Oct, 2016 1 commit


Robbert Krebbers authored

 25 Oct, 2016 2 commits


Robbert Krebbers authored
There are now two proof mode tactics for dealing with modalities:  `iModIntro` : introduction of a modality  `iMod pm_trm as (x1 ... xn) "ipat"` : eliminate a modality The behavior of these tactics can be controlled by instances of the `IntroModal` and `ElimModal` type class. We have declared instances for later, except 0, basic updates and fancy updates. The tactic `iMod` is flexible enough that it can also eliminate an updates around a weakest pre, and so forth. The corresponding introduction patterns of these tactics are `!>` and `>`. These tactics replace the tactics `iUpdIntro`, `iUpd` and `iTimeless`. Source of backwards incompatability: the introduction pattern `!>` is used for introduction of arbitrary modalities. It used to introduce laters by stripping of a later of each hypotheses.

Robbert Krebbers authored
And also rename the corresponding proof mode tactics.

 04 Oct, 2016 2 commits


Robbert Krebbers authored

Robbert Krebbers authored

 27 Sep, 2016 3 commits


Robbert Krebbers authored
Used in iRevert, iClear, iFrame, and for generalizing the IH in iInduction and iLöb.

Robbert Krebbers authored

Robbert Krebbers authored
As proposed by JH Jourdan in issue 34.

 20 Sep, 2016 4 commits


Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored
Before, it failed when these tactics were invoked with persistent hypotheses. The new behavior is more convenient when using these tactics to build other tactics.

Robbert Krebbers authored

 19 Sep, 2016 1 commit


Robbert Krebbers authored
This closes issue 32.

 09 Sep, 2016 2 commits


Robbert Krebbers authored

Robbert Krebbers authored
Before this commit, given "HP" : P and "H" : P ★ Q with Q persistent, one could write: iSpecialize ("H" with "#HP") to eliminate the wand in "H" while keeping the resource "HP". The lemma: own_valid : own γ x ⊢ ✓ x was the prototypical example where this pattern (using the #) was used. However, the pattern was too limited. For example, given "H" : P₁ ★ P₂ ★ Q", one could not write iSpecialize ("H" with "#HP₁") because P₂ ★ Q is not persistent, even when Q is. So, instead, this commit introduces the following tactic: iSpecialize pm_trm as # which allows one to eliminate implications and wands while being able to use all hypotheses to prove the premises, as well as being able to use all hypotheses to prove the resulting goal. In the case of iDestruct, we now check whether all branches of the introduction pattern start with an `#` (moving the hypothesis to the persistent context) or `%` (moving the hypothesis to the pure Coq context). If this is the case, we allow one to use all hypotheses for proving the premises, as well as for proving the resulting goal.

 05 Aug, 2016 1 commit


Robbert Krebbers authored
Also make those for introduction and elimination more symmetric: !% pure introduction % pure elimination !# always introduction # always elimination !> later introduction > pat timeless later elimination !==> view shift introduction ==> pat view shift elimination

 02 Aug, 2016 2 commits


Robbert Krebbers authored

Robbert Krebbers authored

 01 Aug, 2016 2 commits


Robbert Krebbers authored

Robbert Krebbers authored
This makes clear that we do not range over Coq terms.
