Commits · 84c43a1276ba19a8829aade6541bc93aaff4db44 · Michael Sammler / iris-coq

Aug 13, 2019
- Attempt at fixing compilation with Coq 8.7.2. · 77ed4519
  Robbert Krebbers authored 5 years ago
  
  77ed4519
- Fix issue #260. · 890b60e5
  Robbert Krebbers authored 5 years ago
  
  890b60e5
- Improve error message of `iRevert` in case of used variable. · 9c43011e
  Robbert Krebbers authored 5 years ago
  
  9c43011e
- Factor out anonymous rec in `iRevertIntros` to get cleaner Ltac backtraces. · 9a93c850
  Robbert Krebbers authored 5 years ago
  
  9a93c850
- Fix issue #259 . · b0c4d25c
  Robbert Krebbers authored 5 years ago
  
  Based on @Blaisorblade's suggestion.
  b0c4d25c
Jul 01, 2019
- Make `iPure` non-local so it can be used for defining custom `iDestruct`-like tactics. · 1ee1d9f9
  Robbert Krebbers authored 5 years ago
  
  1ee1d9f9
Jun 28, 2019
- Up to 15 binders for `iRevert`, `iRevertIntros`, `iInduction` and `iLöb`! · 82bd1095
  Robbert Krebbers authored 5 years ago
  
  This commit made me cry...
  82bd1095
- Up to 14 binders for `iRevert`, `iRevertIntros`, `iInduction` and `iLöb`! · 8dc59df2
  Robbert Krebbers authored 5 years ago
  
  8dc59df2
Jun 27, 2019
- Up to 12 binders for `iRevert`, `iRevertIntros`, `iInduction` and `iLöb`. · d5c0458f
  Robbert Krebbers authored 5 years ago
  
  Created this commit with pain in my heart!
  d5c0458f
Jun 21, 2019
- Have `iNext` turn `Next x ≡ Next y` into `x ≡ y`. · ee8815c0
  Robbert Krebbers authored 5 years ago
  
  ee8815c0
Jun 18, 2019

Explicitly thunk tactic argument of `iPoseProofCoreLem`. · 3147b08a

This avoids weird Ltac behaviors like those in !272.

Also, change `before_tc` keyword into `as` to be consistent with other tactics.

3147b08a

Jun 17, 2019
- Drop lazy_tc argument · 7b9d27ea
  Paolo G. Giarrusso authored 5 years ago
  
  7b9d27ea
Jun 16, 2019
- ltac_tactics.v: drop dead branch · 160b8c97
  Paolo G. Giarrusso authored 5 years ago
  
  160b8c97
Jun 15, 2019
- tactic->tactic3 for remaining tactics · cec53bd4
  Paolo G. Giarrusso authored 5 years ago
  
  cec53bd4
- tactic->tactic3 for user-facing tactics · c9418149
  Paolo G. Giarrusso authored 5 years ago
  
  c9418149
- Fix inconsistent invocation of iPoseProofCoreLem · 1f3e92e3
  Paolo G. Giarrusso authored 5 years ago
  
  The parens are inconsistent with the other call to `iPoseProofCoreLem`, and this will break after switching to tactic3.
  1f3e92e3
- Fix parsing precedence for iEval · e47c73d8
  Paolo G. Giarrusso authored 5 years ago
  
  e47c73d8
Jun 12, 2019
- `IntoSep` instance for `tc_opaque`. · ae1dd418
  Robbert Krebbers authored 5 years ago
  
  ae1dd418
- Coqdoc tweaks. · 52baecf8
  Robbert Krebbers authored 5 years ago
  
  52baecf8
Jun 09, 2019
- Fix regression with iSpecialize errors. · 6a468eca
  Joseph Tassarotti authored 5 years ago
  
  6a468eca
- Fix error messages for iSplitL/iSplitR. · eb74aeab
  Joseph Tassarotti authored 5 years ago
  
  eb74aeab
Jun 06, 2019
- Fix issue w.r.t. overly eager TC resolution introduced in !254. · ec161a20
  Robbert Krebbers authored 5 years ago
  
  ec161a20
Jun 05, 2019
- Port `tac_specialize_assert`. · 00bfe453
  Robbert Krebbers authored 5 years ago
  
  00bfe453
- Port `tac_specialize`. · 1cb1dd6f
  Robbert Krebbers authored 5 years ago
  
  1cb1dd6f
- Port `tac_assumption`. · 911412f9
  Robbert Krebbers authored 5 years ago
  
  911412f9
- Alternative take on making proof mode terms more compact. · 1945565f
  Robbert Krebbers authored 5 years ago
  
  This is an alternative to !224.
  1945565f
May 24, 2019
- More simple changes to make proof mode terms more compact. · 7ba11ac0
  Robbert Krebbers authored 5 years ago
  
  This is a follow up of !248.
  7ba11ac0
- Allow up to 10 introduction patterns for iInv. · d23e8b0a
  Rodolphe Lepigre authored 5 years ago
  
  d23e8b0a
- Fix error message regression, add new test cases. · ded831d3
  Joseph Tassarotti authored 5 years ago and Robbert Krebbers committed 5 years ago
  
  Also fixes pre-existing bug in iCombine error messages.
  ded831d3
May 19, 2019
- Try to fix compilation with Coq 8.7.*. · c6c5de47
  Robbert Krebbers authored 5 years ago
  
  c6c5de47
- Update documentation of [iFresh] and make sure it returns the old counter. · fa61a3c0
  Robbert Krebbers authored 5 years ago
  
  fa61a3c0
- Make `iFresh` faster by ensuring no evidence appears in the proof term. · 8d24e722
  Robbert Krebbers authored 5 years ago
  
  8d24e722
May 07, 2019
- Improve comment a bit. · 4c341601
  Robbert Krebbers authored 5 years ago
  
  4c341601
May 06, 2019
- Generalize `iPureIntro` to support non-empty spatial contexts with just affine hypotheses. · 1a14cdd3
  Robbert Krebbers authored 5 years ago
  
  1a14cdd3
May 02, 2019
- Conditional `<absorb>?p P` modality. · 887fcf1e
  Robbert Krebbers authored 5 years ago
  
  887fcf1e
May 01, 2019
- Make the argument to `iEval` a selection pattern. · a7fe86a3
  Dan Frumin authored 5 years ago
  
  a7fe86a3
- Allow multiple arguments in `iEval .. in` and `iSimpl in`. · 46151cd2
  Dan Frumin authored 5 years ago
  
  46151cd2
Apr 29, 2019
- Rename misspelled `IAnom` into `IFresh` (`IAnon` is already in use). · c98c721b
  Robbert Krebbers authored 5 years ago
  
  c98c721b
Apr 27, 2019
- Add comments. · 46e7af84
  Robbert Krebbers authored 5 years ago
  
  46e7af84
- Avoid conversion after only reducing goal. · 1595e35f
  Janno authored 5 years ago
  
  1595e35f