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.04Aug2128Jul272625232221201918161513121165432130Jun2827262524232120191817161514876131May30292827252423222120191312111097643229Apr272625242120191815141312111098730Mar2923222120191817161514121110987Better lemmas for splitting the fractional heap_mapsto.Injectivity instance for Z.of_nat.Fix levels of arguments in proof mode terms.Clear temporary hypotheses created by iIntoEntails.CMRA functor (without unit) on auth.Unfolding properties for Nat.iter.docs: fix COFE limit axiomSyntax 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.