Commits · 5fc07ae09f0af31db8ea7412d132d09d722feae6 · Simcha van Collem / Iris

Aug 07, 2017
- Broken exist_mono' · 5fc07ae0
  Jacques-Henri Jourdan authored 7 years ago
  
  5fc07ae0
- pure_flip_mono · 2dc55133
  Jacques-Henri Jourdan authored 7 years ago
  
  2dc55133
- Add instances to boxes. · 873f2d0a
  Jacques-Henri Jourdan authored 7 years ago
  
  873f2d0a
- cofe -> ofe · 4ad619de
  Jacques-Henri Jourdan authored 7 years ago
  
  4ad619de
Aug 06, 2017
- Merge branch 'master' of gitlab.mpi-sws.org:FP/iris-coq · 010efcf2
  Jacques-Henri Jourdan authored 7 years ago
  
  010efcf2
- sig_equivI · 5657f5ca
  Jacques-Henri Jourdan authored 7 years ago
  
  5657f5ca
- Stronger delete_option_local_update · 42ecd0a6
  Jacques-Henri Jourdan authored 7 years ago
  
  42ecd0a6
Aug 04, 2017
- Better error message for iAlways. · 272535e4
  Robbert Krebbers authored 7 years ago
  
  272535e4
- Document elimination of spatial conjunctions. · 83184356
  Robbert Krebbers authored 7 years ago
  
  83184356
Jul 28, 2017
- Typo · 36f74ae4
  Jacques-Henri Jourdan authored 7 years ago
  
  36f74ae4
Jul 12, 2017
- Fix typo. · e1764691
  Robbert Krebbers authored 7 years ago
  
  e1764691
- Convert some tests to Texan triples. · 0abc7f0f
  Robbert Krebbers authored 7 years ago
  
  0abc7f0f
Jul 11, 2017
- update iris.sty · 752371c8
  Ralf Jung authored 7 years ago
  
  752371c8
Jun 27, 2017
- Curry saved_prop_agree. This fixes #90. · 398bae9d
  Robbert Krebbers authored 7 years ago
  
  398bae9d
- Bump std++. · af18cb32
  Robbert Krebbers authored 7 years ago
  
  af18cb32
Jun 13, 2017
- Remove `⌜φ⌝ ⊢ □ ⌜φ⌝` as a primitive rule, it can be derived. · 56321b0f
  Robbert Krebbers authored 7 years ago
  
  56321b0f
- Let always_idemp be the rule `□ □ P ⊣⊢ □ P` in both ways. · 381e8509
  Robbert Krebbers authored 7 years ago
  
  381e8509
- Remove primitive rule `□ (P ∧ Q) ⊢ □ (P ∗ Q)`. · f72ccbec
  Robbert Krebbers authored 7 years ago
  
  It can be derived, thanks to Ales for noticing!
  f72ccbec
Jun 12, 2017
- Lemmas for big_ops and unit. · 6d89cb87
  Robbert Krebbers authored 7 years ago
  
  6d89cb87
- Show that the fancy update can be encoded in terms of the view shift. · 5a291902
  Robbert Krebbers authored 7 years ago
  
  5a291902
- Add is_op_plus to make iCombine behave nicer for nat. · 6b68b171
  Robbert Krebbers authored 7 years ago
  
  6b68b171
Jun 08, 2017
- Merge FromOp and IntoOp into IsOp and perform some tweak the modes. · ab451b4b
  Robbert Krebbers authored 7 years ago
  
  ab451b4b
- More frac_auth stuff. · 39a5e48f
  Robbert Krebbers authored 7 years ago
  
  39a5e48f
- Notations and theory for `authR (optionUR (prodR fracR A))`. · 3cb9abac
  Robbert Krebbers authored 7 years ago
  
  3cb9abac
- Some step-indexed properties for CMRAs that were missing. · 64b1650c
  Robbert Krebbers authored 7 years ago
  
  64b1650c
- Params instances for auth. · 84227fa4
  Robbert Krebbers authored 7 years ago
  
  84227fa4
- FromOp and IntoOp instances for frac. · d7bf36da
  Robbert Krebbers authored 7 years ago
  
  d7bf36da
- Give from_op_op a lower precedence so that it is not picked by default · 3875c726
  Robbert Krebbers authored 7 years ago
  
  when using iCombine.
  3875c726
Jun 06, 2017
- Pretty printing boxes for heap_lang notations. · 5b0f855e
  Robbert Krebbers authored 7 years ago
  
  TODO: document this.
  5b0f855e
May 25, 2017
- Bump coq-stdpp. · 094bee3c
  Robbert Krebbers authored 7 years ago
  
  094bee3c
May 17, 2017
- Add test for iLöb. · bfe7dd4c
  Robbert Krebbers authored 7 years ago
  
  bfe7dd4c
May 12, 2017
- Oops, forgot that. · 646bfc85
  Robbert Krebbers authored 7 years ago
  
  646bfc85
- Have `iInduction x as ...` revert all proofmode hyps involving `x`. · a64bb337
  Robbert Krebbers authored 7 years ago
  
  a64bb337
- Always revert the whole spatial context for iInduction. · e98e4ccc
  Robbert Krebbers authored 7 years ago
  
  Otherwise, the tactic will fail subsequently. Besides, it was inconsistent w.r.t. the iLöb tactic, which was already doing this.
  e98e4ccc
- Prove (P -∗ Q) ⊣⊢ ∃ R, R ∗ □ (P ∗ R → Q) and dually for →. · 4f9deccf
  Robbert Krebbers authored 7 years ago
  
  4f9deccf
- Add a bunch of missing proof mode class instances for ◇. · 066ce7e2
  Robbert Krebbers authored 7 years ago
  
  066ce7e2
- Existentials distribute over ◇ in both ways when the type is inhabited. · 7626a698
  Robbert Krebbers authored 7 years ago
  
  7626a698
- keep building as many files as possible · 07cf3665
  Ralf Jung authored 7 years ago
  
  07cf3665
May 09, 2017
- No longer CPS iElaborateSelPat, there is no point to that. · 7127e553
  Robbert Krebbers authored 7 years ago
  
  7127e553
Apr 27, 2017
- Generalize clear/frame patterns in introduction patterns. · 4084c886
  Robbert Krebbers authored 7 years ago
  
  Now they can also be used to clear/frame the whole pure/persistent/spatial context.
  4084c886