Skip to content
Snippets Groups Projects

Repository graph

You can move around the graph by using the arrow keys.
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
Created with Raphaël 2.2.021Jul201918161513121165432130Jun2827262524232120191817161514876131May30292827252423222120191312111097643229Apr272625242120191815141312111098730Mar292322212019181716151412111098765432129Feb28Do not use agree_car in wsat anymore.* Atomicity of expressions is defined semanticallyMake ∖ left associative.Stronger masks for the WP of assert.Make lock and counter consistent with spawn.Partially revert "Explicit namespaces for counter, lock and spawn."Seal off definition of ndot and nclose.Explicit namespaces for counter, lock and spawn.Explicit namespace for heap instead of parametrizing over it.Remove weird notation for par.Repair tree_sum test case and add to _CoqProject.Better error messages when heap invariant cannot be opened.Remove no longer existing branch from .gitlab-ci.yml.Some tweaks.Merge branch 'rk/substitution'Write some comments.Use SOME/NONE in tests/one_shot.Solve atomic also using reification/vm_compute.Add comment to wp_done and slightly simplify it.Solve more to_val side-conditions using vm_compute.Also establish Closed and to_val _ = Some _ via reification.Merge branch 'rk/substitution' of gitlab.mpi-sws.org:FP/iris-coq into rk/substitutionshow more inforation in build logprefer tee over catstry to also capture user/sys time of buildingdump build times in the log, for good measureImplement substitution by reification.make list_reverse compileadd missing file to _CoqProjectadd list_reverse exampleCorrectness of in-place list reversal.Use option in spawn.Fix the match notation in heap_lang for option.Remove old comment.Revert "Add branch rk/substitution to gitlab-ci.yml."Fix typo in .gitlab-ci.yml.Add branch rk/substitution to gitlab-ci.yml.Misc clean up.Remove dependent types in heap_lang representation.make the extract script work better