Skip to content
Snippets Groups Projects

Repository graph

You can move around the graph by using the arrow keys.
Select Git revision
  • ci/debug
  • ci/for_proph
  • ci/hai/siProp
  • ci/janno/strict-tc-resolution
  • ci/ralf/Z_of_nat
  • ci/ralf/bi-language
  • ci/ralf/frame-frac
  • 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
  • ci/robbert/merge_sbi
  • ci/robbert/naive_solver
  • 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
34 results
Created with Raphaël 2.2.025Oct22211817161514131210976543228Sep272120191514131298765432131Aug302928272625242322212019181716141110986542128Jul272625232221201918161513121165432130Jun282726252423212019181716Rename uPred_eq into uPred_internal_eq.Allow iMod to work under wands and foralls.Generalize update tactics into iMod and iModIntro for modalities.Rename model -> iprop, ghost_ownership -> own.Avoid naming a type class constraint.Rename except_last -> except_0.Move base_logic stuff to its own folder: base_logic.Use notation |==> instead of |=r=> for basic update modality.Rename rvs -> bupd (basic update), pvs -> fupd (fancy update).Make argument K of wp_bind explicit.docs: fix iris version numberMerge branch 'docs-geometry' into 'master' docs: rename proof rule subst -> cutdocs: make the borders slightly larger, so that lines of text dont become so ridicolously long and are easier to readdocs: add a small abstract with more linksdocs: add linkto websitedocs: DC logic, be gonedocs: renaming updatesthis is an rc (and we still have some file renaming planned before the release)docs: update to latest changes in Coq developmentDefine hoare triple and view shift in terms of wand.Tweak macros for maps.Linear VS that do not use tikz, so that the rendering does not depend somewhat on the context.docs: use new notation of None and invalid CMRA elementslet's try not to make those macro names too longupdate iris.stybe even more verbose about licensingMerge branch 'ralf/docs-license' into 'master' Be explicit about the CMRA on optionadd a LICENSE file summarizing our licensingput the appendix under CC-BY 4.0fix CHANGELOG markupFix state CMRA.Use \nat macro.Define \List macro and use the more commonly used \vec for denoting lists.Make better use of \Val, \State, \Expr macros.Move language section to its own file.Define macro for singleton map and use it.Remove obsolete file encodings.tex.Merge branch 'master' of gitlab.mpi-sws.org:FP/iris-coq