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.02Aug128Jul272625232221201918161513121165432130Jun2827262524232120191817161514876131May30292827252423222120191312111097643229Apr272625242120191815141312111098730Mar29232221201918171615141211109876Reorganize algebra/gset a bit.Merge branch 'tlock' into 'master' ticket lockMerge branch 'master' into iris3.0Stronger allocation updates for gset.Conversion from coPset to gset positive.Remark that many proofmode tactics work with other connectives too.Rename trm → pm_trm in proof mode documentation.Fix typo in ProofMode.md.Make hlist universe polymorphic.'Fork' is atomiciris-2.0iris-2.0add 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.