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.021Sep20191514131298765432131Aug302928272625242322212019181716141110986542128Jul272625232221201918161513121165432130Jun2827262524232120191817161514876131May30292827252423222120191312111097643229Apr272625242120Better representation of specialization patterns.Validity and update lemmas for owning multiple ghosts.Use ⊆ type class for set-like inclusion of lists.Make iSplit{L,R} ignore persistent hypotheses.Define shorthand EqDecision A := (∀ x y : A, Decision (x = y)).Document iInduction.Attempt at an iInduction tactic.New iFresh' H tactic that generates names starting with H.Better implementation of iLöb.Support for framing pure hypotheses.Definition of FromPure that is symmetric w.r.t. IntoPure.Better error message for iTimeless.Also change the core of coPset to be the identity.Merge branch 'master' into 'master' [from_exist_later] for instantiating an existential behind a later.Change hypotheses order for [frame_later] for better perfs.Make iFrame able to strip a later from a framed hypothesis when framing under a later.Make 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.