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.010Feb985432131Jan302927262523222120191817161413129865422Dec21161514118423Nov22201918171612119630Oct2928272316151431Aug16Jul24Jun2215115432131May302928272625161514131211723Apr141311109872131Mar30292827252423201918171613remove some unused typeclasses and notation: EquivE and SubsetEqEmake some nested function calls in heap_lang/ more readableignore some tmp emacs filesno reason for this primeRemove Unshelve hack in ghost_ownership.Fix some identation.Typeclass Opacity and Params for inv.Seperate derived rules for own and valid in upred.Make let a built-in connective of heap_lang.Change the level of wand so it is more like the implication.Change the level of view shifts so it is more like the implication.Change wp to have a view shift in the value case.Notation for = in uPred_scope.Notations for LitTrue and LitFalse.Use a named representation of binding in heap_lang.Fix typo in comments and turn them into Coqdoc.Misc clean up.Stronger version of map_insert_op.Stronger version of auth_update w.r.t. step indexes.Remove FIXME, it is due to a Set Printing all above.Remove sum2bool.some commentsderive rules for inv and own for view shifts; change notation for view shiftsghost_ownership: prove frame-preserving update from emptyalgebra: prove some frame-preserving updates from emptyheap_lang: get rid of some unnecessary parenthesisrename namespace -> invariants, global_cmra -> ghost_ownershipprove pvs_allocMerge branch 'master' of gitlab.mpi-sws.org:FP/iris-coqprove open_close also for wpProve coPset_suffixes_infinite.Merge branch 'master' of gitlab.mpi-sws.org:FP/iris-coqprove pvs_alloc, modulo the closure under suffixes being infiniteadd a stub lemma in co_psetfix viewshifts.vprevent autosubst from unfolding our sugarprove some things about invariantsfix and_exist_rrename lemmas about ownI; stronger mask_weaken ruleprove that 'exists' and 'and' commute; make some more BI lemmas derived
Loading