Skip to content
Snippets Groups Projects
Select Git revision
  • ci/debug
  • ci/for_proph
  • ci/general-contractive
  • ci/hai/siProp
  • ci/janno/strict-tc-resolution
  • ci/msammler/nb_state
  • ci/ralf/Z_of_nat
  • ci/ralf/bi-language
  • 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
  • iris-4.0.0
  • iris-3.6.0
  • 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
36 results
You can move around the graph by using the arrow keys.
Created with Raphaël 2.2.021Sep20191514131298765432131Aug302928272625242322212019181716141110986542128Jul272625232221201918161513121165432130Jun2827262524232120191817161514876131May30292827252423222120191312111097643229Apr2726252421Destructors for csum.Make it possible to frame hypotheses using specialization patterns.Make iFrame finish the goal if everything has been framed.Better 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 modality