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.09Sep8765432131Aug302928272625242322212019181716141110986542128Jul272625232221201918161513121165432130Jun2827262524232120191817161514876131May30292827252423222120191312111097643229Apr27262524212019Shorten proof of Qp_lower_bound a bit.Elimination of pure facts using Coq introduction patterns for iVs.Elimination of pure facts using Coq introduction patterns for iAssert.Remove useless scope delimiters.Support for specialization of P₁ -★ .. -★ Pₙ -★ Q where Q is persistent.More validity lemmas for auth.Prove lemma cmra_valid_included.Non-primitive VS that take a step.Add lemma about the existence of a lower bound of two fractions.Merge branch 'double_negation' into 'master' Define disjointness of namespaces in terms of masks.\n\nThe proofs are made simpler and some lemmas get more general.Notation for primitive view shifts that take a step.Direct (double negated) adequacy proof for nnvs modalityUse bool instead of int in barrier implementation.Use pair syntax in par implementation.More consistent names in ticket lock.Remove CAS loop in release of ticket_lock.Variant of pair_split for Leibniz equality.Merge branch 'master' of https://gitlab.mpi-sws.org/FP/iris-coqNon-disjoint CMRA structure on gset and coPset disj.Prove stronger version of later_ownM.Viewshifts that take a step.Rename envs_persistent → env_spatial_is_nil.Tweak.Merge branch 'master' of https://gitlab.mpi-sws.org/FP/iris-coqMore lemmas about Some and included.Double negation elimination for pure props holds under nnvs modality.Relate ≼ and ⊆ on coPset and gset.Prove variants of CMRA facts for CMRAs with = ↔ ≡.Relate ≼ to is_Some and dom.Introduce notation excl' (like Excl' and ExclNone').Merge branch 'master' of https://gitlab.mpi-sws.org/FP/iris-coqGroup iff properties in uPred.Prove that uPred_pure commutes with the first-order connectives.Reorganize double negation equivalence proof; direct proof of transitivityProve more rules for always in the logic.Prove more later properties in the logic.Prove Timelessness of pure in the logic.Merge branch 'master' of https://gitlab.mpi-sws.org/FP/iris-coqProve Timeless instances in the logic instead of the model.