Commits · ci/joe/compact_ipm · Dmitry Khalanskiy / Iris

19 May, 2019 23 commits
- Fix build on Coq master. · 10fe1509
  Joseph Tassarotti authored May 19, 2019
  
  10fe1509
- Revert "Remove redundant pm_reduce." and "Commute match with implication in tac_frame." · 778291fc
  Joseph Tassarotti authored Apr 30, 2019
```
This reverts commits 6d0b75b9068fd26619e94da4dca9b3a99e612306 and
2aea3d477808334fd945ea8407735be82dad0a03.
```
  778291fc
- Remove redundant pm_reduce. · a2863643
  Joseph Tassarotti authored Apr 30, 2019
  
  a2863643
- Commute match with implication in tac_frame. · de815b00
  Joseph Tassarotti authored Apr 30, 2019
  
  de815b00
- Convert other tac_specialize* to avoid nested conjunctions. · db75174d
  Joseph Tassarotti authored Apr 29, 2019
  
  db75174d
- Switch back to notypeclasses refine on tac_specialize* · a742db33
  Joseph Tassarotti authored Apr 29, 2019
  
  a742db33
- Remove unneeded pm_reduce. · 3a95a638
  Joseph Tassarotti authored Apr 29, 2019
  
  3a95a638
- Swap implication with match in some of tac_specialize*. · 4913936f
  Joseph Tassarotti authored Apr 29, 2019
```
By commuting implication with match, we can avoid using deeply nested
conjunctions in these tactics, which may cause them to be faster.
```
  4913936f
- Try to improve performance of converted tac_specialize_* · 5f505004
  Joseph Tassarotti authored Apr 26, 2019
  
  5f505004
- Convert remaining tac_specialize_* lemmas. · 38293588
  Joseph Tassarotti authored Apr 26, 2019
  
  38293588
- Convert tac_specialize frame. · ad375980
  Joseph Tassarotti authored Apr 26, 2019
  
  ad375980
- Convert tac_specialize_assert. · 30cad5e9
  Joseph Tassarotti authored Apr 26, 2019
  
  30cad5e9
- Convert tac_specialize. · ce9a249e
  Joseph Tassarotti authored Apr 25, 2019
  
  ce9a249e
- Convert remaining simple tactics. · 162672ed
  Joseph Tassarotti authored Apr 25, 2019
  
  162672ed
- Convert additional tactics to shrink proof term. · 4f3dd452
  Joseph Tassarotti authored Apr 25, 2019
  
  4f3dd452
- Convert tac_assumption. · 5ba97f02
  Joseph Tassarotti authored Apr 25, 2019
  
  5ba97f02
- Update tac_forall_specialize to not embed the context twice. · 78f4db43
  Joseph Tassarotti authored Mar 14, 2019
  
  78f4db43
- Another attempt to improve tac_frame. · c30bd92f
  Joseph Tassarotti authored Mar 13, 2019
  
  c30bd92f
- Try to make the iFrame change faster. · 68dea1df
  Joseph Tassarotti authored Mar 13, 2019
  
  68dea1df
- Convert tac_frame to not duplicate contexts. · 1a262af5
  Joseph Tassarotti authored Mar 13, 2019
  
  1a262af5
- Convert remaining tac_ lemmas to not duplicate context (where straightforward) · 4e7c9fd3
  Joseph Tassarotti authored Mar 13, 2019
  
  4e7c9fd3
- Convert more tac_ lemmas to not duplicate the context. · 7c061c61
  Joseph Tassarotti authored Mar 12, 2019
  
  7c061c61
- Delete extra copies of context from terms for some proof mode tactics. · f9dd26a5
  Joseph Tassarotti authored Mar 12, 2019
  
  f9dd26a5
30 Apr, 2019 1 commit
- Bump stdpp. · cdc564bf
  Robbert Krebbers authored Apr 30, 2019
  
  cdc564bf
29 Apr, 2019 5 commits
- Rename misspelled `IAnom` into `IFresh` (`IAnon` is already in use). · c98c721b
  Robbert Krebbers authored Apr 29, 2019
  
  c98c721b
- Merge branch 'master' of gitlab.mpi-sws.org:iris/iris · 91dfd8b9
  Ralf Jung authored Apr 29, 2019
  
  91dfd8b9
- editing · ccf8bc36
  Ralf Jung authored Apr 29, 2019
  
  ccf8bc36
- Merge branch 'master-ofe_fun-doc' into 'master' · 195d3beb
  Robbert Krebbers authored Apr 29, 2019
```
Fix documentation for ofe_funR

See merge request iris/iris!236
```
  195d3beb
- Fix documentation for ofe_funR · f25d9024
  Paolo G. Giarrusso authored Apr 29, 2019
```
This comment wasn't updated after
866cad62.
```
  f25d9024
27 Apr, 2019 3 commits
- Merge branch 'ci/janno/reduction_no_check' into 'master' · 470c73cf
  Robbert Krebbers authored Apr 27, 2019
```
Avoid conversion after only reducing goal.

See merge request iris/iris!235
```
  470c73cf
- Add comments. · 46e7af84
  Robbert Krebbers authored Apr 27, 2019
  
  46e7af84
- Avoid conversion after only reducing goal. · 1595e35f
  Janno authored Apr 02, 2019
  
  1595e35f
26 Apr, 2019 2 commits
- Bump stdpp. · d5b0ff9a
  Robbert Krebbers authored Apr 26, 2019
  
  d5b0ff9a
- Bump stdpp. · 8271701f
  Robbert Krebbers authored Apr 26, 2019
  
  8271701f
25 Apr, 2019 2 commits
- More type annotations for https://github.com/coq/coq/pull/9996 . · a9031f7f
  Robbert Krebbers authored Apr 25, 2019
  
  a9031f7f
- Bump std++. Use `binder` library from stdpp. · 3a0ab5e6
  Robbert Krebbers authored Apr 25, 2019
  
  3a0ab5e6
24 Apr, 2019 2 commits
- Make use of new `SetUnfoldElemOf`. · d2f8b689
  Robbert Krebbers authored Apr 23, 2019
  
  d2f8b689
- bump std++ · c3733dd1
  Ralf Jung authored Apr 24, 2019
  
  c3733dd1
23 Apr, 2019 1 commit
- Update example in ProofMode.md · 3f7f9f4e
  Robbert Krebbers authored Apr 23, 2019
  
  3f7f9f4e
17 Apr, 2019 1 commit
- Sketch proof · e85a1027
  Paolo G. Giarrusso authored Apr 17, 2019
  
  e85a1027