Skip to content
Snippets Groups Projects
Select Git revision
  • clairvoyant
  • erasure
  • erasure-squashed
  • erasure_backup
  • janno/early-scopes
  • janno/hoare-notation
  • jh_coreless_cmras
  • jh_inductive_pairs
  • jh_partial_core
  • lang_lemmas
  • less_canonical
  • master default
  • monotone
  • mra-changelog
  • primitive_sealing
  • ralf/magic-singleton
  • rename
  • iris-2.0
  • iris-2.0-rc2
  • iris-2.0-rc1
  • iris-1.1
  • iris-1.0
  • hope-2015-coq-1
  • appendix-1.0.0
  • appendix-1
25 results
You can move around the graph by using the arrow keys.
Created with Raphaël 2.2.04Feb32131Jan302927262523222120191817161413129865422Dec21161514118423Nov22201918171612119630Oct2928272316151431Aug16Jul24Jun2215115432131May302928272625161514131211723Apr141311109872131Mar30292827252423201918171613121186543228Feb272624232221201918171615More stuff for indexed products.Turn master into Iris 2.0Rename modures -> algebra and iris -> program_logic.add a version of bind for ectx itemsRevert "Remove FIXME now that ssr bug #22 is fixed."*oops* forgot to fix importsrename barrier/ -> heap_lang/Merge branch 'v2.0' of gitlab.mpi-sws.org:FP/iris-coq into v2.0Remove FIXME now that ssr bug #22 is fixed.actuall make do_step work on heap_step goalsFix implicit arguments indexed product.change notation for frame-preserving updatesAdd documentation to heap_lang_tactics.Merge branch 'v2.0' of gitlab.mpi-sws.org:FP/iris-coq into v2.0Indexed products as COFE and CMRA.Parenthesis bug in tactic. Thanks to Ralf for noting.add an omega auto databaseMerge branch 'v2.0' of gitlab.mpi-sws.org:FP/iris-coq into v2.0extend derived lifting lemmas to deal with fork (puts them on-par with the hoare lifting lemmas)Merge branch 'v2.0' of gitlab.mpi-sws.org:FP/iris-coq into v2.0Frame preserving updates for auth.Some forgotten Proper instances.Merge branch 'v2.0' of gitlab.mpi-sws.org:FP/iris-coq into v2.0minor nitsMerge branch 'v2.0' of gitlab.mpi-sws.org:FP/iris-coq into v2.0Frame preserving updates for maps.More consistent naming for frame preserving updates.Frame preserving updates for op.Merge branch 'v2.0' of gitlab.mpi-sws.org:FP/iris-coq into v2.0reduce imports of language.vFrame preserving updates for option.Frame preserving updates for excl.Frame preserving updates only from steps ≠ 0.Basic properties of frame preserving updates and those for products.Shorten some stuff in heap_lang.Make names in hoare_lifting more consistent with those in lifting.Remove some unnecessary Implicit Types.Define heap_lang.fill using fold_right.remark a TODO for laterslightly optimize eauto fuel