Commits · 26fdda7a69b2b8b38ef16d1a42b574c5b10c64d0 · Abhishek Anand / Iris · GitLab

Snippets Groups Projects

Feb 16, 2018
- 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
- Revert "Make FromPure depend on an affinity parameter." · c54e1692
  Jacques-Henri Jourdan authored 7 years ago
  
  This reverts commit 78ba9509.
  c54e1692
- Make FromPure depend on an affinity parameter. · 78ba9509
  Jacques-Henri Jourdan authored 7 years ago
  
  78ba9509
- document the RA model briefly · f30188af
  Ralf Jung authored 7 years ago
  
  f30188af
- Restore side-condition of `iMod` tactic and `ElimModal` TC. · 10ce5481
  Robbert Krebbers authored 7 years ago
  
  This supports Iris 2 like update modalities, as used in e.g. by @jtassaro. This commit fixes issue #154.
  10ce5481
- Remove hacks that are no longer needed. · 3f992fb9
  Robbert Krebbers authored 7 years ago
  
  These were needed pre-a63f256e.
  3f992fb9
- Makefile: honor COQBIN · 7e816a90
  Ralf Jung authored 7 years ago
  
  7e816a90