Skip to content
Snippets Groups Projects
Select Git revision
  • ci/debug
  • ci/for_proph
  • ci/hai/siProp
  • ci/janno/strict-tc-resolution
  • ci/ralf/Z_of_nat
  • ci/ralf/bi-language
  • ci/ralf/frame-frac
  • 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
  • ci/robbert/merge_sbi
  • ci/robbert/naive_solver
  • 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
34 results
You can move around the graph by using the arrow keys.
Created with Raphaël 2.2.011Mar1098765432129Feb282726252423222120191817161514131211109docs: UPreddocs: type-level laterdocs: explain why agreement has a chaindocs: global ghost functordocs: complete invariant namespacesstart describing invariant namespacesdocs: one-shotdocs: update iris.sty, some more on agreementdocs: locally non-expansive/contractive also applies to bifunctorsMerge branch 'master' of gitlab.mpi-sws.org:FP/iris-coqcomplete one_shotRename AlwaysStable into Persistent as suggested by Derek.remark about one_shotstart working on a one_shot constructionbenchmark extractor: deal with builds that are still runningfail the build if an Axiom has been foundadd some TODO so some stuff does not get forgottenMerge branch 'master' of gitlab.mpi-sws.org:FP/iris-coqdocs: get rid of division :)Merge branch 'master' of gitlab.mpi-sws.org:FP/iris-coqComment out admitted sts_frag_included, it is not used anyway.Merge branch 'master' of gitlab.mpi-sws.org:FP/iris-coqdocs: record notationMerge branch 'master' of gitlab.mpi-sws.org:FP/iris-coqRemove forgotten admit in auth.Merge branch 'master' of gitlab.mpi-sws.org:FP/iris-coqdocs: align CMRA inclusion notation with CoqMerge branch 'master' of gitlab.mpi-sws.org:FP/iris-coqget rid of an aborted lemmaMerge branch 'master' of gitlab.mpi-sws.org:FP/iris-coqRemove CMRA division.Choice principle for finite types.assume we can get rid of division for the paperdocs: minor editinggo back to # for values, now that this does not look like wp anymorenew (hopefully final) notation for wp: the keyword WPmake entailment notation look like entailmentnow that we use # for wp, use a different symbol for valuesUse fin for indexing into the global functor.Give the project a top-level name so it can be make installed.