Commits · 8d6285407e6c3088f8b5719e9fc7bdd40cd66e39 · Tej Chajed / iris · GitLab

Snippets Groups Projects

Feb 19, 2018
- Remove useless new line. · 8d628540
  Robbert Krebbers authored 7 years ago
  
  8d628540
Feb 18, 2018
- Fix typo. · ddd48268
  Jacques-Henri Jourdan authored 7 years ago
  
  ddd48268
- Merge branch 'gen_proofmode' of https://gitlab.mpi-sws.org/FP/iris-coq into gen_proofmode · 75c98fae
  Ralf Jung authored 7 years ago
  
  75c98fae
- atomic shift: quantify over mask to make it easier to apply; prove an ellimination lemma · 020ad55d
  Ralf Jung authored 7 years ago
  
  020ad55d
- Fix error message of `iMod` · 753de83e
  Robbert Krebbers authored 7 years ago
  
  Thanks to @jtassaro for reporting this problem.
  753de83e
Feb 16, 2018
- Add first definition of (logically) atomic shifts and triples · 2850f888
  Ralf Jung authored 7 years ago
  
  2850f888
- README: where to go for Coq 8.6 compatibility · 26fdda7a
  Ralf Jung authored 7 years ago
  
  26fdda7a
- update dependencies in README · 3cf386d0
  Ralf Jung authored 7 years ago
  
  3cf386d0
Feb 15, 2018
- iIntoValid : for specialization, first try with [hnf] and then with [cbv zeta]. · 80fcebca
  Jacques-Henri Jourdan authored 7 years ago
  
  80fcebca
- Add comment. · 7479b01b
  Jacques-Henri Jourdan authored 7 years ago
  
  7479b01b
- Add back cbv zeta in iIntoValid. · f3033b7d
  Jacques-Henri Jourdan authored 7 years ago
  
  f3033b7d
- move fractional.v to new lib/ folder · c1be91f7
  Ralf Jung authored 7 years ago
  
  c1be91f7
- Merge branch 'gen_proofmode' of gitlab.mpi-sws.org:FP/iris-coq into gen_proofmode · a0ac556c
  Jacques-Henri Jourdan authored 7 years ago
  
  a0ac556c
- Make iPureIntro able to introduce [bi_affinely (bi_pure P)] when the context is empty. · 36654e76
  Jacques-Henri Jourdan authored 7 years ago
  
  36654e76
- fix opam publishing · 8ffd6918
  Ralf Jung authored 7 years ago
  
  8ffd6918
- Also remove the [cbv zeta]. · c6c87884
  Jacques-Henri Jourdan authored 7 years ago
  
  c6c87884
- Do not call [eval hnf] in iIntoValid. · 1560d168
  Jacques-Henri Jourdan authored 7 years ago
  
  1560d168
- update CI · 96ab3ac7
  Ralf Jung authored 7 years ago
  
  96ab3ac7
Feb 14, 2018
- monpred: note that notation is somewhat broken · d870e5cf
  Ralf Jung authored 7 years ago
  
  d870e5cf
- make BUpdFacts depend on SBI · 4b43fcc2
  Ralf Jung authored 7 years ago
  
  4b43fcc2
- Fix build. · 98d8373b
  Jacques-Henri Jourdan authored 7 years ago
  
  98d8373b
- Attempt at fixing #146 definitively by having better types for update properties. · d51217e4
  Jacques-Henri Jourdan authored 7 years ago
  
  Assertions should have type sbi_car PROP and not bi_car (sbi_bi PROP).
  d51217e4
- Merge branch 'gen_proofmode' of gitlab.mpi-sws.org:FP/iris-coq into gen_proofmode · cfca4b37
  Jacques-Henri Jourdan authored 7 years ago
  
  cfca4b37
- Remove Admitted. · 850e6c3c
  Jacques-Henri Jourdan authored 7 years ago
  
  850e6c3c
- Merge branch 'gen_proofmode' of https://gitlab.mpi-sws.org/FP/iris-coq into gen_proofmode · f083acae
  Ralf Jung authored 7 years ago
  
  f083acae
- avoid type ascription · e31f8034
  Ralf Jung authored 7 years ago
  
  e31f8034
- Add test for #146. · 4cd7ccda
  Jacques-Henri Jourdan authored 7 years ago
  
  4cd7ccda
- consistent non-parentheses for Implicit Types · dbb44a40
  Ralf Jung authored 7 years ago
  
  dbb44a40
- explain why we use typeclasses eauto · 2abfa296
  Ralf Jung authored 7 years ago
  
  2abfa296
Feb 13, 2018
- set modes for update modality typeclasses · 74e4d637
  Ralf Jung authored 7 years ago
  
  74e4d637
- solve AsValid without solving all the other evars first · 768be4ca
  Ralf Jung authored 7 years ago
  
  768be4ca
- Fix build by using envs_entails everywhere and by not breaking this abstraction in tactics. · 5e1597b7
  Jacques-Henri Jourdan authored 7 years ago
  
  5e1597b7
- Opaque is not enough. Let's seal envs_entails. · 45a2b465
  Jacques-Henri Jourdan authored 7 years ago
  
  45a2b465
- Make envs_entails opaque. · 957d5fcf
  Jacques-Henri Jourdan authored 7 years ago
  
  957d5fcf
- Fix doc. · b2426163
  Jacques-Henri Jourdan authored 7 years ago
  
  b2426163
- Wrong kind of comment. · 58a49c2a
  Jacques-Henri Jourdan authored 7 years ago
  
  58a49c2a
- Merge branch 'jh/affine_frompure' into 'gen_proofmode' · 411142ee
  Jacques-Henri Jourdan authored 7 years ago
  
  Make `FromPure` depend on an affinity parameter See merge request FP/iris-coq!114
  411142ee
- More doc about FromPure. · 418f57db
  Jacques-Henri Jourdan authored 7 years ago
  
  418f57db
- Merge branch 'robbert/issue_154' into 'gen_proofmode' · cf44ca8b
  Ralf Jung authored 7 years ago
  
  Bring back side-conditionals for `iMod` See merge request FP/iris-coq!113
  cf44ca8b
Feb 12, 2018
- Make FromPure depend on an affinity parameter. · 6a086fc6
  Jacques-Henri Jourdan authored 7 years ago
  
  6a086fc6