Skip to content
Snippets Groups Projects
Select Git revision
  • ci/debug
  • ci/for_proph
  • ci/general-contractive
  • ci/hai/siProp
  • ci/janno/strict-tc-resolution
  • ci/msammler/nb_state
  • ci/ralf/Z_of_nat
  • ci/ralf/bi-language
  • ci/robbert/big_op_binder
  • ci/robbert/contractive_ne
  • ci/robbert/coq_bug_7773
  • ci/robbert/faster_iDestruct
  • ci/robbert/faster_iDestruct2
  • ci/robbert/faster_iFresh_joe
  • ci/robbert/frame_fractional
  • ci/robbert/iFrame
  • ci/robbert/into_fupd
  • ci/robbert/into_val_pures
  • ci/robbert/kill_locked_value_lambdas
  • ci/robbert/mapsto_persist
  • iris-4.0.0
  • iris-3.6.0
  • iris-3.5.0
  • iris-3.4.0
  • iris-3.3.0
  • iris-3.2.0
  • iris-3.1.0
  • iris-3.0.0
  • 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
36 results
You can move around the graph by using the arrow keys.
Created with Raphaël 2.2.08Feb5432131Jan302927262523222120191817161413129865422Dec21161514118423Nov22201918171612119630Oct2928272316151431Aug16Jul24Jun2215115432131May302928272625161514131211723Apr141311109872131Mar30292827252423201918171613121186543228Feb27262423prove the remaining lemmas in global_cmra.vDo not export ownershipCoq syntax nitprove some properties of the embedding into the global CMRAmove indexed products to their own fileadd Robbert's global.v, change some names around, and prove allocationuse "inv" for the invariants in namespacesget rid of a few %L we do not need any moreprove that we can allocate an authImprove notations for heap_lang.Viewshifts from ∅.Frame preserving updates related to ∅.construct the resource functormove functor def. to algebra/show that we always own somethingexperimenting with a global CMRA that is an indexed productMerge branch 'master' of gitlab.mpi-sws.org:FP/iris-coqCombinators for iFunctors.some more work on notationexperiment a little with notation for our languagemove upred.v into the right folderMore indexed product properties.Make various functors more consistent with each other.Misc tweaking of consistency of coding style.Some cleanup in upred.Define some flipped monotonicity Propers for binary uPred connectives.No longer require iFunctor to have an identity element.Extensionality for fmap on option.CMRAIdentity instance for option.Make functor stuff more consistent.More 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 goals