Skip to content
Snippets Groups Projects
Select Git revision
  • ci/debug
  • ci/for_proph
  • ci/janno/debug-opam
  • ci/janno/let_bind_envs
  • ci/janno/vmcast
  • ci/joe/compact_ipm
  • ci/joe/compact_ipm_remaining
  • ci/joe/compact_ipm_simple
  • ci/msammler/iris-coq-seal_big_opM
  • ci/ralf/pm_red
  • ci/ralf/retime
  • ci/ralf/set_unfold_elements
  • ci/ralf/transfinite
  • ci/robbert/faster_iDestruct
  • ci/robbert/faster_iDestruct2
  • ci/robbert/faster_iFresh_joe
  • ci/robbert/iFrame
  • ci/robbert/into_val_pures
  • ci/robbert/kill_locked_value_lambdas
  • ci/robbert/naive_solver
  • 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
31 results
You can move around the graph by using the arrow keys.
Created with Raphaël 2.2.028Jun272625242120191817161514131211109765432131May3029282726252423222120191716151312987642130Apr29272625242317169873229Mar26222019171615141312765432128Feb2726252423222120191816137653130Jan29282726252423221918171514131110225Dec22212019181514131210876330Nov292827262220161211986131OctUp to 14 binders for `iRevert`, `iRevertIntros`, `iInduction` and `iLöb`!Bump stdpp.Up to 12 binders for `iRevert`, `iRevertIntros`, `iInduction` and `iLöb`.chains using le, remove ext condition, sums and discrete cofesMerge branch 'ralf/auth-core-id' into 'master'show auth_update_core_idbump std++CI.ci/robbert/naiv…ci/robbert/naive_solverBump stdpp.Merge branch 'sigT_equivI-admissible' into 'master'Prove sigT_equivI is admissible (fix #250)Prove `existT a` is NonExpansive & ProperFix another typo.carthesian closedMerge branch 'pg/typo-fix' into 'master'Fix typofixpointgroup CAS changes in changelog better togetherMerge branch 'ralf/cas' into 'master'remove some unnecessary scope annotationsavoid use of heap_lang notation in proofmode.vavoid using value notation for primitive operational rulesadd to CHANGELOGcomment nitsrename CompareExchange to CmpXchgconsistently annotate types for prophecy variables and listsremove some unneeded type annotationsuse equality instead of let bindingmake primitive compare-exchange return both boolean and old value for ease of useadd 'atomic triple' for compare-and-set, and use it in one exampleadd lemmas for combining CAS and Resolveturn CAS into compare-and-swap instead of compare-and-set: make it return the old valuedisable some notation for nowmore consistent order and format for CHANGELOGMerge branch 'sigT-cFunctor' into 'master'Reduce use of UIP as suggested by RobbertCofe and cFunctor for sigTintroduce notation for value comparisonralf/val-compareralf/val-compareMerge branch 'fix-sed-mac-really' into 'master'Fix instructions for Mac (and change them for Linux)