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.02Aug128Jul272625232221201918161513121165432130Jun2827262524232120191817161514876131May30292827252423222120191312111097643229Apr272625242120191815141312111098730Mar2923222120191817161514121110987Syntax for framing the entire persistent context.Fix framing under conjunctions.Move tests/ticket_lock.v -> heap_lang/lib/ticket_lock.v.Document iFrame without arguments.Simplify the ticket lock proofs a bit.Sets of sequences of natural numbers.Reorganize 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.