Skip to content
Snippets Groups Projects
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
You can move around the graph by using the arrow keys.
Created with Raphaël 2.2.028Jul272625232221201918161513121165432130Jun2827262524232120191817161514876131May30292827252423222120191312111097643229Apr272625242120191815141312111098730Mar29232221201918171615141211109876add a comment about the 'no core' elementMove proof mode type class instances to their own file.Local and FP updates starting with empty gset.FP update for auth without fragment.Better implementation of iPoseProof.Removed obsolete axiom from the defn of Ex(M).docs: update lifting lemmasadd missing item to CHANGELOGdocs: apply some feedback from AlesMerge branch 'master' of gitlab.mpi-sws.org:FP/iris-coqdocs: address Lars' remaining commentsRule for eliminating a raw view shift into a pure proposition.Better notations for raw view shifts.Merge branch 'master' into iris3.0Declare inG arguments of own_* implicit but not maximally inserted.Iterated later modality.Revert "Make the types of the finite map type classes more specific."Make the types of the finite map type classes more specific.don't backtrace on the operatorMerge remote-tracking branch 'MPI-SWS/master'Use auth_update_no_frame in boxes.More consistent names for gset updates.FP update for auth without frame.Relate subseteq on collections to the extension order.Make type class inference for inG less eager.Revert "Hack to delay type class inference in iPoseProof."Hack to delay type class inference in iPoseProof.Merge branch 'master' of https://gitlab.mpi-sws.org/FP/iris-coqFixed some typos in the appendix.Rename some proofmode stuff to be no longer primitive view shift specific.Proofmode type class instances for raw view shifts.docs: update CMRA constructions for partial coredocs: update (CM)RA algebra axioms to aprtial coresupdate CHANGELOGrename: preserving for a partial order -> monotoneupdates iris.styadd a CHANGELOGNew notion of raw view shifts.Simplify TimelessElim class.Fix implicit arguments of gset CMRA.