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.06Apr432131Mar272523212019181613121096428Feb262524232120191817151413121110765432130Jan29242321181716151413111098720Dec19181413109654225Nov222120141312111087652131Oct2522181412119620Sep19131198630Aug2928272625242216141312987630Jul221413129753130Jun2928272625242120191817161514Add support for pure names in intro patternsMerge branch 'big-op-insert-delete' into 'master'Add insert delete lemma for big ops over gmapMerge branch 'ralf/misc-lemmas' into 'master'bump CI to 8.11.1use type-ascribed equality notationadd pair_included, auth_frag_core, singleton_core_totalFix ambigious entailments.Fix bug that makes compilation with Coq 8.9 fail.Merge branch 'robbert/some_cmra_lemmas' into 'master'Apply suggestion to CHANGELOG.mdupdate dependenciesCHANGELOG.Make `Excl_included` and `Excl_includedN` bi-implications.Add lemma `singleton_included : {[ i := x ]} ≼ ({[ i := y ]} ↔ x ≡ y ∨ x ≼ y`.Merge branch 'ralf/propofe' into 'master'add OFE structure for PropMerge branch 'robbert/lock_namespace' into 'master'Comments and Coqdoc-ify.CHANGELOG.Remove namespaces from lock API.Merge branch 'robbert/tele' into 'master'CHANGELOG.Add proof mode test cases for handling telescopes.Support telescopic `∀..` in `iStartProof`.Add affine, absorbing, persistent, and timeless instances for telescopes.Missing proof mode instances for telescopes.Consistently Use meta variable `TT` for telescopes in `class_instances_bi`.update dependenciesAdd `NonExpansive` instances for `!!!` on maps and lists.Merge branch 'robbert/oFunctor' into 'master'CHANGELOG.Add `{o,r,ur}Functor_oFunctor_compose` to compose two functors.Rename `{o,r,ur}Functor_{ne,id,compose,contractive}` intoMerge branch 'robbert/lock_contractive' into 'master'Merge branch 'master' of https://gitlab.mpi-sws.org/iris/iris into master.2changelog format nitCHANGELOG.Add rule `is_lock_iff` for locks.Make `_iff` and `_alter` lemmas for invariants consistent.