- 04 Oct, 2016 1 commit
-
-
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 3 commits
-
-
Robbert Krebbers authored
-
Robbert Krebbers authored
This makes clear that we do not range over Coq terms.
-
Robbert Krebbers authored
-
- 13 Jul, 2016 1 commit
-
-
Robbert Krebbers authored
-
- 11 Jul, 2016 1 commit
-
-
Ralf Jung authored
-
- 05 Jul, 2016 5 commits
-
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
- 19 Apr, 2016 1 commit
-
-
Ralf Jung authored
-