Commits · 01faec8bbc0f90befa1cfe7b92c4c8f814264f46 · Paolo G. Giarrusso / iris

Oct 15, 2020
- avoid relying on implicit instance generalization · 01faec8b
  Ralf Jung authored 4 years ago
  
  01faec8b
- auth formatting nit · f07fca13
  Ralf Jung authored 4 years ago
  
  f07fca13
Oct 14, 2020
- Merge branch 'ralf/gen_heap' into 'master' · dc793c10
  Ralf Jung authored 4 years ago
  
  clarify the intended use of gen_heap, and rename gen_heap_ctx -> gen_heap_interp See merge request iris/iris!542
  dc793c10
- further work on docs · 87460096
  Ralf Jung authored 4 years ago
  
  87460096
Oct 13, 2020
- rename gen_heap_ctx -> gen_heap_interp, and similar for proph_map_ctx · e31517d5
  Ralf Jung authored 4 years ago
  
  e31517d5
- Merge branch 'ralf/upred-cmra-extension' into 'master' · 5558d66d
  Ralf Jung authored 4 years ago
  
  add counterexample for uPred CMRA extension axiom See merge request iris/iris!539
  5558d66d
- apply feedback; use more coqdoc · 33d0c3c6
  Ralf Jung authored 4 years ago
  
  33d0c3c6
- Merge branch 'ralf/gmap_view_delete' into 'master' · c41a9d2e
  Ralf Jung authored 4 years ago
  
  gmap_view: add deletion lemma See merge request !541
  c41a9d2e
Oct 12, 2020
- Merge branch 'robbert/issue_347' into 'master' · feebc2f5
  Robbert Krebbers authored 4 years ago
  
  Make `solve_inG` faster. See merge request iris/iris!532
  feebc2f5
- Define non-unital camera functors in such a way that the non-unital camera is used. · ee264e90
  Robbert Krebbers authored 4 years ago
  
  ee264e90
- Make `solve_inG` faster. · eac00ee5
  Robbert Krebbers authored 4 years ago
  
  1.) First `simpl` away all the functors 2.) Don't use `done`, which calls `split`.
  eac00ee5
- clarify the intended use of gen_heap · f94e312e
  Ralf Jung authored 4 years ago
  
  f94e312e
- gmap_view: add deletion lemma · 4b2bf95f
  Ralf Jung authored 4 years ago
  
  4b2bf95f
- fix strange scope error with Coq 8.10 · 3494dfba
  Ralf Jung authored 4 years ago
  
  3494dfba
- Merge branch 'ralf/gmap_auth' into 'master' · 93429372
  Ralf Jung authored 4 years ago
  
  add a general gmap_view library and use it for wsat, gen_heap, proph_map Closes #328 See merge request !486
  93429372
Oct 10, 2020
- Merge branch 'ralf/frac-combine' into 'master' · cb8e35b8
  Ralf Jung authored 4 years ago
  
  fix combining two q/2 fractions to a q See merge request !540
  cb8e35b8
- fix combining two q/2 fractions to a q · 96455f78
  Ralf Jung authored 4 years ago
  
  96455f78
- API tweaks · 8912c3d2
  Ralf Jung authored 4 years ago
  
  8912c3d2
Oct 09, 2020
- changelog entry and some more comments at the top of the file · 4e205a0e
  Ralf Jung authored 4 years ago
  
  4e205a0e
- port gmap_auth to view CMRA · 0d988d92
  Ralf Jung authored 4 years ago
  
  0d988d92
- add a general gmap_auth library and use it where possible · b4cf0bc1
  Ralf Jung authored 4 years ago
  
  b4cf0bc1
- remove useless parameter, and export public dependencies from dfrac · af0efbba
  Ralf Jung authored 4 years ago
  
  af0efbba
- Merge branch 'ralf/dfrac' into 'master' · 86125f9c
  Ralf Jung authored 4 years ago
  
  generalize dfrac IsOp instance See merge request iris/iris!537
  86125f9c
- consistently rename algebra IsOp instances · be45363e
  Ralf Jung authored 4 years ago
  
  be45363e
- Merge branch 'ralf/löb' into 'master' · bde48e82
  Robbert Krebbers authored 4 years ago
  
  prove a funny consequence of Löb induction See merge request !538
  bde48e82
- prove a funny consequence of Löb induction · 9a6976e2
  Ralf Jung authored 4 years ago
  
  9a6976e2
- add counterexample for uPred CMRA extension axiom · d22722fa
  Ralf Jung authored 4 years ago
  
  d22722fa
Oct 08, 2020
- Merge branch 'robbert/counter' into 'master' · 206d8842
  Robbert Krebbers authored 4 years ago
  
  Counterexamples for affine+em and Löb+em. See merge request !536
  206d8842
- Take comments into account. · 89d172ed
  Robbert Krebbers authored 4 years ago
  
  89d172ed
- add IsOp instances for addition and min/max · 1f85ff24
  Ralf Jung authored 4 years ago
  
  1f85ff24
- generalize dfrac IsOp instance · e4980084
  Ralf Jung authored 4 years ago
  
  e4980084
- Make the proof closer to the jungle proof. · 7b460868
  Robbert Krebbers authored 4 years ago
  
  7b460868
- Cite jungle paper. · 13e8dee5
  Robbert Krebbers authored 4 years ago
  
  13e8dee5
- Counterexamples for Affine+EM and Löb+EM. · a3f1b72e
  Robbert Krebbers authored 4 years ago
  
  a3f1b72e
Oct 07, 2020
- Merge branch 'robbert/view_auth_frac_rename' into 'master' · b23feb70
  Robbert Krebbers authored 4 years ago
  
  Consistent naming for auth/view lemmas. See merge request !533
  b23feb70
- Remove some redundant type annotations, which are not needed due to `Implicit Types`. · a97d0ee9
  Robbert Krebbers authored 4 years ago
  
  a97d0ee9
- Merge branch 'ralf/to-agree-op-valid' into 'master' · 2d8560ca
  Robbert Krebbers authored 4 years ago
  
  add iff lemma for '✓ (to_agree a ⋅ to_agree b)' See merge request !535
  2d8560ca
- add iff lemma for '✓ (to_agree a ⋅ to_agree b)' · 064690ea
  Ralf Jung authored 4 years ago
  
  064690ea
- fix typo in Makefile · 75de6ad4
  Ralf Jung authored 4 years ago
  
  75de6ad4
Oct 06, 2020
- CHANGELOG. · 037349bf
  Robbert Krebbers authored 4 years ago
  
  037349bf