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.018May1716131198764123Apr2012111087623Mar21201821Feb112130Jan2724222317161716151413121130Dec1716159876532129Nov2624232216151210986527Oct262519151312112127Sep26252413106543131Aug1031Jul302928272625232221201918161297528Jun262524232221201918171514131211109876543231May282726252120191817131211975230Apr2922201918151413121186527Mar252423221817Merge 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`.Bump std++.bring back the verbatimfix some coqdoc warningsMerge branch 'ralf/dom' into 'master'bump std++; port to dom D type being implicitMerge branch 'indentations' into 'master'Updated suggested emacs indendation configurationMerge branch 'ralf/big_sepS' into 'master'strengthen big_sepS_union_2add big_sepS_insert_2' and big_sepS_union_2normalize OCaml versionsfix accidental use of coPset domainstop using coPsetMerge branch 'fixpoint-tele_arg' into 'master'Pick and name universes for [bi_tforall] and [bi_texist].looks like there is no 4.13.2bump ocaml version
Loading