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.014Sep131298765432131Aug302928272625242322212019181716141110986542128Jul272625232221201918161513121165432130Jun2827262524232120191817161514876131May30292827252423222120191312111097643229Apr27262524212019Make Is_true a typeclass.In gset idemp_L rather than union_idem_LCorrect the name gmap_persistent -> gset_persistentMake elements gset persistent.Merge branch 'master' of https://gitlab.mpi-sws.org/FP/iris-coqLemma [exists_impl_forall] for currying an exists into a forall.Merge branch 'master' of https://gitlab.mpi-sws.org/FP/iris-coqShorten 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.