Skip to content
Snippets Groups Projects
Select Git revision
  • atomic
  • ci/janno/vmcast
  • ci/mtac2-tt
  • ci/ralf/atomic
  • ci/ralf/pm_red
  • ci/ralf/telescopes
  • ci/robbert/overloaded_wp
  • fast_string
  • gen_proofmode
  • iris-3.0
  • iris-3.1
  • janno/fix-566
  • janno/iframe-cbv
  • janno/iframe-no-upd
  • janno/ipm-strings
  • janno/ipm-strings-upstream
  • janno/metacoq
  • janno/try-HB
  • jh/done_contradiction
  • jh/evar_iframe
  • 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
30 results
You can move around the graph by using the arrow keys.
Created with Raphaël 2.2.01Jun31May30292827252423222120191312111097643229Apr272625242120191815141312111098730Mar292322212019181716151412111098765432129Feb282726252423222120Notations for X ⊆ Y ⊆ Z.Generalize big_sepM_fn_insert and big_sepS_fn_insert.Make iFresh faster on environments containing evars.Tactic iFrame (without args) that tries to frame all spatial hyps.Auto hints for the proof mode.Simplify the definition of Exclusive. Use it for gmap.Merge branch 'master' of gitlab.mpi-sws.org:FP/iris-coqExclusive typeclass for CMRA elementsChange the precedence of ⊢ to be the same as →, and the precedence of ⊣⊢ toauth: strong allocation and some more proper lemmassolve_proper: let it prove pointwise_relation as wellMore documentation of f_equiv.Oops, fix 8d1b743e, forgot something.Rename box_inv into box_slice_inv.Make f_equiv slightly more robust.Change notation of viewshifts in Coq scope.Prove that Countable A gives Countable B for an injection B → A.boxes: even fewer underscoresMerge branch 'master' of gitlab.mpi-sws.org:FP/iris-coqboxes: fewer underscoresMake iFresh more robust in the presence of evars.Some properties about set disjointness.make box_fill more symmetric to box_emptyStrengthen big_sepM_insert_override and use it.Some forgotten type class instances for boxes.Formalization of Ralf's boxes.Pvs and big_op commute.More uPred_big_op properties.Make iDestruct and iCombine work with (sep)conjunctions under big_ops.Prove that big_sepM and fmap commute.Prove (P ≡ Q) ⊢ (P ↔ Q).Generalize insert_delete lemma.Later stripping for big_ops.Prove equivalent more useful def of valid on auth A when A is discrete.Local updates for option.Csum: sum of two CMRAsMerge branch 'master' of gitlab.mpi-sws.org:FP/iris-coqSimplify local update for exclProperties for uPred_big_opM and fn_insert.Hint Resolve uPred.eq_refl'.