Commits · 95d4a3edeed797ed5912a3a6f2479ecb36515cce · Paolo G. Giarrusso / iris

Nov 28, 2016
- Use the correct setoid equality in algebra/gset and algebra/coPset. · 95d4a3ed
  Robbert Krebbers authored 8 years ago
  
  This fixes issue #46.
  95d4a3ed
- Some nits. · 230b2a6b
  Robbert Krebbers authored 8 years ago
  
  230b2a6b
- Add a local update for auth (needed for nested auth) · 692b8570
  Ralf Jung authored 8 years ago
  
  Proof was done by Hai & me
  692b8570
Nov 27, 2016
- Better error messages for iRevert. · 1bc26dc9
  Robbert Krebbers authored 8 years ago
  
  This fixes issue #44.
  1bc26dc9
- README: add instructions for how to get fixed ssreflect version · e4d5fc87
  Ralf Jung authored 8 years ago
  
  e4d5fc87
- fix the reference to the bullet fix in ssreflect · 6d7d2973
  Ralf Jung authored 8 years ago
  
  6d7d2973
- Generalize boxes to have a version both with and without laters. · f1aa22f6
  Robbert Krebbers authored 8 years ago
  
  f1aa22f6
- Generalize iNext to support multiple and iterated laters. · 86315b42
  Robbert Krebbers authored 8 years ago
  
  86315b42
- Big ops distribute over and. · 4daa00cb
  Robbert Krebbers authored 8 years ago
  
  4daa00cb
- Iterated later modality. · aca09e1e
  Robbert Krebbers authored 8 years ago
  
  aca09e1e
- Fix some typos in comments. · 032879e0
  Robbert Krebbers authored 8 years ago
  
  032879e0
Nov 26, 2016
- Fix issue #45. · b62bb39a
  Robbert Krebbers authored 8 years ago
  
  b62bb39a
- Add .crashcoqide to .gitignore. · 763bfe4f
  Robbert Krebbers authored 8 years ago
  
  763bfe4f
Nov 25, 2016
- More IntoX and FromX proofmode instances. · 4a934341
  Robbert Krebbers authored 8 years ago
  
  4a934341
- make the C-scope magic wand printing · 5c3ad2f9
  Ralf Jung authored 8 years ago
  
  5c3ad2f9
- update CHANGELOG · add4702b
  Ralf Jung authored 8 years ago
  
  add4702b
- list-based agreement · 29c097c6
  Ralf Jung authored 8 years ago
  
  29c097c6
- Some box/slice renaming. · e1ef66ef
  Robbert Krebbers authored 8 years ago
  
  e1ef66ef
- Make auth_frag_op a Leibniz equality. · 6923de66
  Robbert Krebbers authored 8 years ago
  
  6923de66
- Stronger splitting rule for boxes. · 42cf780a
  Jacques-Henri Jourdan authored 8 years ago
  
  42cf780a
- Make iLeft and iRight work with always. · 26ae0c67
  Robbert Krebbers authored 8 years ago
  
  26ae0c67
- Make iLeft and iRight work with later. · 37f022e4
  Robbert Krebbers authored 8 years ago
  
  37f022e4
- Tweak boxes. · f2bf449c
  Robbert Krebbers authored 8 years ago
  
  No longer `put box_own_prop γ P` in the invariant, it is persistent.
  f2bf449c
- Splitting and combining boxes. Also refactored boxes by currying things. · 513b8d85
  Jacques-Henri Jourdan authored 8 years ago
  
  513b8d85
Nov 24, 2016
- Next time I will think about committing something that works... · ff96075a
  Jacques-Henri Jourdan authored 8 years ago
  
  ff96075a
- Merge branch 'master' of https://gitlab.mpi-sws.org/FP/iris-coq · dc432a1f
  Jacques-Henri Jourdan authored 8 years ago
  
  dc432a1f
- Delete full slices. · e575e40d
  Jacques-Henri Jourdan authored 8 years ago
  
  e575e40d
- Merge branch 'master' of https://gitlab.mpi-sws.org/FP/iris-coq · 5eeb0c67
  Ralf Jung authored 8 years ago
  
  5eeb0c67
- compat with older opam · a0e013f5
  Ralf Jung authored 8 years ago
  
  a0e013f5
- Boxes : insert full slices. · 2f15e108
  Jacques-Henri Jourdan authored 8 years ago
  
  2f15e108
- Accessor like lemmas for big ops. · 020acf84
  Robbert Krebbers authored 8 years ago
  
  020acf84
- More multiset stuff. · 85e9d0d5
  Robbert Krebbers authored 8 years ago
  
  85e9d0d5
- Enable solve_ndisj to handle E1 ∖ ↑N1 ⊆ E2 ∖ ↑N2 ∖ .. ∖ ↑Nn. · 3b800620
  Robbert Krebbers authored 8 years ago
  
  3b800620
- Validity coercion from iProp to Prop. Magic wand that works at the Prop level. · 243fdd13
  Jacques-Henri Jourdan authored 8 years ago
  
  The idea on magic wand is to use it for curried lemmas and use ⊢ for uncurried lemmas.
  243fdd13
- Merge branch 'ralf/underscore' into 'master' · c1951443
  Robbert Krebbers authored 8 years ago
  
  ProofMode intro patterns: accept _ as part of variable names @robbertkrebbers beat this. ;) See merge request !29
  c1951443
- ProofMode intro patterns: accept _ as part of variable names · 8239ab05
  Ralf Jung authored 8 years ago
  
  8239ab05
Nov 23, 2016
- opam: rename to coq-iris · d0743f7e
  Ralf Jung authored 8 years ago
  
  d0743f7e
- opam: build in parallel · 55ee8e66
  Ralf Jung authored 8 years ago
  
  55ee8e66
- start experimenting with opam · 4027fedc
  Ralf Jung authored 8 years ago
  
  4027fedc
- Fix typo. · 36c5a842
  Robbert Krebbers authored 8 years ago
  
  36c5a842