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.09Jun87325May242321181716131198764123Apr2012111087623Mar21201821Feb112130Jan2724222317161716151413121130Dec1716159876532129Nov2624232216151210986527Oct262519151312112127Sep26252413106543131Aug1031Jul302928272625232221201918161297528Jun262524232221201918171514131211109876543231May282726252120191817131211975230Apr2922201918151413121186527Mar2524Merge branch 'ralf/proofmode-of-envs' into 'master'remove of_envs_eq'; add of_envs_altchangelogrename env_and_pers → env_and_persistentlyUse big op properly instead of `env_map`. Simplify some proofs.document what needs to be in pm_evaladjust proofmode of_envs to rely less on persistently_emp_2Merge branch 'robbert/big_andL_absorbing' into 'master'normalize 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.