Commits · 741c92b0a34815cc3eb9b219ab779ed798ca0069 · Pierre Roux / Iris

Oct 05, 2020
- CHANGELOG. · 741c92b0
  Robbert Krebbers authored 4 years ago
  
  741c92b0
- Factor out `inG_unfold_validN`. · 265a88d5
  Robbert Krebbers authored 4 years ago
  
  265a88d5
Oct 04, 2020
- Put isomorphism `iProp` to `iPreProp` into `own` construction. · fc6fdaa1
  Robbert Krebbers authored 4 years ago
  
  fc6fdaa1
- Add `valid_entails` to lift `✓{n}` entailments into `uPred`. · 646e26fa
  Robbert Krebbers authored 4 years ago
  
  646e26fa
- Add lemmas for updates on isomorphic cameras. · 3d73e1ff
  Robbert Krebbers authored 4 years ago
  
  3d73e1ff
- Add lemma `cmra_transport_trans`. · cbf81b65
  Robbert Krebbers authored 4 years ago
  
  cbf81b65
- Merge branch 'robbert/cmra_morphism_valid' into 'master' · a36f8a23
  Robbert Krebbers authored 4 years ago
  
  Rename `cmra_monotone_valid` into `cmra_morphism_valid` See merge request iris/iris!529
  a36f8a23
- CHANGELOG. · 8c7c1ba2
  Robbert Krebbers authored 4 years ago
  
  8c7c1ba2
- Rename `cmra_monotone_valid` into `cmra_morphism_valid`. · f2be3543
  Robbert Krebbers authored 4 years ago
  
  f2be3543
Oct 03, 2020
- `Set Default Proof Using` is not needed due to `options`. · f72ef909
  Robbert Krebbers authored 4 years ago
  
  f72ef909
- Merge branch 'discardable-fractions' into 'master' · 4dcc0a1a
  Robbert Krebbers authored 4 years ago
  
  Add discardable fractions camera See merge request iris/iris!497
  4dcc0a1a
- Add dfrac · 7ff11e39
  Simon Friis Vindum authored 4 years ago
  
  7ff11e39
- Merge branch 'ralf/auth-changelog' into 'master' · c6c7acf7
  Ralf Jung authored 4 years ago
  
  expand auth changelog Closes #353 See merge request iris/iris!528
  c6c7acf7
- expand auth changelog · b059329d
  Ralf Jung authored 4 years ago
  
  b059329d
Oct 02, 2020
- Bump stdpp. · 5ab2529d
  Robbert Krebbers authored 4 years ago
  
  5ab2529d
Oct 01, 2020
- Bump std++. · 8f6c063a
  Robbert Krebbers authored 4 years ago
  
  8f6c063a
- Merge branch 'ci/robbert/view' into 'master' · 63b09404
  Robbert Krebbers authored 4 years ago
  
  The view camera. Closes #257 See merge request iris/iris!516
  63b09404
- CHANGELOG. · 8341b39b
  Robbert Krebbers authored 4 years ago
  
  8341b39b
- Remove lemma `view_equivI` and document that. · c66ceaed
  Robbert Krebbers authored 4 years ago
  
  c66ceaed
- Add documentation for auth & view. · 12796181
  Robbert Krebbers authored 4 years ago
  
  12796181
- Add `included_both` lemmas for auth & view. · f98235de
  Robbert Krebbers authored 4 years ago
  
  f98235de
- Add injectivity instances for `●` and `◯` for auth & view. · 55b62c35
  Robbert Krebbers authored 4 years ago
  
  55b62c35
- Add lemma `view_update_frag`. · be858230
  Robbert Krebbers authored 4 years ago
  
  be858230
- Generalize inclusion lemmas for view & auth to iff. · 4df70955
  Robbert Krebbers authored 4 years ago
  
  4df70955
- Add inclusion lemmas for view & auth. · 7f61fa72
  Robbert Krebbers authored 4 years ago
  
  7f61fa72
- The view camera and redefine the auth camera in turns of it. · db3bf9a2
  Robbert Krebbers authored 4 years ago
  
  db3bf9a2
- Merge branch 'robbert/bi_pure_forall' into 'master' · 5bab637b
  Robbert Krebbers authored 4 years ago
  
  Remove `pure_forall_2` from BI interface + BI notation for `¬` See merge request iris/iris!526
  5bab637b
- More Coqdoc. · 377c2d14
  Robbert Krebbers authored 4 years ago
  
  377c2d14
- Remove ¬ notation in counterexamples. · 256de028
  Robbert Krebbers authored 4 years ago
  
  256de028
- ASCII notation for negation in bi_scope. · 82a75fc2
  Robbert Krebbers authored 4 years ago
  
  82a75fc2
- Merge branch 'msammler/multithread_adequacy' into 'master' · ebb6c018
  Ralf Jung authored 4 years ago
  
  Make adequacy apply to multiple initial threads See merge request iris/iris!485
  ebb6c018
- CHANGELOG. · 2c2565ac
  Robbert Krebbers authored 4 years ago
  
  2c2565ac
- Add BI notation for negation. · f73319e8
  Robbert Krebbers authored 4 years ago
  
  f73319e8
- Prove that `BiPureForall` holds if we assume classical logic in Coq. · 3e51bdd7
  Robbert Krebbers authored 4 years ago
  
  3e51bdd7
- Remove property `(∀ a, ⌜ φ a ⌝) ⊢ ⌜ ∀ a, φ a ⌝` from the BI canonical structure and · 6e334252
  Robbert Krebbers authored 4 years ago
  
  put it into a type class `BiPureForall`. This property does not hold for embeddings of classical logic into Coq.
  6e334252
- make adequacy apply to multiple initial threads · 996ec297
  Michael Sammler authored 4 years ago
  
  996ec297
Sep 30, 2020
- Merge branch 'ci/robbert/canonical_underscore' into 'master' · e28498f5
  Ralf Jung authored 4 years ago
  
  Remove anonymous Type fields from camera structures. See merge request iris/iris!525
  e28498f5
- Remove anonymous Type fields from camera structures. · 6ef0253d
  Robbert Krebbers authored 4 years ago
  
  These were already removed from the OFE and BI structures, but were left here.
  6ef0253d
- Merge branch 'msammler/big_op_lemmas' into 'master' · fe735a96
  Robbert Krebbers authored 4 years ago
  
  Lemmas about big op on lists for !485 See merge request !509
  fe735a96
- Lemmas about big op on lists for !485 · bd11cf26
  Michael Sammler authored 4 years ago
  
  bd11cf26