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.08Jun7325May242321181716131198764123Apr2012111087623Mar21201821Feb112130Jan2724222317161716151413121130Dec1716159876532129Nov2624232216151210986527Oct262519151312112127Sep26252413106543131Aug1031Jul302928272625232221201918161297528Jun262524232221201918171514131211109876543231May282726252120191817131211975230Apr2922201918151413121186527Mar25242322normalize away some trailing spacesupdate dependenciesAdd `Absorbing` instances for `[∧ list]`.Merge branch 'functors' into 'master'Add some missing functors in algebra/libMerge branch 'ralf/tex-heaplang' into 'master'Merge branch 'ralf/triples' into 'master'Merge branch 'atomic-flip' into 'master'changelogFlip quantifiers for atomic updates, and double them upadd logically atomic triplesRevert "Merge branch 'iris_style_improvements' into 'master'"add a test document for our macros(maybe) better symbol for Ptraddremove MatchCore macro, and add sugar for match with bindersadd short-circuiting boolean operationsdocument HeapLang syntax and operational semanticsMerge branch 'iris_style_improvements' into 'master'cleanup importsMerge branch 'paolo/fix-461' into 'master'bump std++ properlybump std++Add testcase for #461Bump stdpp for universe fixuse tc_opaque for a complicated definitionupdates preserve being AbsorbingRenamed internal macroRemoved unused angle bracket macrouse Coq 8.15.1, and enable flambdaupdate dependenciesMade hoare triple macro compatible with e.g. array environmentAdd some line breaks to very long lines.Merge branch 'ralf/bi-lemmas' into 'master'changelogmake affinely_True_emp more useful, and make absorbingly lemmas consistentMerge branch 'robbert/seal' into 'master'CHANGELOG.No longer make `envs_entails_unseal` local.Make unseal collections `Local`.Rename seal lemmas from `_eq` to `_unseal` and make sealing stuff `Local`.