Skip to content
Snippets Groups Projects
Select Git revision
  • ci/debug
  • ci/for_proph
  • ci/general-contractive
  • ci/hai/siProp
  • ci/hint-cut-revert
  • ci/janno/strict-tc-resolution
  • ci/msammler/nb_state
  • ci/name-mangle
  • ci/ralf/Z_of_nat
  • ci/ralf/bi-language
  • ci/ralf/options-timing
  • 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/hint_cut_plain
  • ci/robbert/iFrame
  • iris-4.1.0
  • 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
37 results
You can move around the graph by using the arrow keys.
Created with Raphaël 2.2.05Mar43124Feb23221917161514131211105432129Jan282726252320191715141312875424Dec231918161110976432130Nov27262319181312111096543231Oct302927222120151413121098765432130Sep29282726242322211615141211108753230Aug29282412724Jul222118add ghost_map_update lemmafix nitsadd ghost_map libraryMakes it possible to use several logical steps for one logical steps, in a way which can be controlled by ghost state.fix dfrac sed scriptMerge branch 'dfrac-view' into 'master'Merge branch 'yusuke/fix-typos' into 'master'Fix typosMerge branch 'master' of https://gitlab.mpi-sws.org/iris/iriscomment on iAaccIntroMerge branch 'ralf/rewrite' into 'master'avoid relying on rewrite's implicit revertbump CI to Coq 8.13.1Make changes related to dfrac generalizationEnforce fraction naming conventions with implicit typesAdd changelog entry for auth and view changesName lemmas about dfrac accordinglyMake view auth take dfracEnable `Typeclasses Strict Resolution` for dervied_connectives.vci/janno/strict…ci/janno/strict-tc-resolutionfix changelog typosMerge branch 'ralf/changelog' into 'master'iris-3.4.0iris-3.4.0move timing and packaging to the 8.13 jobname authors of highlighted features and release managersfinalize changelog for releaseMerge branch 'ralf/fupd-mask' into 'master'changeloganother naming schemeMove some CHANGELOG entries from proofmode to BI.add better lemmas for working with mask-changing fupd, and rearrange names a bitMerge branch 'ralf/monpred-scope' into 'master'fix monPred scope bindingbetter support for view shift with mismatching masksralf/vs-mask-ad…ralf/vs-mask-adjustMerge branch 'robbert/equiv_entails' into 'master'Rename `equiv_spec` → `equiv_entails` to be consistent with conventions in std++.fix typosilence warningsexplain why we reconfigure printing all the timeMerge branch 'print-prim' into 'master'adapt to coq/coq#13840Merge branch 'ralf/frac-op-valid' into 'master'