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/big_op_binder
  • 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
  • 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.07Jun6131May30292827252423222120191312111097643229Apr272625242120191815141312111098730Mar292322212019181716151412111098765432129Feb28272625242322benchmark visualize: but legend next to graphTurn some "case _ :" occurences into "case:'.Name some intro-ed stuff.Not all [Qp]s are [frac]s, so make the notation only parsing.Simplify prod_leibniz.useless ArgumentsMerge branch 'master' of gitlab.mpi-sws.org:FP/iris-coqSimplify frac : use a pair of a rational and a carrierMake iAssert infer the cmra M of the asserted uPred M.Merge branch 'master' of gitlab.mpi-sws.org:FP/iris-coqGot rid of one_shotUse |==> syntax for 'preserve pvs' specialization pattern.Rename box_slice into slice.Change the Coq scope notations for viewshifts into parsing only.Notations 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.